Existentials on a leash | existentials-on-a-leash

Existentials on a leash<br>In 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).<br>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.<br>This technique also relies on linear types, but not the encoding mentioned above.<br>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.<br>I explain why I believe the coercions are safe, but I haven’t proven anything formally.<br>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.<br>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.<br>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).<br>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: (forall a. a -> r) -> r. This corresponds to exists a. (a -> r) -> r (which is equivalent to exists a. a).

Using a GADT: data Wrapper where Wrapper :: forall a. a -> Wrapper. When pattern matching on Wrapper, a will be existentially quantified.

Both these techniques do not actually use existential quantification, but instead encode it through negated universal quantification.<br>A GHC proposal for adding first-class existential types to GHC was written a while ago, but the author seems to be prioritizing other work.<br>The proposal also shows a simple example of a function that is impossible to write using the CPS-style or GADT wrapping: a lazy filter :: (a -> Bool) -> Vec n a -> exists m. Vec m a.

The encoding presented in this article can be used to implement many of the motivating examples from the GHC proposal, including the lazy filter.<br>However, when I started this project, I was using vectors from an external package which did not export its constructors, and to test a lazy filter I also needed a lazy function to create vectors, so that became the main example of the article.<br>I didn’t end up needing so many existing functions on vectors, so the article now defines its own vectors, but the example stayed.<br>So instead of a lazy filter function, I’ll demonstrate the benefits of the encoding using a function lazyVecFromList :: [a] -> Exists m (Vec m a) that lazily converts lists to vectors.

Sadly, this encoding did not work so well for defining optics with existentially quantified types<br>I continued searching and found a different technique that makes such optics possible.

But before we dive into these techniques, let’s see why we can’t write a lazy vecFromList using CPS-style or GADT wrapping.<br>We’ll work out the second option, but first we need to enable some language extensions and import some stuff.<br>I also define my own . because the version from linear-base is not as polymorphic as I’d like it to be.

Imports and language extensions

{-# LANGUAGE AllowAmbiguousTypes #-}<br>{-# LANGUAGE LinearTypes #-}<br>{-# LANGUAGE TypeAbstractions #-}<br>{-# LANGUAGE TypeFamilies #-}<br>{-# OPTIONS_GHC -Wall -Wno-missing-signatures -Wno-unused-top-binds -Wno-orphans #-}

{- HLINT ignore "Use first" -}

{- cabal:<br>ghc-options: -Wall<br>default-language: GHC2024<br>build-depends:<br>base,<br>linear-base,<br>lens,<br>mtl,<br>profunctors,<br>kind-apply,<br>-}<br>{- project:<br>with-compiler: ghc-9.12.3

index-state: 2026-03-18T08:38:52Z

semaphore: True<br>-}

import Control.Functor.Linear (Monad (..))<br>import Control.Functor.Linear qualified as Control<br>import Control.Lens qualified as Lens<br>import Control.Monad.Except<br>import Control.Monad.State.Lazy qualified as NL<br>import Control.Optics.Linear<br>import Data.Bifunctor.Linear<br>import Data.Char<br>import Data.Functor qualified as NL<br>import Data.Functor.Identity<br>import Data.Functor.Linear<br>import Data.Kind<br>import Data.Maybe<br>import Data.PolyKinded hiding (Nat)<br>import Data.Profunctor.Kleisli.Linear<br>import...