Existentials on a Leash

Summary

Existentials on a leashIn this article, I will share an encoding for existential types in Haskell that allows them to appear “naked” in types, thus relieving us from having to wrap existential type variables with a GADT constructor or with a higher-rank function (CPS-style). The encoding is based on linear functions that consume a proof-token that ensures proper treatment of existentially typed values. Additionally, I share an independent technique that ensures functions instantiate hidden (“non-naked”) existential types in their result with the same type as its input type is instantiated, i.e. they preserve the instantiation of hidden type variables. This technique also relies on linear types, but not the encoding mentioned above. I will demonstrate by implementing a safe variant of the unsafePartsOf:: Functor f => Traversing (->) f s t a b -> LensLike f s t [a] [b] optic combinator. Both techniques use unsafeCoerce. I explain why I believe the coercions are safe, but I haven’t proven anything formally. Please try to break this stuff if you see some hole I have missed. While I will briefly explain what linear types are, this article is not meant as a general introduction to this concept. Familiarity with GADTs, linear types and optics (for the sections pertaining to those) is recommended. That being said, I made it as easy as I can for the reader to tinker with the code and interactively learn about these concepts by providing a GitHub Codespace prebuild. Clicking that link will allow you to tinker with the code with the support of the Haskell Language Server without needing to install anything (hint: use “Preview embedded markdown” to see the .hs file with its markdown version to the side). It might even be a nice way to read the article because you can hover over variables and functions to see their types for example. Current limitations of existential types As of GHC 9.14, GHC only supports 2 ways of “existentially quantifying” type variables: With a rank-2 type...