Type Pattern-Matching for Existential Types

Lennart Augustsson lennart@mail.augustsson.net
Wed, 31 Jan 2001 01:16:30 -0500


Ashley Yakeley wrote:

> data Any = forall a. Any a
>
> get :: Any -> Maybe Char
> get (Any (c::Char)) = Just c -- bad
> get _ = Nothing
> --
>
> ...but as it stands, this is not legal Haskell, according to Hugs:
>
> ERROR "test.hs" (line 4): Type error in application
> *** Expression     : Any c
> *** Term           : c
> *** Type           : Char
> *** Does not match : _0
> *** Because        : cannot instantiate Skolem constant
>
> This, of course, is because the '::' syntax is for static typing. It
> can't be used as a dynamic pattern-test.
>
> Question: how big of a change would it be to add this kind of pattern
> matching? Is this a small issue, or does it have large and horrible
> implications?

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

    -- Lennart