Generalization of Exponential Type

Question

How (if at all) does the exponential interpretation of (->) (a -> b as b^a) 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 2^{a * b} (a -> b -> Bool).

Answer 1

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:

• a product object (a * b), and
• an exponential object (b^ab)

with morphisms

• eval : (b^a)*a -> b (in Haskell: \(f,x) -> f x, AKA apply)
• for any f : (a*b)->c, there exists Lf : a -> (c^b) (in Haskell: curry f)

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

• f = (Lf * id_a) ; eval

In Haskell, the last equation is:

• f = \(x :: (a,b), y :: a) -> apply (curry f x, id y) where apply (g,z) = g z

or, using arrows,

• f = (curry f *** id) >>> apply where apply (g,z) = g z