3 ms·
(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 n
by 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/