[Haskell-cafe] universal quantification is to type instantiations as existential quantification is to what

[Dan Doel]

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