Generalization of Exponential Type

370 views Asked by At

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).

1

There are 1 answers

0
chi On BEST ANSWER

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