3 ms·
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,
by Smaug123 7y ago
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 7y agoWhat is a GADT?
- Smaug123 7y ago"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.