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

[AUGER Cédric]

Le Wed, 4 Jan 2012 20:13:34 +0100,
Yves Parès <limestrael at gmail.com> 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 <sedrikov at gmail.com>
> 
> > Le Wed, 4 Jan 2012 14:41:21 +0100,
> > Yves Parès <limestrael at gmail.com> 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.
> >