Why aren't there existentially quantified type variables in GHC Haskell

Question

There are universally quantified type variables, and there are existentially quantified data types. However, despite that people give pseudocode of the form exists a. Int -> a to help explain concepts sometimes, it doesn't seem like a compiler extension that there's any real interest in. Is this just a "there isn't much value in adding this" kind of thing (because it does seem valuable to me), or is there a problem like undecidability that's makes it truly impossible.

EDIT: I've marked viorior's answer as correct because it seems like it is probably the actual reason why this was not included. I'd like to add some additional commentary though just in case anyone would want to help clarify this more.

As requested in the comments, I'll give an example of why I would consider this useful. Suppose we have a data type as follows:

data Person a = Person
  { age: Int
  , height: Double
  , weight: Int
  , name: a
  }

So we choose parameterize over a, which is a naming convention (I know that it probably makes more sense in this example to make a NamingConvention ADT with appropriate data constructors for the American "first,middle,last", the hispanic "name,paternal name,maternal name", etc. But for now, just go with this).

So, there are several functions we see that basically ignore the type that Person is parameterized over. Examples would be

age :: Person a -> Int
height :: Person a -> Double
weight :: Person a -> Int

And any function built on top of these could similarly ignore the a type. For example:

atRiskForDiabetes :: Person a -> Bool
atRiskForDiabetes p = age p + weight p > 200
--Clearly, I am not actually a doctor

Now, if we have a heterogeneous list of people (of type [exists a. Person a]), we would like to be able to map some of our functions over the list. Of course, there are some useless ways to map:

heteroList :: [exists a. Person a]
heteroList = [Person 20 30.0 170 "Bob Jones", Person 50 32.0 140 3451115332]
extractedNames = map name heteroList

In this example, extractedNames is of course useless because it has type [exists a. a]. However, if we use our other functions:

totalWeight :: [exists a. Person a] -> Int
totalWeight = sum . map age

numberAtRisk :: [exists a. Person a] -> Int
numberAtRisk = length . filter id . map atRiskForDiabetes

Now, we have something useful that operates over a heterogeneous collection (And, we didn't even involve typeclasses). Notice that we were able to reuse our existing functions. Using an existential data type would go as follows:

data SomePerson = forall a. SomePerson (Person a) --fixed, thanks viorior

But now, how can we use age and atRiskForDiabetes? We can't. I think that you would have to do something like this:

someAge :: SomePerson -> Int
someAge (SomePerson p) = age p

Which is really lame because you have to rewrite all of your combinators for a new type. It gets even worse if you want to do this with a data type that's parameterized over several type variables. Imagine this:

somewhatHeteroPipeList :: forall a b. [exists c d. Pipe a b c d]

I won't explain this line of thought any further, but just notice that you'd be rewriting a lot of combinators to do anything like this using just existential data types.

That being said, I hope I've give a mildly convincing use that this could be useful. If it doesn't seem useful (or if the example seems too contrived), feel free to let me know. Also, since I am firstly a programmer and have no training in type theory, it's a little difficult for me to see how to use Skolem's theorum (as posted by viorior) here. If anyone could show me how to apply it to the Person a example I gave, I would be very grateful. Thanks.

Can you provide an example of how it would be useful? I'm actually curious if there is a good use case in Haskell. It's also possible that what you're wanting that feature for could be solved using another technique, but that's hard to say without anything concrete. — bheklilr
Does data Exists t = forall a. Exists (t a) work? In your case you'd write foo :: Exists ((->) Int). We do have existentials in this sense, just bounded by a data constructor — Daniel Gratzer
You have to wrap it in a data type, which is inconvenient, but then existential types are not very common. — augustss
UHC has an extension for writing existential types, but you can't put a constraint on the existential type, making it nearly useless. — Carl
You have an error: someAge :: SomePerson -> Int someAge p = age p - right one — viorior

viorior viorior · Accepted Answer · 2014-05-30T08:33:17

It is unnecessary.

By Skolem's Theorem we could convert existential quantifier into universal quantifier with higher rank types:

(∃b. F(b)) -> Int   <===>  ∀b. (F(b) -> Int)

Every existentially quantified type of rank n+1 can be encoded as a universally quantified type of rank n

Why aren't there existentially quantified type variables in GHC Haskell

2 Answers