Another way of understanding the terminology is this: A "dependent product" type (usually written \Pi x:A.B) can be thought of as a big product of the types (B[a1/x], ..., B[aN/x]) for the inhabitants a1...aN of the type A. To introduce a dependent product, you have to provide each component of the tuple. To eliminate a dependent product, you can project out one component. A "dependent sum" type (usually written \Sigma x:A.B) can be thought of as a big sum of the types B[a1/x] + ... + B[aN/x], where again a1 .. aN are all the inhabitants of A. To introduce a dependent sum, you pick a particular branch of the sum (by choosing an a_i) and inject a value of that type (i.e., B[a_i/x]). To eliminate a dependent sum, you can see what branch a value is in (i.e., recover the a_i) and you can see what the associated data is. This terminology takes a little getting used to because of how we usually present these intro and elim forms syntactically. Consider dependent products. For finite products (e.g., (Int, String)) we introduce a product just by writing down an inhabitant of each component type. However, the dependent product needs one component for each inhabitant of the type A, so we can't in general list them all explicitly. Thus, the usual intro form for a dependent product is to give an inhabitant of B for a generic inhabitant x of A (i.e., a variable x:A). So the intro form is a function. On the other hand, to eliminate a finite product we usually say "I'd like the 2nd component, please". But for a dependent product, you have to say "I'd like the a_i^th component", so the elim is application. Sums are similar. For a finite sum, we usually say "this data is in the second branch", but for a dependent sum, we have to say "this data is in the a_i^th branch". So the intro form is a pair of a tag a_i and a value of type B[a_i/x]. On the other hand, to eliminate a finite sum, we usually do a case with one branch for each of the tags, where in each branch we get the tagged value. To eliminate a dependent sum, we cover all those cases at once by getting (1) a generic tag x:A and (2) a value of the type associated with that tag. But this is exactly a split (x,y) = e1 in e2 pattern-matching style elimination form for a pair. So, dependent products are represented by functions, and dependent sums are represented by pairs. It's confusing at first, but it's established terminology. I tend to use "dependent function" and "dependent pair" myself, since sometimes people use "dependent product" to mean \Sigma rather than \Pi (understandable given the intro and elim for \Sigma!), so I sometimes find it ambiguous. Does that make sense? -Dan On Aug04, Derek Elkins wrote:
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.
_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe