指數類型的推廣

Question

(->)（a -> b as $ b^a $）的指數解釋如何（如果有的話）推廣到除Hask/Set以外的類別？例如，對於非確定性函數類別的解釋看起來大致爲Kliesli [] a b爲$ 2 ^（a * b）$（a - > b - > Bool）。

Answer 1

除了Hask/Set之外，指數的概念可以用一般術語定義。指數和產品類別稱爲cartesian closed category。這是理論計算機科學的一個關鍵概念，因爲每一個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）

滿足方程 「他們在演算享受」，即如果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