Re:Trying Haskell
by Peaker on Tuesday April 12, 2011 @12:46PM
(#2437965)
1. True, this is harder in Haskell. More easily possible in a language like Agda.
2. The assurances you get in return are probably worth it.
3. I think that piece is unnecessary, and the type system will see that constructor is impossible. If it doesn't, it's a limitation of Haskell GADT's, and can be fixed. I don't think you ever resort to "Nil -> undefined" in Agda.
2. The assurances you get in return are probably worth it.
3. I think that piece is unnecessary, and the type system will see that constructor is impossible. If it doesn't, it's a limitation of Haskell GADT's, and can be fixed. I don't think you ever resort to "Nil -> undefined" in Agda.