Type Pattern-Matching for Existential Types
Wed, 31 Jan 2001 18:11:13 +1100
On 31-Jan-2001, Lennart Augustsson <firstname.lastname@example.org> 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')
Main> get (Any "c")
Main> get (Any 42)
ERROR: Unresolved overloading
*** Type : (Typeable a, Num a) => Maybe Char
*** Expression : get (Any 42)
Main> get (Any (42 :: Int))
Fergus Henderson <email@example.com> | "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.