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

[Yves Parès]

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 <sedrikov at gmail.com>

> 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.
> > >
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/haskell-cafe/attachments/20120105/fabf6b10/attachment.htm>