Type Pattern-Matching for Existential Types

[Fergus Henderson]

On 31-Jan-2001, Lennart Augustsson <lennart@mail.augustsson.net> wrote:
> 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).

But you can achieve a similar effect to the example above using the
Hugs/ghc `Dynamic' type.  Values of type Dynamic do carry around the
type of encapsulated value.

	data Any = forall a. typeable a => Any a

	get :: Any -> Maybe Char
	get (Any x) = fromDynamic (toDyn x)

This works as expected:

	Main> get (Any 'c')
	Just 'c'
	Main> get (Any "c")
	Nothing
	Main> get (Any 42)
	ERROR: Unresolved overloading
	*** Type       : (Typeable a, Num a) => Maybe Char
	*** Expression : get (Any 42)

	Main> get (Any (42 :: Int))
	Nothing

-- 
Fergus Henderson <fjh@cs.mu.oz.au>  |  "I have always known that the pursuit
                                    |  of excellence is a lethal habit"
WWW: <http://www.cs.mu.oz.au/~fjh>  |     -- the last words of T. S. Garp.