Type Pattern-Matching for Existential Types
Tom Pledger
Tom.Pledger@peace.com
Thu, 1 Feb 2001 10:31:56 +1300
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