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
).
Generalization of Exponential Type
370 views Asked by David Harrison At
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 * b)
, and(b^ab)
with morphisms
eval : (b^a)*a -> b
(in Haskell:\(f,x) -> f x
, AKA apply)f : (a*b)->c
, there existsLf : 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