|
dougdrums posted:How would you explain polymorphic lambda calculus well enough for another person to be able to derive typing judgements by hand? Let's say that this person is a Java programmer that is loosely familiar with prop logic. I can't do it without puking out formalisms or being too vague. I would start by constructing proof trees using typing rules for simply-typed lambda calculus, unless there's some pressing need to skip straight into System F. I don't see any way to avoid the formalism - in the simply-typed case, it is straightforward and easy to apply. The typing rules have fairly obvious interpretations which might make them easier to remember and understand.
|
#
¿
Feb 24, 2016 09:44
|
|
|
|
| # ¿ May 15, 2024 10:33 |
|
|
I learned to program in Haskell, and the worst thing about having to use other languages in school (Java, C, Ruby, OCaml) is the lack of typed side effects (and the entire apparatus Haskell uses to accomplish this). I'm pretty convinced that monads should be Haskell's selling point (from a software development standpoint), but I might just be brainwashed or something.
quickly fucked around with this message at 05:30 on Feb 27, 2016 |
|
#
¿
Feb 27, 2016 05:25
|
|