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  10021 reads

Browse archivesActive forum topics 
Recent comments
3 hours 40 min ago
7 hours 41 min ago
7 hours 49 min ago
8 hours 7 min ago
8 hours 12 min ago
8 hours 31 min ago
8 hours 40 min ago
8 hours 44 min ago
8 hours 47 min ago
8 hours 54 min ago