[Prev][Next][Index][Thread]
Re: what are dependent types??
To: Larry Paulson <@nsfnet-relay.ac.uk:lcp@lfcs.edinburgh.ac.uk>
Cc: types@theory.lcs.mit.edu
Date: Wed, 23 May 90 09:52:56 +0100
Well, in my book (yet to be written!) `dependent' types are type
expressions which contain (hence DEPEND on) variables---in contrast
with `simple types' (as in "simply typed lambda calculus") which do not.
Within the context of such dependent types, there are sum types
($\Sigma) x\in A.B(x)$) and product types ($\Pi x\in A.B(x)$). Then
it's a useful short-hand to refer to `dependent sum types' and
`dependent product types'.
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).
Finally, don't forget that
"Exessive concern with terminology gives a subject a bad name."
Anon
Andy Pitts