3 ms·
There's also this: http://www.haskell.org/haskellwiki/Curry-Howard-Lambek_correspondence http://www.haskell.org/haskellwiki/Curry-Howard-Lambek_corre...
by Natsu 12y ago
There's also this:
http://www.haskell.org/haskellwiki/Curry-Howard-Lambek_correspondence http://www.haskell.org/haskellwiki/Curry-Howard-Lambek_corre...
- evincarofautumn 12y agoThis one is beautiful as well. It was mind-opening for me to think of types in terms of provability (intuitionistic/constructive logic) rather than truth (classical logic). The only way to prove that a function returning a value of type T actually halts (and therefore does not actually “return” bottom/void) is to run it and obtain that T value, i.e., to find the object that the type claims exists.