[Haskell-cafe] Categorical description of systems with dependent types

[Larry Evans]

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