[Haskell-cafe] Categorical description of systems with dependent types
cppljevans at suddenlink.net
Thu Dec 2 17:01:38 CET 2010
On 12/02/10 09:13, Petr Pudlak wrote:
> 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
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:
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).
More information about the Haskell-Cafe