GADT are really cool, but I would like to note three caveats:
1.
> in lines 13..21, an AVLTree type is defined -- with its invariants encoded in the type system
Its balance invariants are encoded, but its ordering invariants are not.
2. The code for manipulating AVL and red-black trees in GADT form is significantly more complicated that it would be if they were not in GADT form.
3. Sometimes, whether using GADTs or not, one ends up with code like this, from the AVL example:
> Nil -> undefined -- shouldnt happen
Needless to say, this negatively affects the comfort we might receive from the type system.
Having said all that, I think there are cases where GADTs are really worth the extra effort. Sometimes, they even simplify code when the alternative to GADTs is checking things at run-time!
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.
Comments
GADT are really cool, but I would like to note three caveats:
1.
> in lines 13..21, an AVLTree type is defined -- with its invariants encoded in the type system
Its balance invariants are encoded, but its ordering invariants are not.
2. The code for manipulating AVL and red-black trees in GADT form is significantly more complicated that it would be if they were not in GADT form.
3. Sometimes, whether using GADTs or not, one ends up with code like this, from the AVL example:
> Nil -> undefined -- shouldnt happen
Needless to say, this negatively affects the comfort we might receive from the type system.
Having said all that, I think there are cases where GADTs are really worth the extra effort. Sometimes, they even simplify code when the alternative to GADTs is checking things at run-time!
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.