On Sat, 2007-08-04 at 23:25 +0800, Shin-Cheng Mu wrote:
[...]
In Haskell, the existential quantifier is mimicked by forall. We define:
data DepSum a p = forall i . DepSum (a i) (p i)
The term "dependent sum" is borrowed from the Omega tutorial of Sheard, Hook, and Linger [2] (why is it called a sum, not a product?).
There is already a dependent product. One compelling reason for this naming comes from category theory and how they relate to each other (the dependent sum is a left adjoint, the dependent product is a right adjoint [not directly to each other].) They are related in the same way products and sums are related, or universal quantification and existential quantification are. So, looking at the product case (A,B)=AxB (and ()=1) and the sum case Either A B = A+B we can see how they generalize to be the above. Let's say we have a pair of the same type. We can clearly represent it as AxA, but another alternative is 1+1->A. We can write the isomorphism in Haskell: pToF :: (a,a) -> (Either () () -> a) pToF (x,_) (Left ()) = x pToF (_,y) (Right ()) = y fToP :: (Either () () -> a) -> (a,a) fToP f = (f (Left ()), f (Right ())) Similarly for sums, A+A can be written (1+1)xA. Again, the Haskell: sToP :: Either a a -> (Either () (),a) sToP (Left x) = (Left (), x) sToP (Right x) = (Right (), x) pToS :: (Either () (), a) -> Either a a pToS (Left (), x) = Left x pToS (Right (), x) = Right x Incidentally, this is how sums are usually encoded, i.e. a pair of a tag and a value. (Also incidentally, these are almost exactly the isomorphisms defining adjunctions related to the ones that define product and sum, i.e. the above definitions immediately fall out of the category theory.) So how to represent AxB or A+B with this encoding? You can't. However, in a dependently typed language we can write (in some dependently typed pseudo-Haskell) [for concreteness, let's set A=Int, B=String]: f :: Either () () -> Type f (Left ()) = Int f (Right ()) = String Now we use the same definitions as above only with the types, pToF :: (Int,String) -> (s :: Either () () -> f s) fToP :: (s :: Either () () -> f s) -> (Int,String) sToP :: Either Int String -> s :: Either () (). f s pToS :: (s :: Either () (). f s) -> Either Int String This leads to the dependent product being a function space when there is no dependency, and similarly the dependent sum being a (normal) product.