[Smaug123]

At $WORK we use initial algebras in F# instead of tagless final. (They're isomorphic ideas.) It's possible to hack up a GADT using the initial algebra pattern, if you have existential types (which you can get via skolemisation) and type-equality types (which you can pretend exist as a pair 'a -> 'b and 'b -> 'a).

[aardvark291]

What is a GADT?

[Smaug123]

"Generalised algebraic data type". Pattern-matching on a GADT not only gives you information about the term that was in the datatype, but also about a type that was in the datatype.

For an ADT that doesn't need the power of GADTs: pattern-matching on a List<'a> gives you either an Empty or a Cons(x, xs), where you know up front before you do the pattern-match that x and xs are of type 'a and List<'a>.

For a GADT that is not an ADT: pattern-matching on an Expression might give you "Const(a) where a is an int", or "Equal(a, b) where a, b are bools", etc. Without doing the pattern-match, you can't necessarily tell what types you've ended up with.