Type Pattern-Matching for Existential Types

[Tom Pledger]

Lennart Augustsson writes:
 [...]
 > Slightly more interesting might be
 > data Foo = forall a . Foo a (a -> Int)
 > 
 > Now you can at least apply the function to the value after pattern
 > matching.  You don't have to carry any types around, because the
 > type system ensures that you don't misuse the value.

Hi.

In that particular example, I'd be more inclined to use the
existential properties of lazy evaluation:

    packFoo x f = Foo x f
    -- The actual type of x is buried in the existential

    data Bar = Bar Int
    packBar x f = Bar (f x)
    -- The actual type of x is buried in the (f x) suspension

Of course, when there are more usable things which can be retrieved
from the type, an explicit existential is more appealing:

    data Foo' = forall a . Ord a => Foo' [a]
    packFoo' xs = Foo' xs
    -- The actual type of xs is buried in the existential

    data Bar' = Bar' [[Ordering]]
    packBar' xs = Bar' oss where
        oss = [[compare x1 x2 | x2 <- xs] | x1 <- xs]
    -- The actual type of xs is buried in the oss suspension, which
    -- is rather bloated

Regards,
Tom