[Haskell-cafe] Categorical description of systems with dependent types
cppljevans at suddenlink.net
Fri Dec 3 01:54:18 CET 2010
On 12/02/10 15:47, Iavor Diatchki wrote:
> 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.
*Maybe* the computer science people are trying to minimize the concepts.
In this case, the one concept common to both the sum and product ( in
the math peoples viewpoint) is there's a function:
field2type: field_name -> Type
in the case of a product or record, r, it's:
product = f:fieldname -> field2type(f)
in the case of a disjoint sum its:
sum = (f:fieldname, field2type(f))
or something like that.
More information about the Haskell-Cafe