universal quantification is to type instantiations as existential quantification is to what
Hi, If I have a universally quantified type mapInt :: forall a. (Int -> a) -> [Int] -> [a] I can instantiate that function over a type and get a beta-reduced version of the type mapInt [String] :: (Int -> String) -> [Int] -> [String] (I'm borrowing syntax from Pierce here since I don't think Haskell allows me to explicitly pass in a type to a function.) This makes sense to me. The universal quantifier is basically a lambda, but it works at the type level instead of the value level. My question is... what is the analog to an existential type? mapInt :: exists a. (Int -> a) -> [Int] -> [a] (I don't think this is valid syntax either. I understand that I can rewrite this using foralls and a new type variable, doing something that looks like double negation, but the point of my question is to get an intuition for what exactly the universal quantifier means in the context of function application... if this even makes sense.) In particular: 1. If I can "instantiate" variables in a universal quantifier, what is the corresponding word for variables in an existential quantifier? 2. If type instantiation of a universally quantified variable is beta-reduction, what happens when existentially quantified variables are [insert answer to question 1]? 3. Is there any analogue to existential quantifiers in the value world? "Forall" is to "lambda" as "exists" is to what? Also (separate question), is the following statement true? forall T :: * -> *. (forall a. T a) -> (exists a. T a) If so, what does the implementation look like? (What function inhabits it, if it is interpreted as a type?) Josh "Ua" Ball
The existential is a pair where one component is a type, and the type of the
second component depends on the value (i.e., which type went in the first
component) of the first. It's often called a sigma type when you have full
dependent types.
So your exists a. (Int -> a) -> [Int] -> [a] type might hypothetically be
represented as (assuming you write an instance for Bool):
(*, (\a -> (Int -> a) -> [Int] -> [a])) -- the type, where * is the kind of
types
(Bool,
Hi,
If I have a universally quantified type
mapInt :: forall a. (Int -> a) -> [Int] -> [a]
I can instantiate that function over a type and get a beta-reduced version of the type
mapInt [String] :: (Int -> String) -> [Int] -> [String]
(I'm borrowing syntax from Pierce here since I don't think Haskell allows me to explicitly pass in a type to a function.)
This makes sense to me. The universal quantifier is basically a lambda, but it works at the type level instead of the value level.
My question is... what is the analog to an existential type?
mapInt :: exists a. (Int -> a) -> [Int] -> [a]
(I don't think this is valid syntax either. I understand that I can rewrite this using foralls and a new type variable, doing something that looks like double negation, but the point of my question is to get an intuition for what exactly the universal quantifier means in the context of function application... if this even makes sense.)
In particular:
1. If I can "instantiate" variables in a universal quantifier, what is the corresponding word for variables in an existential quantifier? 2. If type instantiation of a universally quantified variable is beta-reduction, what happens when existentially quantified variables are [insert answer to question 1]? 3. Is there any analogue to existential quantifiers in the value world? "Forall" is to "lambda" as "exists" is to what?
Also (separate question), is the following statement true?
forall T :: * -> *. (forall a. T a) -> (exists a. T a)
If so, what does the implementation look like? (What function inhabits it, if it is interpreted as a type?)
Josh "Ua" Ball _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Daniel Peebles wrote:
The existential is a pair where one component is a type, and the type of the second component depends on the value (i.e., which type went in the first component) of the first. It's often called a sigma type when you have full dependent types.
Not quite. Strong-sigma is a dependent pair where you can project both elements. Weak-sigma is a dependent pair where you can only project the first element (because the second is erased). Existentials are dependent pairs where you can only project the second component (because the first is erased). Strong-sigma is often just called "sigma" because it's the assumed default case. Weak-sigma is used for refinement types, where the second component is a proof that some property holds for the first element. Existentials are special because they don't allow you to recover the witness. fst :: (A :: *) -> (B :: A -> *) -> (p :: StrongSig A B) -> A snd :: (A :: *) -> (B :: A -> *) -> (p :: StrongSig A B) -> B (fst p) elim :: (A :: *) -> (B :: A -> *) -> (_ :: Exists A B) -> (C :: *) -> (_ :: (a :: A) -> B a -> C) -> C Notice how we only get the Church-encoding for existential elimination and how 'a' cannot appear in 'C'. Whereas for 'snd' we explicitly allow 'fst p' to escape. -- Live well, ~wren
On Thursday 12 August 2010 7:59:09 pm wren ng thornton wrote:
Not quite. Strong-sigma is a dependent pair where you can project both elements. Weak-sigma is a dependent pair where you can only project the first element (because the second is erased). Existentials are dependent pairs where you can only project the second component (because the first is erased).
elim :: (A :: *) -> (B :: A -> *) -> (_ :: Exists A B) -> (C :: *) -> (_ :: (a :: A) -> B a -> C) -> C
Notice how we only get the Church-encoding for existential elimination and how 'a' cannot appear in 'C'. Whereas for 'snd' we explicitly allow 'fst p' to escape.
This is how it's usually explained, but note that this eliminator type is not strict enough to guarantee that it's safe to erase the first component. We can still write: fst'ex :: (A :: *) -> (B :: A -> *) -> Exists A B -> A fst'ex A B p = elim A B p A (\a _ -> a) to get the first component of the pair out. What cannot be done (unless there is some other strong sigma type) is to prove the second component has a type dependent on the thing we've projected. snd'ex :: (A :: *) -> (B :: A -> *) -> (p :: Exists A B) -> B (fst'ex p) snd'ex A B p = elim A B p (B (fst'ex p)) (\a b -> {- b :: B a /= B (fst p) -}) So, an existential of this sort still has to carry around its first component, it just doesn't have a strong elimination principle. This isn't very surprising, because in the calculus of constructions, say, we can implement existentials via Church encoding: Exists A B = (R :: *) -> ((a :: A) -> B a -> R) -> R and we can also implement pairs: A * B = (R :: *) -> (A -> B -> R) -> R but the latter is just a specialization of the former, where B is constant. And certainly, pairs are expected to carry both of their components. (One case where it may be safe to erase is: Ex :: (* -> *) -> * elim :: (B :: * -> *) -> Ex B -> (R :: *) -> (_ :: (A :: *) -> B A -> R) -> R because to project out the first component, we'd need * :: * to set R = *, which is often rejected.) However, one thing you can do is have a special erasable function space [1], which places restrictions on how you are allowed to use the parameter. Roughly, you have: (x :: A) => B /\(x :: A) -> e f @x for the function space, lambda expression and application respectively. And for instance: /\(A :: *) -> \(x :: A) -> x is well-typed---because the erasable parameter A only appears to the right of a ::, and type annotations get erased---but: /\(A :: *) -> A is not, because the function returns a value that is supposed to be erasable. Then, we can give existentials the following eliminator: elim :: (A :: *) => (B :: A -> *) => (_ :: Exists A B) -> (C :: *) => (_ :: (a :: A) => B a -> C) -> C (you may have to take my word that that's a valid signature in some places, or read the linked paper below) and we can attempt to write fst'ex as above: elim @A @B p @A (/\a -> \_ -> a) but we see that the lambda expression we've written here tries to return a value from an erasable lambda, and so it is rejected. So using these sort of types, it's actually safe to erase the first component of an existential. -- Dan [1] http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.92.7179
Dan Doel wrote:
On Thursday 12 August 2010 7:59:09 pm wren ng thornton wrote:
Not quite. Strong-sigma is a dependent pair where you can project both elements. Weak-sigma is a dependent pair where you can only project the first element (because the second is erased). Existentials are dependent pairs where you can only project the second component (because the first is erased).
elim :: (A :: *) -> (B :: A -> *) -> (_ :: Exists A B) -> (C :: *) -> (_ :: (a :: A) -> B a -> C) -> C
Notice how we only get the Church-encoding for existential elimination and how 'a' cannot appear in 'C'. Whereas for 'snd' we explicitly allow 'fst p' to escape.
This is how it's usually explained, but note that this eliminator type is not strict enough to guarantee that it's safe to erase the first component. We can still write:
[...]
So, an existential of this sort still has to carry around its first component, it just doesn't have a strong elimination principle.
Right. The point remains that existentials and sigmas differ. Using only 'elim' they differ in not having a strong elimination principle; using other things they differ in erasure properties as well. People seem eager to conflate the notions of existential quantification with strong sigma types, but the fact is that they are different things. Often we use existentials precisely because we want the weaker elimination principle, in order to hide details and bracket off where things can be accessed from. With strong sigmas we can't get those guarantees. -- Live well, ~wren
Hi, to understand forall and exists in types, I find it helpful to look at the terms which have such types. Joshua Ball wrote:
mapInt :: forall a. (Int -> a) -> [Int] -> [a]
I can instantiate that function over a type and get a beta-reduced version of the type
mapInt [String] :: (Int -> String) -> [Int] -> [String]
So mapInt could be defined with a upper-case lambda /\ which takes a type: mapInt = /\a -> ... Of course, in Haskell, we don't have that lambda explicitly.
The universal quantifier is basically a lambda, but it works at the type level instead of the value level.
Not quite. It is the /\ which is like \, except that \ takes a value, while /\ takes a type. Now, the type of /\ ... is forall ..., and the type of \ ... is ... -> ... . Therefore, forall is similar to ->. And indeed, both forall and -> describe terms which take arguments. However, there are two differences between -> and forall. First, a term described by -> takes a value argument, while a term described by forall takes a type argument. And second, the result type of a term described by -> is independent from the argument taken, while the result type of a term described by forall may depend on the argument taken.
My question is... what is the analog to an existential type?
mapInt :: exists a. (Int -> a) -> [Int] -> [a]
This mapInt could be defined with a version of the pair constructor (,) which accepts a type in the first component. mapInt = (SomeType, ...) Note that the ... in that definition need to have the following type: (Int -> SomeType) -> [Int] -> SomeType So exists is similar to (,). Both exists and (,) describe terms which represent pairs. And again, there are two differences between (,) and exists. First, a term described by (,) represents a pair of two values, while a term described by exists represents a pair of a type and a value. And second, the type of the second component of a term described by (,) is independent of the first component, while the type of the second component of a term described by exists may depend on the first component.
1. If I can "instantiate" variables in a universal quantifier, what is the corresponding word for variables in an existential quantifier?
If foo has an universal type, the caller of foo can choose a type to be used by foo's body by instantiating the type variable. That type variable is available to foo's body. If foo has an existential type, the body of foo can choose a type to be available to the caller of foo by creating an existential pair. That type is available to foo's caller by unpacking the existential pair, for example, by pattern matching.
2. If type instantiation of a universally quantified variable is beta-reduction, what happens when existentially quantified variables are [insert answer to question 1]?
beta-reduction happens when the type application meets the lambda abstraction: (/\ a -> b) [T] ~> b [a := T] The corresponding reduction for existentials happens when the unpacking meets the construction of the existential pair. case (T, t) of (a, x) -> b ~> b [a := T; x := t] I don't know how it is called. BTW, note how the type variable a is bound in the pattern of the case expression, so it scopes over b. But the type of b is also the type of the overall case expression. Therefore, if the type of b would mention the type variable a, so would the overall type of the case expression, and then, the type variable a would be used out of scope. This is why GHC complains about "escaping type variables" sometimes.
3. Is there any analogue to existential quantifiers in the value world? "Forall" is to "lambda" as "exists" is to what?
Forall is to lambda as exists is to (,), as discussed above. HTH, Tillmann
Joshua Ball wrote:
Hi,
If I have a universally quantified type
mapInt :: forall a. (Int -> a) -> [Int] -> [a]
I can instantiate that function over a type and get a beta-reduced version of the type
mapInt [String] :: (Int -> String) -> [Int] -> [String]
(I'm borrowing syntax from Pierce here since I don't think Haskell allows me to explicitly pass in a type to a function.)
The standard syntax around here is to use @ for type application. I.e., that's what's used in Core.
This makes sense to me. The universal quantifier is basically a lambda, but it works at the type level instead of the value level.
Not quite. In standard Church-style System F it's a lambda at the value level, just a different one from the regular lambda. Tillmann Rendel covered this. If you actually have lambdas at the type-level, then it's a higher-order language. System F^omega has this, but System F does not.
My question is... what is the analog to an existential type?
mapInt :: exists a. (Int -> a) -> [Int] -> [a]
Existentials are a pair of a witness (the particular type A) and the thing being quantifier over. E.g., one possible implementation of mapInt is: mapInt = Ex A (mapPoly @A) where Ex :: forall f. (a :: *) -> (_ :: f a) -> (exists b. f b) This is just part of the duality between functions and pairs. (Though the idea of "pairs" breaks apart once you move to full dependent types or various other interesting systems.)
1. If I can "instantiate" variables in a universal quantifier, what is the corresponding word for variables in an existential quantifier?
The first component of the pair with an existential type is called a "witness". Because this first component serves to witness the fact that, yes, there does indeed exist such a type; namely this one right here.
Also (separate question), is the following statement true?
forall T :: * -> *. (forall a. T a) -> (exists a. T a)
If so, what does the implementation look like? (What function inhabits it, if it is interpreted as a type?)
No, it's not true. However, this slight variation is true (using (->) for forall): foo :: (T :: * -> *) -> (A :: *) -> (x :: (B :: *) -> T B) -> Exists T foo T A x = Ex A (x @A) That is, your statement is only true when we can independently prove that there is a type. Which type doesn't matter, but we must prove that at least one type exists. This is because we can't construct a proof of the existential unless we can come up with a witness; for all we know, the set being quantified over may be empty, in which case there doesn't exist an a such that T a. -- Live well, ~wren
participants (5)
-
Dan Doel -
Daniel Peebles -
Joshua Ball -
Tillmann Rendel -
wren ng thornton