How to unpack a haskell existential type?

Question

Hello all. Experimenting with existential types. Seems to be a great way to get some type flexibility.

I'm hitting a problem with unboxing an existential type after I've wrapped it up. My code as follows:

{-# LANGUAGE ExistentialQuantification #-}

class Eq a => Blurb a
data BlurbBox = forall a . Blurb a => BlurbBox a

data Greek = Alpha | Beta deriving Eq
instance Blurb Greek

data English = Ay | Bee deriving Eq
instance Blurb English

box1 :: BlurbBox
box1 = BlurbBox Alpha

box2 :: BlurbBox
box2 = BlurbBox Ay

main = do
    case box1 of
        BlurbBox Alpha -> putStrLn "Alpha"
        BlurbBox Beta -> putStrLn "Beta"
        BlurbBox Ay -> putStrLn "Ay"
        BlurbBox Bee -> putStrLn "Bee"

This code compiles up to main, then complains about the type of BlurbBox Alpha. How do I go about unboxing/unpacking an existential type?

Answer 1

As far as I know you can't do that. The whole point of existential types is to hide a type, so you can access all "instances" uniformly (kinda like dynamic dispatch of subclass methods in Java and other object-oriented languages).

So, in your example, your "interface" is BlurbBox and you would use it to apply some method uniformly to different BlurbBoxes, without worrying about what the internal type a is (e.g. if Blurb subclasses Show, then you can have a [BlurbBox] and print each element of the list without having to know the exact internal type of each BlurbBox in the list).

Answer 2

Indeed, existential types can't be unpacked, because their whole point is that the code expecting an existential type must work absolutely the same way (in the sense of parametric polymorphism) regardless of with which exact type the existential type variable was instantiated.

You can understand that better by understanding that

data BlurbBox = forall a . Blurb a => BlurbBox a

gets translated to

type BlurbBox = forall b . (forall a . Blurb a => a -> b) -> b

that is, BlurbBox is something that, given a polymorphic function that works for absolutely all Blurbs, can be used to produce the result of applying that function to some (unknown) blurb.

Thus, similarly to how you can't write a function of type f :: a -> Int and have f String = 5 and f Bool = 3, you can't dispatch on the type of 'a' in a BlurbBox.

You might have a look at the chapter in TAPL on existential types. It describes the translation that I've provided.