How to unpack a haskell existential type?

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 . Bl开发者_如何学JAVAurb 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?

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.

You can't* specialize a type after you've hidden it away. Add some constraint or method to Blurb if you need an operation like this.

-- choose one
class (Eq a, Show a) => Blurb a where
    printBlurb :: a -> IO ()
instance Blurb Greek where
    printBlurb Alpha = putStrLn "Alpha"
...

class (Eq a, Show a) => Blurb a
data Greek deriving (Eq, Show)
...

data BlurbBox = forall a. (Blurb a, Show a) => BlurbBox a
data Greek deriving (Eq, Show)
...

*I would very much recommend against this, but if you really wanted…

{-# LANGUAGE DeriveDataTypeable #-}
import Data.Dynamic

data Greek = Alpha | Beta deriving (Eq, Typeable)
data English = Ay | Bee deriving (Eq, Typeable)

box1 :: Dynamic
box1 = toDyn Alpha

box2 :: Dynamic
box2 = toDyn Ay

main = do
    case fromDynamic box1 of
      Just Alpha -> putStrLn "Alpha"
      Just Beta -> putStrLn "Beta"
      Nothing -> case fromDynamic box1 of
        Just Ay -> putStrLn "Ay"
        Just Bee -> putStrLn "Bee"

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).

11 years later, it's time to mention singletons, another useful way of dealing with existentials! Note, no typeclasses in sight :)

data SBlurb t where
  SGreek   :: SBlurb Greek
  SEnglish :: SBlurb English

data BlurbBox where -- your original existential, with an extra singleton param
  BlurbBox :: SBlurb a -> a -> BlurbBox

data Greek   = Alpha | Beta
data English = Ay    | Bee

box1, box2 :: BlurbBox
box1 = BlurbBox SGreek Alpha
box2 = BlurbBox SEnglish Ay

main :: BlurbBox -> IO ()
main (BlurbBox s x) = case (s, x) of
  (SGreek, Alpha) -> putStrLn "Alpha"
  (SGreek, Beta)  -> putStrLn "Beta"
  (SEnglish, Ay)  -> putStrLn "Ay"
  (SEnglish, Bee) -> putStrLn "Bee"

The idea is you have a singleton packaged up inside the existential that you can also pattern match on.

For ex, you match on SGreek and it proves that x :: Greek for you; then you can do whatever you want with the greek value!