3 ms·
��
by ampdepolymerase 6y ago
��
- TheAsprngHacker 6y agoGiven that most (but not all) Lisps are untyped, I don't see what Lisp evangelism has to do with the Curry-Howard correspondence...
- wglb 6y agoWhich Lisp are you referring to? There are types all over CL.
- TheAsprngHacker 6y agoSorry, by "untyped" I meant "dynamically typed." CL does have a sophisticated type hierarchy, but to my knowledge, according to the standard, types are checked at runtime, right? In the type-theoretic sense, "type" refers to a statically known classification. Curry-Howard is the idea that static types are propositional formulas and expressions that have such types are their proofs. Under the Curry-Howard correspondence, a static typechecker analyzing your program is equivalent to a proof checker ensuring that your proof is valid. People tend to invoke Curry-Howard to praise ML- and Haskell-style algebraic types (according to Curry-Howard, sum types are disjunction, product types are conjunction, and function/exponential types are implication).
- wglb 6y agotypes are checked at runtime, right? Not entirely. There are type errors that are caught at compilation time. A stark difference is that Lisp has the idea that type checking is done on values, not on symbols. If the compiler can deduce that a value is going to conflict in a given context, it will flag the error. And types are checked at run time as well.