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

[wren ng thornton]

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