[Haskell-cafe] Enforcing data structures invariant in the type system

Marcin Mrotek marcin.jan.mrotek at gmail.com
Mon Mar 30 17:14:13 UTC 2015


First of all, if you don't mind me not answering your question
directly, I'd strongly suggest learning Agda or Idris before you start
using dependent types in Haskell. (for example try the first two
tutorials from here:
These are true dependently typed languages, and while GHC's extensions
can get Haskell remarkably close, the result is still somewhat clunky.
IMHO learning the basics in a cleaner environment is going to be much

Secondly, have a look at Liquid Haskell:
Refinement types are a restricted kind of dependent types that can be
solved automagically by SMT solvers.

Thirdly, as for your actual question, have a look at this series of
tutorials: https://www.fpcomplete.com/user/konn/prove-your-haskell-for-great-safety/dependent-types-in-haskell

Best regards,
Marcin Mrotek

More information about the Haskell-Cafe mailing list