[Prev][Next][Index][Thread]
Re: what are dependent types? (reply to A. Pitts)
Date: Tue, 12 Jun 90 20:48:00 BST
To: ap <ap@computer-lab.cambridge.ac.uk>, types@theory.lcs.mit.edu
Andy Pitts wrote:-
----
. . . . . .
From: ap <ap%uk.ac.cam.cl@nsfnet-relay.ac>
I like the (Cornell?) terminology of `dependent product type' for
\Sigma and `dependent function type' for \Pi because it reminds you
that in the special case of no dependency (i.e. for simple types) the
notions specialize to the usual binary product and function type.
However, I don't use that terminology because I judge that the use of
the terms `dependent sum' and `dependent product' are generally
accepted (and more importantly, generally understood).
. . . . . . . .
---- (end of quoted material)
My experience has been that the terms "dependent sum" and "dependent
product" are a source of confusion; the Cornell terms are far more natural.
In our work on the Flagship type system, we used the Cornell terms and
avoided Sigma and Pi notation (a decorated arrow for dependent function,
and a decorated cross for dependent product). My own feeling is that if
we were to call the dependent product a dependent sum, and use a sigma
notation, we would end up calling the simple (no dependence) product
a sum and using a decorated plus instead of a cross (the simple product
is of course the sum - disjoint union - of many copies of the right hand
argument with itself, the labels being taken from the left hand argument).
The flagship type system went through many versions, and I hope one day to
find time to write it up properly; dependent types were a large bone of
contention and we had many different versions at different times; none
of us (industrial and academic partners in the project) ever advocated
using the term dependent sum to describe a product. We had one dependent type
in addition to the usual function and product: the dependent map (a map is
a function extent, ie a set of pairs representing argument and value). Has
this cropped up anywhere else? A very brief description of (an early version
of) this type system - about one page - appeared as a subsection of the
paper "Designing System Software for Parallel Declarative Systems" [Broughton,
Thomson,Leunig &Prior; ICL Tech Journal Vol5 No3, May 87].
Tom Thomson