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

Il giorno 30/mar/2015, alle ore 19:14, Marcin Mrotek 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/dep...

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

Best regards, Marcin Mrotek

Greetings, Nicola