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