[Haskell-cafe] Enforcing data structures invariant in the type system
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
More information about the Haskell-Cafe