Re: [Haskell-cafe] Solved but strange error in type inference

Thanks Cédric for your explanations. To sum up, that's the way I understood all this, in a bit less formal way: (Could help some, I guess) Universal quantification (forall) means that the *caller *will instanciate ("fix") the type variables, and that *callee *cannot know those types. Existential quantification (through data E = forall a. E a) means that the *callee *will fix the type variables, and that the *caller *cannot know those types. Now concerning the way existential (resp. universal) in a context becomes universal (resp. existential) in the outer context: f :: forall a. a -> a means that when you're *inside *f, 'a' will have been fixed to some type *that f cannot know*, only the outer context can. f says "I can work with any type a, so give me whatever type you want". g :: (forall a. a -> a) -> Something g f = .... means the exact opposite: 'a' is universally quantified in the signature of 'f', so it is existentially quantified in that of 'g'. So it's equivalent to: g :: exists a. (a -> a) -> Something g says "I can only work with *some* specific types 'a', but as you don't know what they will be, you can but give me something that can will work with *any *type 'a'." And so on: h :: ((forall a. a -> a) -> Something) -> SomethingElse h g = ... h can also be written as follows, am I right?: h :: forall a. ((a -> a) -> Something) -> SomethingElse And to be sure: foo :: forall a. a -> (forall b. b -> a) is equivalent to: foo :: forall a b. a -> b -> a Right? And: foo :: forall a. a -> ((forall b. b) -> a) to: foo :: forall a. exists b. a -> b -> a ?? 2012/1/4 AUGER Cédric

Le Wed, 4 Jan 2012 20:13:34 +0100, Yves Parès a écrit :

...

...

f :: forall a. (forall b. b -> b) -> a -> a f id x = id x

...

is very similar to the first case, x is still universally quantified (a) and there is an existential quantification in id (b).

I don't get it. What is 'id' existentially quantified in? f calls id so f will decide what will be its type. In this case, because it's applied to 'x', id type will get instanciated to 'a -> a' (where a is rigid, because bound by f signature).

Sorry I badly expressed it.

I wanted to say that the "b" type variable in "id" is existentially quantified in the type of f.

forall a. (forall b. b -> b) -> a -> a ^ existentially quantified in the overall type but locally universally quantified in the type forall b. b -> b

It is the same things for data types.

Consider the data type of lists:

data List a = Nil | Cons a (List a)

its elimination principle is:

list_rec :: forall a b. b -> (a -> list a -> b -> b) -> List a -> b list_rec acc f l = case l of Nil -> acc Cons a l -> f a l (list_rec acc f l) (it is the type version of the induction principle: "∀ P. P Nil ⇒ (∀ x l, P l ⇒ P (Cons x l)) ⇒ ∀ l, P l" which by Curry-DeBruijn-Horward gives b -> ( b -> List a -> b -> b ) -> list a -> b you can also find an "optimized" version where "l" is removed from the recursion as its information can be stored in "P l/b"; this function is exactly "foldr" )

Now if we take a look at the elimination principle,

forall a b. b -> (a -> list a -> b -> b) -> List a -> b

contains only universally quantified variables.

Cons as a function is also universally quantified: Cons :: forall a. a -> List a -> List a

Nil as a function is also universally quantified: Nil :: forall a. List a

So that elimination and introduction are all universally quantified. (Nothing very surprising here!) =====================================================================

Now for the existential part:

data Existential = forall b. ExistIntro b

What is its elimination principle (ie. what primitive function allows us to use it for all general purpouses)?

Existential types are less easy to manipulate, since in fact they require functions which takes universally quantified functions as arguments.

existential_elim :: forall b. (forall a. a -> b) -> Existential -> b existential_elim f e = case e of ExistIntro x -> f x (∀ P. (∀ a. a ⇒ P (ExistIntro a)) ⇒ ∀ e. P e)

Here, you can see that "a" is existentially quantified (isn't it normal for a type containing existentials)!

Note also that its introduction rule: ExistIntro :: forall a. a -> Existential is also universally quantified (but with a type variable which doesn't appear in the introduced type).

Which is not to mess with:

data Universal = UnivIntro (forall a. a)

elimination principle: univ_elim :: forall b. ((forall a. a) -> b) -> Universal -> b univ_elim f u = case u of UnivIntro poly -> f poly (∀ P. (∀ (poly:∀a.a). P (UnivIntro poly)) ⇒ ∀ u. P u)

Here you can see that you don't need special syntax, and again, the elimination principle is universally quantified in both a and b. Its introduction has some existential quantification (which doesn't appear in the introduced type).

...

2012/1/4 AUGER Cédric

...

Le Wed, 4 Jan 2012 14:41:21 +0100, Yves Parès a écrit :

...

...

I expected the type of 'x' to be universally quantified, and thus can be unified with 'forall a. a' with no problem

As I get it. 'x' is not universally quantified. f is. [1] x would be universally quantified if the type of f was :

f :: (forall a. a) -> (forall a. a)

[1] Yet here I'm not sure this sentence is correct. Some heads-up from a type expert would be good.

For the type terminology (for Haskell),

notations: a Q∀ t := a universally quantified in t a Q∃ t := a existentially quantified in t a Q∀∃ t := a universally (resp. existentially) quantified in t a Q∃∀ t := a existentially (resp. universally) quantified in t

Two different names are expected to denote two different type variables. A type variable is not expected to be many times quantified (else, it would be meaningless, a way to omit this hypothesis is to think of path to quantification instead of variable name; to clarify what I mean, consider the following expression:

forall a. (forall a. a) -> a

we cannot tell what "a is existentially quantified" means, since we have two a's; but if we rename them into

forall a. (forall b. b) -> a or forall b. (forall a. a) -> b

, the meaning is clear; in the following, I expect to always be in a place where it is clear.)

rules: (1) ⊤ ⇒ a Q∀ forall a. t (2)b Q∀∃ t ⇒ b Q∀∃ forall a. t (3)a Q∀∃ u ⇒ a Q∀∃ t -> u (in fact it is the same rule as above, since "->" is an non binding forall in type theory) (4)a Q∀∃ t ⇒ a Q∃∀ t -> u

So in this context, we cannot say that 'x' is universally or existentially quantified, but that the 'type of x' is universally or existentially quantified 'in' some type (assuming that the type of x is a type variable).

so:

a Q∃ (forall a. a -> a) -> forall b. b -> b since (4) and "a Q∀ forall a. a -> a" due to (1)

and

b Q∀ (forall a. a -> a) -> forall b. b -> b since (3) and "b Q∀ forall b. b -> b" due to (1)

The quick way to tell is count the number of unmatched opening parenthesis before the quantifying forall (assuming you don't put needless parenthesis) if it is even, you are universally quantified, if it is odd, you are existentially quantified.

So in:

f :: (forall a. a -> a) -> forall b. b -> b f id x = id x

the type of 'x' (b) is universally quantified in the type of f, and the type of 'id' contains an existential quantification in the type of f (a).

In:

f :: forall a. (a -> a) -> a -> a f id x = id x

the type of 'x' (a) is universally quantified in the type of f; there is no existential quantification.

f :: forall a. (forall b. b -> b) -> a -> a f id x = id x

is very similar to the first case, x is still universally quantified (a) and there is an existential quantification in id (b).

I guess that the only difference is that when you do a "f id" in the last case, you might get an error as the program needs to know the "a" type before applying "id" (of course if there is some use later in the same function, then the type can be inferred)

Hope that I didn't write wrong things, and if so that you can tell now for sure if a type is universally or existentially quantified.