2 ms·
Great explanation. I would have killed to see something like this back when I had no clue what GADTs were about. The only thing I would add is pointing out that
by ufo 13y ago
Great explanation. I would have killed to see something like this back when I had no clue what GADTs were about. The only thing I would add is pointing out that the syntax you used in the end kind of does the same thing as
data Node = Nil | BlackNode | RedNode
but with the extra extra restrictions on the type variables.
- tel 13y agoThanks, and true. GADTs are weird creatures when you first see them. I originally thought it was entirely a syntactic thing! As weird as it is, I always recommend Agda/Coq for learning GADTs. It feels like overkill, but Haskell's DT stuff is really wonky, so it's nice to see GADTs expressed in a clean manner before trying them out in Haskell.