Why don't existential types have pattern matching?

1
votes

Even without extension ExistentialQuantification, Haskell supports some existential types, via the type isomorphism, for any typeclass C,

(forall a. C a => (a -> b))  ~  ((exists a. C a => a) -> b)

So a function f :: C a => a -> b expects an argument x of type exists a. C a. But Haskell doesn't allow to pattern match x against some types of C (finishing by a wild match _, because type classes are usually infinite).

This is strange, because existential types are generalized sum types. Haskell does support finite sum types with the data keyword and allows pattern matching for them. In languages such as C++, Java and C#, existential types are interfaces and they support pattern matching with keywords such as dynamic_cast or instanceof.

Is there a reason why Haskell didn't implement pattern matching for functions such as f above ?

2
haskell
If I understand you correctly, you want to pattern match on the type. This is impossible, because there is no run-time type information. For normal sum types, the information about the constructor having been used is retained at run-time. For existentials, there is nothing. If you want something like that, you can use a GADT as a witness, or use Typeable. – kosmikus
@kosmikus Yes, I want to pattern match on the type. I understand it is impossible the way GHC was implemented, I'm asking why GHC was implemented like this. Can you give an example of an infinite sum type with pattern matching using GADTs ? It's not clear to me how to do it. – V. Semeria
Why would GHC be implemented any other way? Pattern matching on types just leads to bad practises; the set of available types being unlimited, you can never really have full coverage without catch-all cases; and having the type information at runtime would generally be a significant performance overhead. – leftaroundabout
Shouldn't the iso be (forall a. (C a => a) -> b) ~ ((exists a. C a => a) -> b)? – gallais

2 Answers

8
votes

Haskell was designed so to allow a type-erasing implementation. We can still run Haskell without carrying all the type-level information at runtime. This allows implementations to reduce the memory footprint.

Note that the programmer can still choose to keep type information around at runtime by adding Typeable a constraints. cast can then be used to pattern match on types.

Further, the inability of performing pattern matching on types at runtime is important to guarantee parametricity / free theorems. For instance, if we have a polymorphic function

f :: forall a. a -> a

we are guaranteed that f is the identity (or fails to terminate). This is because any such f must be a natural transformation, and no other options but the identity are available. That would not be true if we could write

f x = if a==Int then x+1 else x

Something like that can indeed be written if we add Typeable a.

Similarly, g :: a->a->a must be a projection, and h :: [a]->[a] can not send [True] to [False,True]. Further, if h [1,2]=[2,2,1] then necessarily h "ab" = "bba". By naturality, these function must work "uniformly" over all the types a.

2
votes

If you want to pattern match on types, that is impossible, because

  1. There are an infinite number of types to match against, so your patterns can never be exhaustive.

  2. As an implementation detail, GHC erases all type information at compile-time, so there's no way to implement this anyway. (Which is probably due to point #1.)

You mention that OO languages typically have something like an instanceof operator. You can do this in Haskell with the Typeable class. If a type is an instance of Typeable, you can "cast" it to the Dynamic type using toDyn. You can then later try to cast it back using fromDynamic, which returns a Maybe. (Or fromDyn, which returns a default value.) So the Dynamic type is similar to Java's Object; it can be anything. Typically that's not really restrictive enough, and generally you tend not to see this kind of programming in Haskell.

You can also use GADTs to represent a finite set of types which you can then pattern match against just fine. Or regular data structures, for that matter.