Simulating existential quantification in function return types

existential-type, gadt, haskell, return-type

Solution

The standard solution is to create an existentially quantified data type. The result would be something like

{-# LANGUAGE ExistentialQuantification #-}

data Exists1 = forall a . (Show a) => Exists1 a
instance Show Exists1 where
    showsPrec _ (Exists1 x) = shows x

somethingPrintable1 :: Int -> Exists1
somethingPrintable1 x = Exists1 x

Now, one can freely use `show (somethingPrintable 42)`. `Exists1` cannot be `newtype`, I suppose it's because it's necessary to pass around the particular implementation of `show` in a hidden context dictionary.

For type-safe vectors, one could proceed the same way to create `fromList1` implementation:

{-# LANGUAGE GADTs #-}

data Zero
data Succ n

data Vec a n where
    Nil  ::                 Vec a Zero   
    Cons :: a -> Vec a n -> Vec a (Succ n)

data Exists1 f where
    Exists1 :: f a -> Exists1 f

fromList1 :: [a] -> Exists1 (Vec a)
fromList1 [] = Exists1 Nil
fromList1 (x:xs) = case fromList1 xs of
                    Exists1 r -> Exists1 $ Cons x r

This works well, but the main drawback I see is the additional constructor. Each call to `fromList1` results in an application of the constructor, which is immediately deconstructed. As before, `newtype` isn't possible for `Exists1`, but I guess without any type-class constraints the compiler could allow it.

I created another solution based on rank-N continuations. It doesn't need the additional constructor, but I'm not sure, if additional function application doesn't add a similar overhead. In the first case, the solution would be:

{-# LANGUAGE Rank2Types #-}

somethingPrintable2 :: Int -> ((forall a . (Show a) => a -> r) -> r)
somethingPrintable2 x = \c -> c x

now one would use `somethingPrintable 42 show` to get the result.

And, for the `Vec` data type:

{-# LANGUAGE RankNTypes, GADTs #-}

fromList2 :: [a] -> ((forall n . Vec a n -> r) -> r)
fromList2 [] c      = c Nil
fromList2 (x:xs) c  = fromList2 xs (c . Cons x)

-- Or wrapped as a newtype
-- (this is where we need RankN instead of just Rank2):
newtype Exists3 f r = Exists3 { unexists3 :: ((forall a . f a -> r) -> r) }

fromList3 :: [a] -> Exists3 (Vec a) r
fromList3 []     = Exists3 (\c -> c Nil)
fromList3 (x:xs) = Exists3 (\c -> unexists3 (fromList3 xs) (c . Cons x))

this can be made a bit more readable using a few helper functions:

-- | A helper function for creating existential values.
exists3 :: f x -> Exists3 f r
exists3 x = Exists3 (\c -> c x)
{-# INLINE exists3 #-}

-- | A helper function to mimic function application.
(?$) :: (forall a . f a -> r) -> Exists3 f r -> r
(?$) f x = unexists3 x f
{-# INLINE (?$) #-}

fromList3 :: [a] -> Exists3 (Vec a) r
fromList3 []     = exists3 Nil
fromList3 (x:xs) = (exists3 . Cons x) ?$ fromList3 xs

The main disadvantages I see here are:

- Possible overhead with the additional function application (I don't know how much the compiler can optimize this).

- Less readable code (at least for people not used to continuations).

Problem

Sometimes I come upon a need to return values of an existentially quantified type. This happens most often when I'm working with phantom types (for example representing the depth of a balanced tree). AFAIK GHC doesn't have any kind of `exists` quantifier. It only allows existentially quantified data types (either directly or using GADTs). To give an example, I'd like to have functions like this: ``` -- return something that can be shown somethingPrintable :: Int -> (exists a . (Show a) => a) -- return a type-safe vector of an unknown length fromList :: [a] -> (exists n . Vec a n) ``` So far, I have 2 possible solutions that I'll add as an answer, I'd be happy to know if anyone knows something better or different.

Original source