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

[wren ng thornton]

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