Type Pattern-Matching for Existential Types

[Lennart Augustsson]

Ashley Yakeley wrote:

> At 2001-01-30 22:16, Lennart Augustsson wrote:
>
> >It has large and horrible implications.  To do dynamic type tests you need
> >to carry around the types at runtime.  This is not something that Haskell
> >does (at least you don't have to).
>
> Hmm. In this:
>
> --
> data Any = forall a. Any a
>
> a1 = Any 3
> a2 = Any 'p'
> --
>
> ...are you saying that a1 and a2 do not have to carry types at runtime?

That's right.
Your data type is actually degenerate.  There is nothing you can do what
so ever with a value of type Any (except pass it around).

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.

    -- Lennart