Uustalu, Altenkirch and Capretta have come up with a way of hiding partial functions inside a monad. The idea is that partiality is an effect, and can be treated in the same way as, for example, IO in Haskell. You can see more about this on the Nottingham FP lunch page, or talks by Altenkirch or Uustalu.

Anyway, I decided to try to implement this, and use it to write an evaluator for the SK combinator calculus in Coq. The SK calculus can implement all computable functions (it is Turing complete), so writing this evaluator suggests that any language with primitive recursion over strictly positive inductive families and coinduction would be Turing complete too (e.g. Epigram, with the addition of coinduction). Any nasty effects such as non-termination, however, could be hidden inside a monad, so you could tell from a program's type whether it was definitely terminating, or possibly non-terminating.

My implementation is below. There is a Coq script, an extracted
Haskell module containing the partiality monad (called
`Delay`

) and a small driver program with some examples.

- The original Coq script
- The extracted Haskell module
- The Haskell driver