[Haskell-cafe] universal quantification is to type instantiations
as existential quantification is to what
wren ng thornton
wren at freegeek.org
Thu Aug 12 19:59:09 EDT 2010
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
More information about the Haskell-Cafe
mailing list