Pedagogical theory for GADTs

[arxanas]

Expanding on the Twitter comment here: https://twitter.com/arxanas/status/1457051545233604609

I wrote an article for my team on the topic of GADTs (called "Real World GADTs", haha). You can find a copy of the article here: https://docs.google.com/document/d/1hfXGtFPFeS7AOweOvvCBp7v4lBBKxRFe/edit.

Point 1: emphasize practical use-cases

There are three categories of GADTs which are interesting to consider for a one-type-variable GADT, and used for very different things:

• Zero type variables on the right side of the arrow: for existential types.
  • Motivating case: serialization/deserialization, when type safety is lost and needs to be explicitly recovered. An example using Marshal would be quite practical.
• One type variable: for type mappings.
  • Motivating case: type-safe RPC/API call system.
  • Motivating case: ad-hoc polymorphism.
• Two or more type variables: for type equality constraints.
  • Motivating case: avoiding mixing up variables of the same type using phantom types.
  • Motivating case: being a compiler nerd and evaluating ASTs. But this happens very rarely...

In my experience, they're useful in practice in the following order: 1 (most useful), 0, 2+ (least useful). Pedagogically, this means that the AST evaluator example is the least important, even if it's the most interesting from a type-theoretical view. We should strongly deemphasize it. My advice is to focus on completely different examples for this chapter, because the given one is not "real-world" at all.

Point 2: the type annotation syntax is unintuitive

The syntax for GADT type annotations is not particularly intuitive. My recommendation is to advise that the reader primarily do rote symbolic manipulation of the involved types.

Compare to TypeScript's mapped types, where you use a type and square brackets and that indicates that you're carrying out a mapping from one type to another — just the same as mapping values. A is a type map and A[B] is a value in the type map, the result of indexing A by B.

On the other hand, consider a type signature like type a. a value -> a. Logically, you're applying a type mapping operation, in the sense that you start with an a and want to apply the value map to it and get an output type. But the input type is a value and the output type is a.

This is somewhat unintuitive from a value standpoint. The expressionfun x -> f x is the same kind of thing (from a certain point of view), but the map application is on the opposite side of the arrow!

This point might be hard to grasp if you're used to using OCaml GADTs, but in my experience, it's a significant confounder for users, and it should be addressed explicitly.

[yminsky]

Thanks for the detailed notes! I think your point about the AST example being a bit rare is reasonable, but I still think it's a reasonable place to start, for a few reasons. First, it's an example that lets you really easily cover a lot of ground in terms of the mechanism. Second, it's more real-world than you I think you're giving it credit for. We build lots of little embedded languages as a regular thing, and understanding how GADTs can help is useful there.

I think I just disagree with you on the syntax. The syntax could surely be better (indeed, OCaml's syntax is not ideal in many aspects), but I think it's absolutely worth trying to explain the intuition behind it. I tried to both explain good rules of thumb, and provide a basic understanding of where those rules come from.

Finally, the RPC example you suggest is a good one, and one I considered, but I think the current list is a reasonably balanced set.

Anyway, thanks for all the thoughts!