[Haskell-cafe] universal quantification is to type instantiations
as existential quantification is to what
wren ng thornton
wren at freegeek.org
Fri Aug 13 03:57:28 EDT 2010
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
More information about the Haskell-Cafe
mailing list