13

私が書いているライブラリでは、次のような (ただし、より一般的な) クラスを書くのが一見エレガントであることがuncurryわかりました。必要に応じて):fanin

{-# LANGUAGE TypeOperators, TypeFamilies,MultiParamTypeClasses, FlexibleInstances #-}
import Prelude hiding(uncurry)
import qualified Prelude 

class Uncurry t r where
    type t :->-> r
    uncurry :: (t :->-> r) -> t -> r

instance Uncurry () r where
    type () :->-> r = r
    uncurry = const

instance Uncurry (a,b) r where
    type (a,b) :->-> r = a -> b -> r
    uncurry = Prelude.uncurry

instance (Uncurry b c, Uncurry a c)=> Uncurry (Either a b) c where
    type Either a b :->-> c = (a :->-> c, b :->-> c)
    uncurry (f,g) = either (uncurry f) (uncurry g)

私は通常、Edward Kmett のcategoriesパッケージ (上記のリンク) を参照して、この種のことを理解していますが、そのパッケージには、fanin と uncurry がそれぞれ CoCartesian クラスと CCC クラスに分けられています。

BiCCCについて少し読んだことがありますが、まだよくわかりません。

私の質問は

  1. 上記の抽象化は、圏論に目を細める何らかの方法によって正当化されますか?

  2. もしそうなら、クラスとそのインスタンスについて話すのに適切なCTに基づいた言語は何でしょうか?

編集：それが役に立ち、上記の単純化が物事を歪めている場合：私の実際のアプリケーションでは、ネストされた製品と副産物を扱ってい(1,(2,(3,())))ます。これが実際のコードです (ただし、退屈な理由から、最後のインスタンスは簡略化されており、書かれているように単独では機能しません)

instance Uncurry () r where
    type () :->-> r = r
    uncurry = const

instance (Uncurry bs r)=> Uncurry (a,bs) r where
    type (a,bs) :->-> r = a -> bs :->-> r
    uncurry f = Prelude.uncurry (uncurry . f)

-- Not quite correct
instance (Uncurry bs c, Uncurry a c)=> Uncurry (Either a bs) c where
    type Either a bs :->-> c = (a :->-> c, bs :->-> c)
    uncurry (f,fs) = either (uncurry f) (uncurry fs) -- or as Sassa NF points out:
                                                     -- uncurry (|||)

したがって、constインスタンスは()、n-ary tuple uncurry インスタンスの再帰的な基本ケースとして自然に生まれましたが、3 つすべてを一緒に見ると... 恣意的なものではないように見えました。

アップデート

代数演算の観点から考えると、「ADT の代数」についてのChris Taylor のブログであることがわかりました。そうすることで、私のクラスとメソッドが実際には指数法則にすぎないことが明らかになりました (そして、私の最後のインスタンスが正しくなかった理由)。

結果は、私のshapely-dataパッケージのExponentおよびBaseクラスで確認できます。ノートと不安定でないドキュメント マークアップのソースも参照してください。

4

1 に答える 1

10

最後の Uncurry インスタンスはまさにuncurry (|||)であるため、「より一般的な」ものはありません。

Curry は、任意の矢印 f: A×B→Cに対して、一意の矢印 eval: C B ×B→Cが交換されるような矢印カレーf : A→C Bを見つけます。eval を として表示できます。「CCC」と言うのは、「このカテゴリには、すべての積、すべての指数、および終端オブジェクトがあります」の省略形です。つまり、カリー化は、任意の型のペアと haskell の任意の関数に対して機能します。CCC であることの重要な結果の 1 つは、A=1×A=A×1 (またはが と同形でと同形) であるということです。($)a(a,())((),a)

Haskell の Uncurry は、同じプロセスの反対のラベル付けです。矢印 f=uncurry gから始めます。各ペアには 2 つのプロジェクションがあるため、proj 1とカリーf =g の合成により C Bが得られます。構成と製品について話しているので、CCC での uncurry は、任意の g に対して一意の uncurry gを定義します: A→C B。CCC にはすべての製品があるため、C に評価できる C B × B があります。

特に、A=A×1 を思い出してください。これは、任意の関数 A→B が関数 A×1→B であることを意味します。これを、「任意の関数 A→B に対して関数 A×1→B が存在する」と見なすこともできます。これは、簡単な uncurrying によって証明されますid。

カリー化が定義されているのと同じ意味で、最後のインスタンスを「アンカリー」とは呼びません。最後のインスタンスは、共積の定義の構成です。矢印 f: A→C および g: B→C の任意のペアに対して、一意の矢印 [f,g]: (A+B)→C が存在します。この意味で、これはインターフェイスの乱用のように見えます。これは、「uncurry」から「与えられたもの、何かを与えてください」または「:->->と haskell 関数の間の真の対応」への意味の一般化です。おそらく、クラスの名前を Arrow に変更できます。

于 2013-10-09T09:15:59.110 に答える