Anonymous user
Talk:Proof: Difference between revisions
m
→Haskell: run -> compile
(→Draft status: re) |
m (→Haskell: run -> compile) |
||
Line 160:
:: "Yes, but..." The solution requires two languages extensions (GADTs and type families) that together allow one to express some dependent types. They are not as expressive as full dependent types, but are powerful enough to express this rather simple theorem and its proof.
:: Your understanding of dependent types is wrong: the typing is not done at run time, but rather code is executed at compile time. Haskell cannot execute arbitrary code at
:: The "but" is that fact that Haskell allows general recursion, making the logic unsound, i.e. any theorem - including false ones - can be proven by an expression that would diverge at run-time. The given solution does not use this "feature", however.
:: This is a solution that the task should clearly allow, with the appropriate footnotes, though. —''[[User:Ruud Koot|Ruud]]'' 18:35, 12 May 2012 (UTC)
| |||