[Haskell-cafe] Enforcing data structures invariant in the type system
nicola.gigante at gmail.com
Mon Mar 30 17:23:54 UTC 2015
> Il giorno 30/mar/2015, alle ore 19:14, Marcin Mrotek <marcin.jan.mrotek at gmail.com> ha scritto:
> 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
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:
> 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
More information about the Haskell-Cafe