Partiality is an effect

In languages like Coq where all computations must terminate and only total functions are allowed it would still be nice to be able to express non-terminating computations. While searching for solutions other people had come up with I stumbled across this little Coq development: SK Combinator Calculus Interpreter.
The main insight is that you can view partiality as a computational effect that can be hidden inside a monad. I think it’s a clever and intriguing idea.

This entry was posted in Coq and tagged , , . Bookmark the permalink.

Leave a Reply

Your email address will not be published.

This site uses Akismet to reduce spam. Learn how your comment data is processed.