I think good insight on GADTs can be that they're no more than sugar around "implicit fields" - like, ignoring restrictions on typeclass instance manipulation, you could write them by hand with normal ADTs:
If GHC let us explicitly pass instances around (or Show was a normal record).
You don't want to do that in Haskell - this way you would have to manually apply "coercions" and pass instances around, and compiler wouldn't be that clever in exhaustivity checking - but it can help you realize what GADTs can and cannot do.
-- You'll see why I'm doing this later onnewtypeEmpty=Empty{unEmpty::Void}dataNonEmpty=NonEmptydataListxy=Nil(IsoyEmpty)|forallz.Cons(IsoyNonEmpty)x(Listxz)
https://haskell.zettel.page/5956fd49.html
I think good insight on GADTs can be that they're no more than sugar around "implicit fields" - like, ignoring restrictions on typeclass instance manipulation, you could write them by hand with normal ADTs:
could be written as:
Similarly:
could be written as:
If GHC let us explicitly pass instances around (or
Show
was a normal record).You don't want to do that in Haskell - this way you would have to manually apply "coercions" and pass instances around, and compiler wouldn't be that clever in exhaustivity checking - but it can help you realize what GADTs can and cannot do.
First-class type equality is also an important part of it.
Knowing the "index type" of a GADT can tell you something about what constructors are possible for a GADT value. http://wiki.haskell.org/Generalised_algebraic_datatype#Example_with_lists Is that captured in the "implicit fields" explanation, or a further fact?
@Daniel Díaz Carrete let's copy that example there:
and rewrite it in terms of explicit fields:
Now,
safeHead
would be:Basically, in unreachable case you can create
Void
by using nonexistentIso Empty NonEmpty
, making both typechecker and exhaustivity checker happy