Type Pattern-Matching for Existential Types

At 2001-01-30 19:52, Fergus Henderson wrote:
On 30-Jan-2001, Ashley Yakeley
wrote: At 2001-01-30 02:37, Fergus Henderson wrote:
class BaseClass s where downcast_to_derived :: s -> Maybe Derived
Exactly what I was trying to avoid, since now every base class needs to know about every derived class. This isn't really a practical way to build an extensible type hierarchy.
Right.
I don't know of any way to do that in Hugs/ghc without the problem that you mention. Really it needs language support, I think. (I have no idea if you can do it in O'Haskell.)
It can't be done in O'Haskell either... Given that we have existential types, it would be nice to have a pattern-matching mechanism to get at the inside value. Something like... -- 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? -- Ashley Yakeley, Seattle WA

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

On 31-Jan-2001, Lennart Augustsson
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

Lennart Augustsson 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).
-- Lennart
It can also be questioned from a software engineering standpoint. Much of the purpose with existential types is to provide information hiding; that is, the user of an existentially quantified type is not supposed to know its concrete representation. The merits of an information hiding dicipline is probably no news to anybody on this list. However, this whole idea gets forfeited if it's possible to look behind the abstraction barrier by pattern-matching on the representation. Allowing that is a little like saying "this document is secret, but if you're able to guess its contents, I'll gladly confirm it to you!". The same argument also applies to information hiding achieved by coercing a record to a supertype. This doesn't mean that I can't see the benefit of dynamic type checking for certain problems. But it should be brought in mind that such a feature is a separate issue, not to be confused with existential types or subtyping. And as Lennart says, it's a feature with large (and horrible!) implications to the implementation of a language. -- Johan

On 30-Jan-2001, Johan Nordlander
It can also be questioned from a software engineering standpoint. Much of the purpose with existential types is to provide information hiding; that is, the user of an existentially quantified type is not supposed to know its concrete representation. The merits of an information hiding dicipline is probably no news to anybody on this list.
However, this whole idea gets forfeited if it's possible to look behind the abstraction barrier by pattern-matching on the representation.
That's a good argument for dynamic type casts not being available by default. However, there are certainly times when the designer of an interface wants some degree of abstraction, but does not want to prohibit dynamic type class casts. The language should permit the designer to express that intention, e.g. using the `Typeable' type class constraint.
Allowing that is a little like saying "this document is secret, but if you're able to guess its contents, I'll gladly confirm it to you!".
Yes. But there are times when something like that is indeed what you want to say. The language should permit you to say it. The specific language that you have chosen has some connotations which imply that this would be undesirable. But saying "this data structure is abstract, but you are permitted to downcast it" is really not a bad thing to say. There's different levels of secrecy, and not everything needs to be completely secret; for some things it's much better to allow downcasting, so long as you are explicit about it.
This doesn't mean that I can't see the benefit of dynamic type checking for certain problems. But it should be brought in mind that such a feature is a separate issue, not to be confused with existential types or subtyping.
OK, perhaps we are in agreement after all.
--
Fergus Henderson
participants (4)
-
Ashley Yakeley
-
Fergus Henderson
-
Johan Nordlander
-
Lennart Augustsson