3 ms·

Nice article, but Haskell type system is not a logical limit. I would say that Coq's type system (or some other Martin Lof type system) would be a logical limi

• eru 17y ago
  > Nice article, but Haskell type system is not a logical limit. Indeed. Though it makes some sense as a figure of speech.
• camccann 17y ago
  (is there IO Monad in Coq?) To the best of my knowledge, no. If memory serves me, Coq actually isn't even Turing-complete, being a typed lambda calculus with no general fixpoint operator (specifically, a variant on the Calculus of Constructions). Any "program" that "type checks" in Coq is thus provably terminating. Note that, in Haskell terms, the simplest general fixpoint operator is: y :: (t -> t) -> t y f = f (y f) ...which, interpreting "->" as logical implication, is a theorem stating that a proposition implying its own truth implies its own truth. Given that (t -> t) is clearly a tautology, this suffices to prove all possible propositions, also known as the "principle of explosion". [0] On the other hand, see http://ynot.cs.harvard.edu/ http://ynot.cs.harvard.edu/ for an attempt to add side-effects and general recursion to Coq in a controlled fashion, in order to turn it into more of a programming language. [0] http://xkcd.com/704/ http://xkcd.com/704/