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