Existential type wrappers necessity

Question

Turns out that it is surprisingly difficult to use existential/rank-n types correctly despite the very simple idea behind them.

Why are wrapping existential types into data types is necessary?

I have the following simple example:

{-# LANGUAGE RankNTypes, ImpredicativeTypes, ExistentialQuantification #-}
module Main where

c :: Double
c = 3

-- Moving `forall` clause from here to the front of the type tuple does not help,
-- error is the same
lists :: [(Int, forall a. Show a => Int -> a)]
lists = [ (1, \x -> x)
        , (2, \x -> show x)
        , (3, \x -> c^x)
        ]

data HRF = forall a. Show a => HRF (Int -> a)

lists' :: [(Int, HRF)]
lists' = [ (1, HRF $ \x -> x)
         , (2, HRF $ \x -> show x)
         , (3, HRF $ \x -> c^x)
         ]

If I comment out the definition of lists, the code compiles successfully. If I do not comment it out, I'm getting the following errors:

test.hs:8:21:
    Could not deduce (a ~ Int)
    from the context (Show a)
      bound by a type expected by the context: Show a => Int -> a
      at test.hs:8:11-22
      `a' is a rigid type variable bound by
          a type expected by the context: Show a => Int -> a at test.hs:8:11
    In the expression: x
    In the expression: \ x -> x
    In the expression: (1, \ x -> x)

test.hs:9:21:
    Could not deduce (a ~ [Char])
    from the context (Show a)
      bound by a type expected by the context: Show a => Int -> a
      at test.hs:9:11-27
      `a' is a rigid type variable bound by
          a type expected by the context: Show a => Int -> a at test.hs:9:11
    In the return type of a call of `show'
    In the expression: show x
    In the expression: \ x -> show x

test.hs:10:21:
    Could not deduce (a ~ Double)
    from the context (Show a)
      bound by a type expected by the context: Show a => Int -> a
      at test.hs:10:11-24
      `a' is a rigid type variable bound by
          a type expected by the context: Show a => Int -> a at test.hs:10:11
    In the first argument of `(^)', namely `c'
    In the expression: c ^ x
    In the expression: \ x -> c ^ x
Failed, modules loaded: none.

Why is this happening? Shouldn't the second example be equivalent to the first one? What is the difference between these usages of n-rank types? Is it possible at all to leave out extra ADT definition and use only simple types when I want such kind of polymorphism?

Answer 1

Your first attempt is not using existential types. Rather your

lists :: [(Int, forall a. Show a => Int -> a)]

demands that the second components can deliver an element of any showable type that I choose, not just some showable type that you choose. You're looking for

lists :: [(Int, exists a. Show a * (Int -> a))]  -- not real Haskell

but that's not what you've said. The datatype packaging method allows you to recover exists from forall by currying. You have

HRF :: forall a. Show a => (Int -> a) -> HRF

which means that to build an HRF value, you must supply a triple containing a type a, a Show dictionary for a and a function in Int -> a. That is, the HRF constructor's type effectively curries this non-type

HRF :: (exists a. Show a * (Int -> a)) -> HRF   -- not real Haskell

You might be able to avoid the datatype method by using rank-n types to Church-encode the existential

type HRF = forall x. (forall a. Show a => (Int -> a) -> x) -> x

but that's probably overkill.

Answer 2

There are two issues you have to consider regarding the handling of existential types:

• If you store "anything that can be shown," you have to store the thing that can be shown along with how to show it.
• An actual variable can only ever have one single type.

The first point is why you have to have existential type wrappers, because when you write this:

data Showable = Show a => Showable a

What actually happens is that something like this gets declared:

data Showable a = Showable (instance of Show a) a

I.e. a reference to the class instance of Show a is stored along with the value a. Without this happening, you can't have a function that unwraps a Showable, because that function wouldn't know how to show the a.

The second point is why you get some type quirkiness sometimes, and why you can't bind existential types in let bindings, for example.

---

You also have an issue with your reasoning in your code. If you have a function like forall a . Show a => (Int -> a) you get a function that, given any integer, will be able to produce any kind of showable value that the caller chooses. You probably mean exists a . Show a => (Int -> a), meaning that if the function gets an integer, it will return some type for which there exists a Show instance.

Answer 3

The examples are not equivalent. The first,

lists :: [(Int, forall a. Show a => Int -> a)]

says that each second component can produce any desired type, as long as it's an instance of Show from an Int.

The second example is modulo the type wrapper equivalent to

lists :: [(Int, exists a. Show a => Int -> a)]

i.e., each second component can produce some type belonging to Show from an Int, but you have no idea which type that function returns.

Further, the functions you put into the tuples don't satisfy the first contract:

lists = [ (1, \x -> x)
        , (2, \x -> show x)
        , (3, \x -> c^x)
        ]

\x -> x produces the same type as result that it is given as input, so here, that's Int. show always produces a String, so it's one fixed type. finally, \x -> c^x produces the same type as c has, namely Double.