[Haskell-cafe] Categorical description of systems with dependent types

[wren ng thornton]

On 12/2/10 4:47 PM, Iavor Diatchki wrote:
> Hi,
> You have it exactly right, and I don't think that there's a
> particularly deep reason to prefer the one over the other.  It seems
> that computer science people
> tend to go with the (product-function) terminology, while math people
> seem to prefer the (sum-product) version, but it is all largely a
> matter of taste.

The product=function,sum=pair terminology comes from a certain 
interpretation of dependent types in set theory. I believe this 
originated with Per Martin-Löf's work, though I don't have any citations 
on hand.

That terminology conflicts with the standard product=pair,sum=either 
terminology of functional languages, however. So folks from a functional 
background tend to prefer: dependent function, dependent product, sum; 
whereas folks from a set-theoretic background tend to prefer product, 
sum, <no name>/union.

-- 
Live well,
~wren