haskell - 指数型の一般化

Question

(->)( a -> bas b ^a )の指数関数的解釈は、Hask/Set 以外のカテゴリにどのように一般化されますか? たとえば、非決定論的関数のカテゴリの解釈は、おおよそ2 ^{a * b} ( ) のKliesli [] a bように見えます。a -> b -> Bool

Answer 1

指数関数の概念は、Hask/Set を超えた一般的な用語で定義できます。指数と積を含むカテゴリは、デカルト閉カテゴリと呼ばれます。各 cc カテゴリは本質的に型付きラムダ計算のモデルであるため、これは理論的コンピューター サイエンスにおける重要な概念です。

大まかに、オブジェクトの任意のペアのデカルト閉カテゴリには、次のものa,bが存在します。

• 製品オブジェクト(a * b)、および
• 指数オブジェクト(b^ab)

射で

• eval : (b^a)*a -> b(Haskell: \(f,x) -> f x, AKA apply)
• 任意の に対してf : (a*b)->c、存在しますLf : a -> (c^b)(Haskell: curry f)

「彼らはラムダ計算を楽しんでいる」という方程式を満たします。つまり、 if f : (a*b)->c, then:

• 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