tel

90 ms·

841.
by tel 11y ago
Silly and wonderful there is always data Fake a = Fake which is trivially a monad instance Monad Fake where return _ = Fake Fake >>= f = Fake yet it clearly contains nothing.
842.
by tel 11y ago
I agree, but am pretty excited by the opportunity that such research will have outsize long-term benefits.
843.
by tel 11y ago
You can compose Monads in this way too. Even in Haskell, mtl-style transformers are very similar.
844.
by tel 11y ago
I don't see any meaningful distinction between human reasoning and logic, tbqh. As I stated earlier, your stacks of scoped continuations are exactly equivalent to monads but, depending on how you restrict them, a little less flexible.
845.
by tel 11y ago
Ah, yes. Generally you're right: on 2nd order functions ((nat -> nat) -> nat) TMs and LC differ where TM's have strictly more functionality. But then it flips again at 3rd order (((nat -> nat) -> nat) -> nat) and so
846.
by tel 11y ago
I'm interested as well in alternative ways to do this kind of thing which are more "psych friendly" though I don't have any warm leads at the moment. I don't think of CH as being a way of doing verification, as you
847.
by tel 11y ago
It's late, so while I'd like to bite more, I'll just take this one on: > other than that our mathematical exploration is guided by our human minds I think that's exactly it. I'm not honestly a good enough philoso
848.
by tel 11y ago
Have a pure model of memory which is implemented directly. Associate this with a proof that the extensional side of it is pure (copying mechanics of substructural types) and you're done.
849.
by tel 11y ago
I'm curious to see how parallel or is implemented on a TM. It's not a function from (nat -> nat) of course since we're talking about something other than extensional equality... but even then I tend to find these things no
850.
by tel 11y ago
I'm being a little poetic and talking a little limitedly about calculus. Obviously it's got big connections elsewhere, but my perspective on it has shifted a lot.
851.
by tel 11y ago
I think this is an interesting perspective to think about. I certainly remember a long time where I felt this way—that calculus was the entire reason for learning mathematics and the rest are a little silly or outdated. It took a long time
852.
by tel 11y ago
Yup, that's another way to do it so long as you're interested in paying the explicitness tax to introduce substructural types. My point about Hoare logic is not to promote it but instead to note that it's not categorically di
853.
by tel 11y ago
Equational reasoning extends to mutation as long as you track the monad. It also smoothly devolves into Hoare Logic. It's the same tool, just applied in either different (monadic) contexts. Mutation is not disallowed in PFP, by the way
854.
by tel 11y ago
I'm interested what you mean by [1]. The rigorous part of Church's Thesis says exactly that the set of LC-computable, TM-computable, and general recursive functions (nat -> nat) are all identical. This is somewhat weaker that &
855.
by tel 11y ago
You can write an interpreter in any language. That's what I'm angling for here. There's no relationship to laziness except that if Haskell is your only example implementation then you're stuck with it.
856.
by tel 11y ago
I agree, but then I also add to that the roughly four major definitions of what that means today and the various misinterpretations therein and call it a wash. It's a series of cultures all bandied about within a larger cultural phenom
857.
by tel 11y ago
Oh, I'm completely happy to roll all of "tooling, libraries, community" into "language". It matters a ton which one you choose! But we're not disagreeing here. The relative merits of all these factors are expen
858.
by tel 11y ago
> a non-Haskell (or Haskell-like) PFP I'd immediately suggest that Haskell is not a particularly pure language itself and that you should take a look at { Coq, Agda, Idris } for far more ideas about where PFP ought to go. You can al
859.
by tel 11y ago
It's not lazy performance, it's a representation of that computation as a value. Most concretely by an interpreter. That's not really lazy evaluation and suffers from almost none of the ailments.
860.
by tel 11y ago
Hm, well, I suppose I'm in agreement about many things, but also a little unsure of how to interpret PFP unless it is meant to be "PFP = Haskell". I think the primary things I'd ask about or try to answer revolve around
861.
by tel 11y ago
I've written something like this, essentially just providing sum types, but it'e currently embedded in some code at work. If anyone is familiar with putting ES6 NPM libraries together and would like to help, I'd be happy to o
862.
by tel 11y ago
I'm not confident that it's much easier in any universal sense, but I certainly agree that the nature of at least the presentation of an algorithm defines the easiest way to talk about its analysis.
863.
by tel 11y ago
It's not actually crappy at all for complexity analysis. Laziness is sometimes spoken about in that way, but nobody is forcing you to be lazy.
864.
by tel 11y ago
That is precisely my favorite definition :)
865.
by tel 11y ago
Ah, now I think I understand what they were trying to argue—full ES5 versus ES6 where I took it to be ES6 versus ES6-using-class.
866.
by tel 11y ago
Javascript has Object.freeze and Object.seal built right in! How is that not emphasis? (He asks with a touch of both sarcasm and seriousness.) (I seriously believe that any attempt to define FP will end in tears. It's a marketing term
867.
by tel 11y ago
Also, I'm a fan of saying that "FP" is a community not a definition.
868.
by tel 11y ago
I think it's well known that Cont is the "mother of all monads" which gives you the embedding. Then, anywhere you have global continuations you can have delimited continuations with one global variable. This is less well know
869.
by tel 11y ago
There's at least one bit that goes further than you've noted and while it has an analogue in vegetarianism, it's much more important to note in FP. It's this: language choice is often a shared/communal one. Therefor
870.
by tel 11y ago
More Javascript `this` juggling. I really want to write a wrapper around `createClass` which just passes things as normal arguments.

More ›