| > That's a little weird to me ... it seems to be confusing the metalanguage and the language being implemented. Well, that's sort of the point. It's perhaps a little less important if you're writing a compiler for a separate programming language, but that's a relatively rare use case. GADTs are mainly used for implementing DSLs to be used elsewhere in the same program. > Is the more abstract GADT solution supposed to "save" you some work of writing a type checker by somehow letting you reuse Haskell or OCaml's type system to express that? Yes. Writing your own typechecker and integrating it into an existing compiler pipeline is a ton of work, easy to screw up, and a potential compatibility nightmare. > I also wonder how all that is actually implemented and expanded into running code. The GADT syntax seems to get further and further away from something I imagine can be compiled :) GADTs are syntactic sugar for constrained type constructors. So this data Example a where
Example :: Int -> Example Int
becomes this data Example a = (a ~ Int) => Example a
which is then compiled to a type coercion in the intermediate language |