List of existentially quantified values in Haskell

Question

I'm wondering why this piece of code doesn't type-check:

{-# LANGUAGE ScopedTypeVariables, Rank2Types, RankNTypes #-}
{-# OPTIONS -fglasgow-exts #-}

module Main where

foo :: [forall a. a]
foo = [1]

ghc complains:

Could not deduce (Num a) from the context ()
  arising from the literal `1' at exist5.hs:7:7

Given that:

Prelude> :t 1
1 :: (Num t) => t
Prelude> 

it seems that the (Num t) context can't match the () context of arg. The point I can't understand is that since () is more general than (Num t), the latter should and inclusion of the former. Has this anything to do with lack of Haskell support for sub-typing?

Thank you for any comment on this.

Answer 1

You're not using existential quantification here. You're using rank N types.

Here [forall a. a] means that every element must have every possible type (not any, every). So [undefined, undefined] would be a valid list of that type and that's basically it.

To expand on that a bit: if a list has type [forall a. a] that means that all the elements have type forall a. a. That means that any function that takes any kind of argument, can take an element of that list as argument. This is no longer true if you put in an element which has a more specific type than forall a. a, so you can't.

To get a list which can contain any type, you need to define your own list type with existential quantification. Like so:

data MyList = Nil | forall a. Cons a MyList
foo :: MyList
foo = Cons 1 Nil

Of course unless you restrain element types to at least instantiate Show, you can't do anything with a list of that type.

Answer 2

First, your example doesn't even get that far with me for the current GHC, because you need to enable ImpredecativeTypes as well. Doing so results in a warning that ImpredicativeTypes will be simplified or removed in the next GHC. So we're not in good territory here. Nonetheless, adding the proper Num constraint (foo :: [forall a. Num a => a]) does allow your example to compile.

Let's leave aside impredicative types and look at a simpler example:

data Foo = Foo (forall a. a)
foo = Foo 1

This also doesn't compile with the error Could not deduce (Num a) from the context ().

Why? Well, the type promises that you're going to give the Foo constructor something with the quality that for any type a, it produces an a. The only thing that satisfies this is bottom. An integer literal, on the other hand, promises that for any type a that is of class Num it produces an a. So the types are clearly incompatible. We can however pull the forall a bit further out, to get what you probably want:

data Foo = forall a. Foo a
foo = Foo 1

So that compiles. But what can we do with it? Well, let's try to define an extractor function:

unFoo (Foo x) = x

Oops! Quantified type variable 'a' escapes. So we can define that, but we can't do much interesting with it. If we gave a class context, then we could at least use some of the class functions on it.

There is a time and place for existentials, including ones without class context, but its fairly rare, especially when you're getting started. When you do end up using them, often it will be in the context of GADTs, which are a superset of existential types, but in which the way that existentials arise feels quite natural.

Answer 3

Because the declaration [forall a. a] is (in meaning) the equivalent of saying, "I have a list, and if you (i.e. the computer) pick a type, I guarantee that the elements of said list will be that type."

The compiler is "calling your bluff", so-to-speak, by complaining, "I 'know' that if you give me a 1, that its type is in the Num class, but you said that I could pick any type I wanted to for that list."

Basically, you're trying to use the value of a universal type as if it were the type of a universal value. Those aren't the same thing, though.