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/Xfunctionali... 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