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

[Marcin Mrotek]

Hello,

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

I admit I only have experience in using Agda, I've name-checked Idris
after only reading the docs (the last time I tried to install the
compiler, cabal didn't let mi do it because of package conflits; now I
tried again and it's doing just fine). Idris is newer and, apparently,
more oriented towards practical programming than theorem proving,
that's all I know.

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

It depends on what you mean by "Haskell's type system". It's more
capable than Haskell's type system without extensions, and less than
full-on dependent typing (delibrately so, because dependent type
equivalence is undecidable). I don't know where exactly does
Haskell-with-GHC-extensions type system lie. I think it's the same as,
let's say, Agda's, only requiring more kludges when moving back and
forth between type- and value-level, but I'm not sure. I'm just a
"self"-taught programmer, not a computer scientist ;)

Best regards,
Marcin Mrotek