> 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 <sedri...@gmail.com> > Le Wed, 4 Jan 2012 14:41:21 +0100, > Yves Parès <limestr...@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. >
_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe