User loginNavigation 
Type theory question...I've been thinking (and reading) about dependent types and related topics (Calculus of constructions, ML type theory, and so on). First, I'd like to say how really clear and useful I found the second chapter of ATTAPL ("Dependent Types" by Aspinall and Hofmann). Their presentation of the CoC really clarified things for me. The extra overhead of the Prf type constructor and the distinction it draws between Πtypes and ∀ terms was pretty instructive to me (I'd previously seen the CoC with only λ and ∀, as it's presented here). Obviously I've hardly gotten my feet wet, but as an introduction, I highly recommend this article. But I'm left with a question that I hope someone here can answer. I'm confused by the standard terminology for Π and Σtypes, "dependent products" and "dependent sums," respectively. For the life of me I can't fathom what these types have to do with anything I've normally thought of as a product or a sum. The product seems to be a function type, and the sum seems (against all common sense) to be a product! And in fact, to make matters even worse, what I generally think of as a "sum" (logical disjunction or variant types) seems to be most easily defined in terms of dependent product. I guess I'm not alone in finding this confusing. This post on the types list is relevant, but doesn't really help me understand the logic (no pun intended) behind the standard terminology, and the observation that "the dependent product type was in fact a sum type" really highlights my lack of insight.
This might also be relevant (from here), but honestly I'm not even sure anymore! I really hope someone can clarify this for me, even if only from a historical perspective... [Ehud, I'm not really sure if this kind of thing is appropriate for the front page... Any guidance?] By Matt Hellige at 20060211 21:41  LtU Forum  previous forum topic  next forum topic  other blogs  12134 reads

Browse archivesActive forum topicsNew forum topics

Recent comments
1 hour 21 min ago
3 hours 24 min ago
9 hours 34 min ago
10 hours 17 min ago
12 hours 41 sec ago
13 hours 2 min ago
14 hours 40 min ago
14 hours 53 min ago
15 hours 50 min ago
22 hours 1 min ago