[Haskell-cafe] Categorical description of systems with dependent types
Larry Evans
cppljevans at suddenlink.net
Thu Dec 2 17:01:38 CET 2010
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
More information about the Haskell-Cafe
mailing list