Haskell for Coq programmers March 17, 2014
So you may have heard about this popular new programming language called Haskell. What’s Haskell? Haskell is a non-dependently typed programming language, sporting general recursion, type inference and built-in side-effects. It is true that dependent types are considered an essential component of modern, expressive type systems. However, giving up dependence can result in certain benefits for other aspects of software engineering, and in this article, we’d like to talk about the omissions that Haskell makes to support these changes.