[Prev][Next][Index][Thread]
what are dependent types??
Date: Mon, 21 May 90 14:34:04 BST
The term "dependent type" was, I think, coined at Cornell to explain the
Pi and Sigma types as generalizations of function and (binary) product types.
The Pi type was called the "dependent function type" and the Sigma type was
called the "dependent product type". This gave the right intuition, but
unfortunately the dependent product type was in fact a sum type.
An alternative terminology is now often seen: the Pi type is called the
"dependent product type" and the Sigma type is called the "dependent sum
type". This avoids the problem with the Cornell terminology, but loses the
original intuition; it is not clear whether "dependent" means anything any
more.
A recent paper combines these terminologies: Pi is called the dependent
function type and Sigma is called the dependent sum type. This appears to
be an error, but it suggests that the terminology of dependent types is too
confusing to be useful. Why can't Pi and Sigma types just be called Pi and
Sigma types? If a more formal terminology is required, how about "general
product" and "general sum"?
Larry Paulson