Thanks Cédric for your explanations.<br>To sum up, that's the way I understood all this, in a bit less formal way:<br>(Could help some, I guess)<br><br>Universal quantification (forall) means that the <b>caller </b>will instanciate ("fix") the type variables, and that <b>callee </b>cannot know those types.<br>
<br>Existential quantification (through data E = forall a. E a) means that the <b>callee </b>will fix the type variables, and that the <b>caller </b>cannot know those types.<br><br>Now concerning the way existential (resp. universal) in a context becomes universal (resp. existential) in the outer context:<br>
<br>f :: forall a. a -> a<br>means that when you're <i>inside </i>f, 'a' will have been fixed to some type <i>that f cannot know</i>, only the outer context can.<br>f says "I can work with any type a, so give me whatever type you want".<br>
<br>g :: (forall a. a -> a) -> Something<br>g f = ....<br>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:<br>
g :: exists a. (a -> a) -> Something<br>g says "I can only work with <b>some</b> specific types 'a', but as you don't know what they will be, you can but give me something that can will work with <b>any </b>type 'a'."<br>
<br>And so on:<br>h :: ((forall a. a -> a) -> Something) -> SomethingElse<br>h g = ...<br>h can also be written as follows, am I right?:<br>h :: forall a. ((a -> a) -> Something) -> SomethingElse<br><br>
And to be sure:<br>foo :: forall a. a -> (forall b. b -> a)<br>is equivalent to:<br>foo :: forall a b. a -> b -> a<br>Right?<br><br>And:<br>foo :: forall a. a -> ((forall b. b) -> a)<br>to:<br>foo :: forall a. exists b. a -> b -> a<br>
??<br><br><div class="gmail_quote">2012/1/4 AUGER Cédric <span dir="ltr"><<a href="mailto:sedrikov@gmail.com">sedrikov@gmail.com</a>></span><br><blockquote class="gmail_quote" style="margin:0pt 0pt 0pt 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">
Le Wed, 4 Jan 2012 20:13:34 +0100,<br>
<div class="im">Yves Parès <<a href="mailto:limestrael@gmail.com">limestrael@gmail.com</a>> a écrit :<br>
<br>
</div><div class="im">> > f :: forall a. (forall b. b -> b) -> a -> a<br>
> > f id x = id x<br>
><br>
> > is very similar to the first case, x is still universally<br>
> > quantified (a) and there is an existential quantification in id (b).<br>
><br>
> I don't get it. What is 'id' existentially quantified in?<br>
> f calls id so f will decide what will be its type. In this case,<br>
> because it's applied to 'x', id type will get instanciated to 'a -><br>
> a' (where a is rigid, because bound by f signature).<br>
<br>
</div>Sorry I badly expressed it.<br>
<br>
I wanted to say that the "b" type variable in "id" is existentially<br>
quantified in the type of f.<br>
<div class="im"><br>
forall a. (forall b. b -> b) -> a -> a<br>
</div> ^<br>
existentially quantified in the overall type<br>
but locally universally quantified in the type forall b. b -> b<br>
<br>
It is the same things for data types.<br>
<br>
Consider the data type of lists:<br>
<br>
data List a = Nil<br>
| Cons a (List a)<br>
<br>
its elimination principle is:<br>
<br>
list_rec :: forall a b. b -> (a -> list a -> b -> b) -> List a -> b<br>
list_rec acc f l = case l of<br>
Nil -> acc<br>
Cons a l -> f a l (list_rec acc f l)<br>
(it is the type version of the induction principle:<br>
"∀ P. P Nil ⇒ (∀ x l, P l ⇒ P (Cons x l)) ⇒ ∀ l, P l"<br>
which by Curry-DeBruijn-Horward gives<br>
b -> ( b -> List a -> b -> b ) -> list a -> b<br>
you can also find an "optimized" version where "l" is removed from<br>
the recursion as its information can be stored in "P l/b";<br>
this function is exactly "foldr"<br>
)<br>
<br>
Now if we take a look at the elimination principle,<br>
<br>
forall a b. b -> (a -> list a -> b -> b) -> List a -> b<br>
<br>
contains only universally quantified variables.<br>
<br>
Cons as a function is also universally quantified:<br>
Cons :: forall a. a -> List a -> List a<br>
<br>
Nil as a function is also universally quantified:<br>
Nil :: forall a. List a<br>
<br>
So that elimination and introduction are all universally quantified.<br>
(Nothing very surprising here!)<br>
=====================================================================<br>
<br>
Now for the existential part:<br>
<br>
data Existential = forall b. ExistIntro b<br>
<br>
What is its elimination principle (ie. what primitive function allows<br>
us to use it for all general purpouses)?<br>
<br>
Existential types are less easy to manipulate, since in fact they<br>
require functions which takes universally quantified functions as<br>
arguments.<br>
<br>
existential_elim :: forall b. (forall a. a -> b) -> Existential -> b<br>
existential_elim f e = case e of<br>
ExistIntro x -> f x<br>
(∀ P. (∀ a. a ⇒ P (ExistIntro a)) ⇒ ∀ e. P e)<br>
<br>
Here, you can see that "a" is existentially quantified (isn't it<br>
normal for a type containing existentials)!<br>
<br>
Note also that its introduction rule:<br>
ExistIntro :: forall a. a -> Existential<br>
is also universally quantified (but with a type variable which doesn't<br>
appear in the introduced type).<br>
<br>
Which is not to mess with:<br>
<br>
data Universal = UnivIntro (forall a. a)<br>
<br>
elimination principle:<br>
univ_elim :: forall b. ((forall a. a) -> b) -> Universal -> b<br>
univ_elim f u = case u of<br>
UnivIntro poly -> f poly<br>
(∀ P. (∀ (poly:∀a.a). P (UnivIntro poly)) ⇒ ∀ u. P u)<br>
<br>
Here you can see that you don't need special syntax, and again, the<br>
elimination principle is universally quantified in both a and b.<br>
Its introduction has some existential quantification (which doesn't<br>
appear in the introduced type).<br>
<div class="HOEnZb"><div class="h5"><br>
><br>
> 2012/1/4 AUGER Cédric <<a href="mailto:sedrikov@gmail.com">sedrikov@gmail.com</a>><br>
><br>
> > Le Wed, 4 Jan 2012 14:41:21 +0100,<br>
> > Yves Parès <<a href="mailto:limestrael@gmail.com">limestrael@gmail.com</a>> a écrit :<br>
> ><br>
> > > > I expected the type of 'x' to be universally quantified, and<br>
> > > > thus can be unified with 'forall a. a' with no problem<br>
> > ><br>
> > > As I get it. 'x' is not universally quantified. f is. [1]<br>
> > > x would be universally quantified if the type of f was :<br>
> > ><br>
> > > f :: (forall a. a) -> (forall a. a)<br>
> > ><br>
> > > [1] Yet here I'm not sure this sentence is correct. Some heads-up<br>
> > > from a type expert would be good.<br>
> > ><br>
> ><br>
> > For the type terminology (for Haskell),<br>
> ><br>
> > notations:<br>
> > a Q∀ t := a universally quantified in t<br>
> > a Q∃ t := a existentially quantified in t<br>
> > a Q∀∃ t := a universally (resp. existentially) quantified in t<br>
> > a Q∃∀ t := a existentially (resp. universally) quantified in t<br>
> ><br>
> > Two different names are expected to denote two different type<br>
> > variables. A type variable is not expected to be many times<br>
> > quantified (else, it would be meaningless, a way to omit this<br>
> > hypothesis is to think of path to quantification instead of<br>
> > variable name; to clarify what I mean, consider the following<br>
> > expression:<br>
> ><br>
> > forall a. (forall a. a) -> a<br>
> ><br>
> > we cannot tell what "a is existentially quantified" means, since we<br>
> > have two a's; but if we rename them into<br>
> ><br>
> > forall a. (forall b. b) -> a<br>
> > or<br>
> > forall b. (forall a. a) -> b<br>
> ><br>
> > , the meaning is clear; in the following, I expect to always be in a<br>
> > place where it is clear.)<br>
> ><br>
> > rules:<br>
> > (1) ⊤ ⇒ a Q∀ forall a. t<br>
> > (2)b Q∀∃ t ⇒ b Q∀∃ forall a. t<br>
> > (3)a Q∀∃ u ⇒ a Q∀∃ t -> u (in fact it is the same rule as above,<br>
> > since "->" is an non binding forall in<br>
> > type theory)<br>
> > (4)a Q∀∃ t ⇒ a Q∃∀ t -> u<br>
> ><br>
> > So in this context, we cannot say that 'x' is universally or<br>
> > existentially quantified, but that the 'type of x' is universally or<br>
> > existentially quantified 'in' some type (assuming that the type of x<br>
> > is a type variable).<br>
> ><br>
> > so:<br>
> ><br>
> > a Q∃ (forall a. a -> a) -> forall b. b -> b<br>
> > since (4) and "a Q∀ forall a. a -> a" due to (1)<br>
> ><br>
> > and<br>
> ><br>
> > b Q∀ (forall a. a -> a) -> forall b. b -> b<br>
> > since (3) and "b Q∀ forall b. b -> b" due to (1)<br>
> ><br>
> > The quick way to tell is count the number of unmatched opening<br>
> > parenthesis before the quantifying forall (assuming you don't put<br>
> > needless parenthesis) if it is even, you are universally<br>
> > quantified, if it is odd, you are existentially quantified.<br>
> ><br>
> > So in:<br>
> ><br>
> > f :: (forall a. a -> a) -> forall b. b -> b<br>
> > f id x = id x<br>
> ><br>
> > the type of 'x' (b) is universally quantified in the type of f,<br>
> > and the type of 'id' contains an existential quantification in the<br>
> > type of f (a).<br>
> ><br>
> > In:<br>
> ><br>
> > f :: forall a. (a -> a) -> a -> a<br>
> > f id x = id x<br>
> ><br>
> > the type of 'x' (a) is universally quantified in the type of f;<br>
> > there is no existential quantification.<br>
> ><br>
> > f :: forall a. (forall b. b -> b) -> a -> a<br>
> > f id x = id x<br>
> ><br>
> > is very similar to the first case, x is still universally<br>
> > quantified (a) and there is an existential quantification in id (b).<br>
> ><br>
> > I guess that the only difference is that when you do a<br>
> > "f id" in the last case, you might get an error as the program<br>
> > needs to know the "a" type before applying "id" (of course if there<br>
> > is some use later in the same function, then the type can be<br>
> > inferred)<br>
> ><br>
> > Hope that I didn't write wrong things, and if so that you can tell<br>
> > now for sure if a type is universally or existentially quantified.<br>
> ><br>
<br>
</div></div></blockquote></div><br>