3 ms·
Can you clarify the essential difference between Haskell's and Agda's versions of monadic I/O? Or are you talking about divergent side-effects like bottom and
by mbrock 12y ago
Can you clarify the essential difference between Haskell's and Agda's versions of monadic I/O?
Or are you talking about divergent side-effects like bottom and exceptions?
- mafribe 12y agoThanks for your question. I should have been more careful. I meant Agda used as a prover, not Agda used as a 'conventional' programming language (Indeed in years of usage, I've never executed an Agda program, I've only ever used the type checker). In other words, Agda, the proof calculus for Martin-Loef type theory. That said, I was talking about effects in general, including non-termination, exceptions, concurrency ...