指数类型的泛化

Question

(->)（a -> b作为b^a）的指数解释如何（如果有的话）推广到Hask/Set以外的类别？例如，对非确定性函数类别的解释似乎大致Kliesli [] a b为2^{a * b}（a -> b -> Bool）。

Answer 1

指数的概念可以用一般术语来定义，超越 Hask/Set。具有指数和乘积的类别称为笛卡尔封闭类别。这是理论计算机科学中的一个关键概念，因为每个c.c.类别本质上都是类型化lambda演算的模型。

粗略地说，在笛卡尔闭合范畴中，存在a,b任何一对对象：

• 产品对象(a * b) ，以及
• 指数对象(b^ab)

有态射

• eval : (b^a)*a -> b（哈斯克尔语：(f,x) -> f x，AKA适用）
• 对于任何f : (a*b)->c，都存在Lf : a -> (c^b)（哈斯克尔：curry f）

满足方程"他们在lambda演算中享受"，即，如果f : (a*b)->c，则：

• f = (Lf * id_a) ; eval

在 Haskell 中，最后一个等式是：

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

或者，使用箭头，

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