I've come to think that these toy interpreter examples are a bit questionable unless they contain a variadic structure like an arbitrary tuple - they give the impression that programming with GADTs is simpler than it really is.
Problem with toy AST examples is they're great if you're doing something like that, but don't give much motivation if you're not. (Unless you starting seeing all programming as AST manipulation, which can be an interesting viewpoint.)
More important that using GADTs for one thing or another is to start looking at the type checker as something you use to assist you in writing the kind of code you want to write, and avoiding the kind of code you want to avoid. GADTs are one amoung many useful tools in the modern toolbox for that.
That’s a really fascinating post! Thank you! I’m still not sure I understand GADTs (in part, here, because I know very little Haskell indeed) but this helps.
Do GADTs allow Turing-complete computation at compile time, like C++ templates? Are there limits to what kind of correctness properties you can use them to get compile-time machine-checked proofs of?
GADTs by themselves do not allow arbitrary computation[1]. But Haskell also allows you to write functions at the type-level ("type families" in the Haskell jargon), so you can directly write functions to compute types without any trickery, and the Propeller example uses this feature.
GADTs let you write down basically the same things that you could write as an inductive datatype in a dependent language like Coq and Agda. So (with some patience) you can make a function return a "proof" of anything that can be witnessed by a first-order inductive type, e.g. equations between expressions, list membership, proofs that a term in an object-language is welltyped, etc. The main limitation is that Haskell doesn't have any termination checking, so if you consider it as a dependently typed language there is no way to write a trustworthy proof that uses induction. Also its not very user-friendly, see [2] for some examples.
[1] Basically, GADTs are equivalent to having equations between types. If all the equations are written out in full, it is reasonably straightforward to check whether two types are provably equal. If you want to do type _inference_, i.e. figure out what equality assumptions a given function should make in order to become welltyped, then you run into various undecidable problems (e.g. "rigid E-unification"). My guess would be that if you wrote down a completely general typesystem featuring GADTs, then you would be able to encode arbitrary computations as type-inference problems, but the encoding would be very clumsy. The Haskell and Ocaml implementations deliberately don't try to be very general in the type inference, and instead try to pick a decidable subset, so the programmer has to add enough type annotations to guide it.
data Rec (f :: k -> *) (ts :: [k]) where
RNil :: Rec f '[]
(:&) :: f t -> Rec f ts -> Rec f (t ': ts)
infixr 9 :&
data ElField f where
Field :: KnownSymbol s => t -> ElField '(s, t)
x :: Rec ElField ['("foo", Int), '("bar", String)]
x = Field 3 :& Field "bar" :& RNil
It's an embedding of (variadic) typed records.
Anyway, I don't actually use GADT-driven embedded ASTs myself. They're just a pretty clear example.
[0] This is Jon Sterling's `vinyl` package in Haskell
