Home » forums » LtU Forum

Examples of Categorical Semantics for Languages with Dependent Types

Is there a reference that describes how to define categorical semantics for lambda calculus enriched with dependent types? Both Pierce and Gunter give a good description of the categorical semantics of lambda calculus in their respective books. However, they use a simple type system. I would like to see a description of something more expressive. Examples from any class of dependent type system are helpful--system F, full calculus of constructions, etc...

I am working on a language where I would like to have simple dependent types such as sized lists. I don't really need higher-order abstraction. But, I would like to describe the semantics of /\n.list(n).

By echinuz at 2007-09-06 20:43 | LtU Forum | previous forum topic | next forum topic | other blogs | 7331 reads

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

Categorical Logic and Type Theory by Bart Jacobs

Categorical Logic and Type Theory by Bart Jacobs does the full lambda cube categorically. The book is expensive however so maybe his PhD thesis is enough to get you started.

Cheers,
Thorvaldur

UPDATE: Actually, the "left plane" of the lambda cube is covered and the calculus of constructions. Logical frameworks are mentioned only briefly.

By Thorvaldur Thorvaldsson at Thu, 2007-09-06 21:06 | login or register to post comments

Good Reference, but the Approach Requires a lot of Machinery

Thank you for the reference; it was precisely what I asked for. Although it will take some time to work through the book, the approach seems very complicated for the simple situation that I am looking at. Consider a very simple mathematical language where we want to add and multiply matrices. The grammar for this language is:

e::=c | e + e | e * e
t::=Real[m,n]

where c is a constant, + indicates addition, and * indicates multiplication. The types in t represent all m by n real matrices. Are dependent types needed in this case (t::=pi n.pi m.Real[m,n])? Or, is it proper to state that there's an infinite number of types of the form Real[1,1], Real[1,2], etc...? In the second case, describing the semantics is far easier since all the machinery for correctly describing the semantics of dependent types is not needed.

By echinuz at Fri, 2007-09-07 05:20 | login or register to post comments

Syntax and Semantics of Dependent Types

You may be interested in Syntax and Semantics of Dependent Types by Martin Hofmann. It's not exactly light reading, but it does not rely on all the "fibration machinery". It has a few useful references and compares his "categories with families" to several other formalizations of type theory.

I think it will require quite some work to the understand and apply this kind of categorical semantics. It sure took me a while to get some kind of clue.

By Wouter Swierstra at Fri, 2007-09-07 08:06 | login or register to post comments

Seconded

This is the reference I would recommend, or rather either this (which is his lecture notes from the CLiCS-II summer school), or his PhD thesis Extensional concepts in intensional type theory, which is a must read for folks interested in getting to grips with the concept of equality in dependent type theory. Thomas Streicher has done a fair bit with Hofmann-style semantics for dependent types.

His PhD appears in the CUP distinguished dissertations series, so it is a pretty common inhabitant of CS libraries.

Postscript: Twenty-five years of constructive type theory (OUP 1997) has a chapter on groupoid semantics of dependent types by Hofmann and Streicher, which I have not worked through.

Postscript 2: Hofmann & Streicher's paper is available as a preprint, The Groupoid Interpretation of Type Theory.

By Charles Stewart at Fri, 2007-09-07 12:28 | login or register to post comments

Thanks for the pointer, this

Thanks for the pointer, this definitely seems lighter than Jacobs' tour de force.

By Thorvaldur Thorvaldsson at Sat, 2007-09-08 02:04 | login or register to post comments