GADTs That Can Be Newtypes and How to Roll 'Em, 2nd Revision: Arbitrary Embeddings, Keeping It Shallow & Unboxed GADTs

10 Likes

Thanks, this might be a useful reference.

Another somewhat different example is using a machine word for a Peano-natural-like GADT. This is used in the pqueue package, and might also end up in containers (containers #1078).

3 Likes

Thanks for pointing me to this! Apart from being a nice example in its own right, it also reminded me that I’d actually encountered a similar technique in a @rae video years ago, though clearly it’d fallen out of my head in the meantime.

In any case, I realised the woeful incompleteness of the article, so I’ve written a 2nd revision with three new sections: Arbitrary Embeddings, Keeping It Shallow and Unboxed GADTs.

Of course, there are changes to other parts—like broadening Computable Classes to encompass the offerings of GHC.TypeLits—but they’re mostly tweaks and can be ignored; I invite anyone who enjoyed the original article to read the new second half!

1 Like