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
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
