the unadorned typed lambda calculus correspond to the closed cartesian categories, but if we add in dependent or parametric types how are they then characterised?
Remember to vote up questions/answers you find interesting or helpful (requires 15 reputation points)
|
2
2
|
|
|
|
|
9
|
Dependent type theory, i.e., $\lambda$-calculus with dependent products and dependent sums corresponds to locally cartesian closed categories, which was written up by R. Seely in "Locally cartesian closed categories and type theory", Math. Proc. Phil. Comb. Soc, (1984), 95, 33. If by "parametric types" you mean the kind of polymorphism that is present in ML, then one possible semantics is that of relationally parametric models. Probably the most influental in the development of this idea was John Reynolds, see for example his "Types, abstraction and parametric polymorphism" from 1983. |
|||||||||||
|
You can accept an answer to one of your own questions by clicking the check mark next to it. This awards 15 reputation points to the person who answered and 2 reputation points to you.
|
4
|
The internal language of a locally Cartesian closed category is a dependent type theory. A category $\mathcal C$ is locally Cartesian closed, if all of its slices $\mathcal C/X$ are Cartesian closed. An arrow $f:X\to Y$ is both interpreted as a variable substitution and as a family of types indexed over $Y$ in the type theory. |
||
|
|
