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

[Larry Evans]

On 12/02/10 15:47, 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.
> -Iavor
[snip]
*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.

-Larry