Simulating existential quantification in function return types

Question

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.

Answer 1

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:

1. Possible overhead with the additional function application (I don't know how much the compiler can optimize this).
2. Less readable code (at least for people not used to continuations).