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

[Yves Parès]

> 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).

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/20120104/d16ffa7e/attachment.htm>