MathOverflow is a question and answer site for professional mathematicians. Join them; it only takes a minute:

Sign up
Here's how it works:
  1. Anybody can ask a question
  2. Anybody can answer
  3. The best answers are voted up and rise to the top

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?

share|cite|improve this question

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.

share|cite|improve this answer
I was thinking of what wikipedia calls the polymorphic lambda calculus or system F. As it is a form of 2nd-order logic, would this mean it would be modelled by some kind of bicategory? – Mozibur Ullah Sep 22 '12 at 22:18
You can't run analogies like that. The prefix "bi" in bicategories has nothing to do with "second" in "second order arithmetic. System F is quite a bit trickier to get right. See for example Paul Taylor's "Semantics of System F" at – Andrej Bauer Sep 22 '12 at 22:53
@Bauer: It was a guess, and a bad guess at that :), thanks for the reference. – Mozibur Ullah Sep 23 '12 at 15:59

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.

share|cite|improve this answer

Your Answer


By posting your answer, you agree to the privacy policy and terms of service.

Not the answer you're looking for? Browse other questions tagged or ask your own question.