Hi,
Bart Jacobs's book "Categorical Logic and Type Theory" has a
categorical description of a system with dependent types (among
others). The book is fairly advanced but it has lots of details about
the constructions.
Hope this helps,
-Iavor
On Thu, Dec 2, 2010 at 8:18 AM,
On Thu, 2 Dec 2010, Petr Pudlak wrote:
Hi,
recently, I was studying how cartesian closed categories can be used to describe typed functional languages. Types are objects and morphisms are functions from one type to another.
Since I'm also interested in systems with dependent types, I wonder if there is a categorical description of such systems. The problem (as I see it) is that the codomain of a function depends on a value passed to the function.
I'd happy if someone could give me some pointers to some papers or other literature.
Voevodsky talks about the category of contexts in http://www.mefeedia.com/watch/31778282, which I understand is described in more detail in "Semantics of type theory : correctness, completeness, and independence results" by Thomas Streicher.
-- Russell O'Connor http://r6.ca/ ``All talk about `theft,''' the general counsel of the American Graphophone Company wrote, ``is the merest claptrap, for there exists no property in ideas musical, literary or artistic, except as defined by statute.''
_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe