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