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

[Nicola Gigante]

> Il giorno 30/mar/2015, alle ore 19:14, Marcin Mrotek <marcin.jan.mrotek at gmail.com> ha scritto:
> 
> Hello,
> 
Hi!

> 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:
> http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Main.Othertutorials)
> 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
> easier.
> 
I appreciate this suggestion! 
Agda has been on the todo list for a while. Which do you suggest to start
from, choosing between agda and idris? Are there any major differences?

> Secondly, have a look at Liquid Haskell:
> http://ucsd-progsys.github.io/liquidhaskell-tutorial/01-intro.html
> Refinement types are a restricted kind of dependent types that can be
> solved automagically by SMT solvers.
> 
I’ve read a paper about liquid haskell some time ago and I find it amazing.
What I’d like to ask now is: is liquid haskell strictly more expressive than the
haskell type system or is “only” a more convenient way of writing the constraints
in a way that can be efficiently solved?

> 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
> 

Thank you! Those are exactly the droids I was looking for.

> Best regards,
> Marcin Mrotek

Greetings,
Nicola