haskellcategory-theorycategory-abstractions

Generalization of Exponential Type


How (if at all) does the exponential interpretation of (->) (a -> b as ba) generalize to categories other than Hask/Set? For example it would appear that the interpretation for the category of non-deterministic functions is roughly Kliesli [] a b as 2a * b (a -> b -> Bool).


Solution

  • The notion of exponential can be defined in general terms, beyond Hask/Set. A category with exponentials and products is called a cartesian closed category. This is a key notion in theoretical computer science since each c.c. category is essentially a model of the typed lambda calculus.

    Roughly, in a cartesian closed category for any pair of objects a,b there exist:

    with morphisms

    satisfying the equation "they enjoy in the lambda calculus", i.e., if f : (a*b)->c, then:

    In Haskell, the last equation is:

    or, using arrows,