4 ms·

> 1. FP programming languages are not really Church’s lambda calculus, and the Y combinator in them is implicit. You cannot define a Y combinator in a typed LC.

• pron 9y ago
  Sorry, you are absolutely right. This can be done if the language allows for types to occur in "non-positive" positions (e.g., you can do `data T = X (T -> Bool)`, which is a type that doesn't have a model in a consistent set theory, and can't be defined in a consistent type theory). I don't know Haskell, but I'm playing with Lean, where this can't be done (Curry's paradox), and got confused. BTW, I've been told that the limitation of LC I discussed is handled nicely in computational type theories, like PRL, which, I'm told, is similar in many ways to the formalisms I do like (and so should be able to relate the different expressions of the factorial computation), but I know nothing about PRL so I can't really discuss it. I can't judge on how simple PRL is, seeing that the documentation is quite horrific, but my point is that there are very simple formalisms, both for formal proofs, like TLA+ (see my talk https://www.youtube.com/watch?v=15uy9Ga-14I https://www.youtube.com/watch?v=15uy9Ga-14I), and for programming, like Eve (IMO, the most advanced, publicly available programming language, in terms of PL theory), that make this very, very easy; and they're far easier to learn and much more uniform than Haskell.