On 12/02/10 09:13, 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. > > Thanks, > Petr
Hi Petr, Although it's not a categorical description of dependent types (AFAICT, but I've almost no experience in category theory), dependent types are described by Nuprl: http://www.cs.cornell.edu/Info/People/sfa/Nuprl/NuprlPrimitives/Xfunctionality2_doc.html For example, on that page, there's this: Actually, A->B is a special form of the more general x:A->C(x). When A is a type and C(x) is a type-valued function (in x) over domain A, then a member of x:A->C(x) is a function which for an argument, a:A takes a value in the type C(a). HTH. -Larry _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe