短い質問:プログラミング (つまり、関数型プログラミング) における同形関数の重要性は何ですか?
長い質問:関数型プログラミングと圏論の概念との間のいくつかの類推を、時々耳にする専門用語に基づいて描こうとしています。基本的に、私はその専門用語を具体的なものに「アンパッケージ」して、さらに拡張できるようにしようとしています。その後、私が話していることを理解して専門用語を使用できるようになります。これはいつもいいです。
私がよく耳にするこれらの用語の 1 つにIsomorphismがあります。これは、関数または関数合成間の同等性についての推論に関するものだと思います。同型のプロパティが (関数型プログラミングで) 役立ついくつかの一般的なパターンと、同型関数に関する推論からのコンパイラの最適化などの副産物について、誰かがいくつかの洞察を提供できるかどうか疑問に思っていました。
同型写像の圏論定義はオブジェクトについて何も述べていないので、私は同型写像の賛成の答えに少し問題を抱えています。理由を確認するために、定義を確認してみましょう。
同型写像は、射のペア（つまり、関数）でfありg、次のようになります。
f . g = id
g . f = id
これらの射は、「等」射と呼ばれます。多くの人は、同型写像の「射」がオブジェクトではなく関数を指していることに気づいていません。ただし、それらが接続するオブジェクトは「同形」であると言うでしょう。これは、他の答えが説明していることです。
同型の定義は、（.） 、、、idまたはが何である=必要があるかを示していないことに注意してください。唯一の要件は、それらが何であれ、カテゴリ法も満たしていることです。
f . id = f
id . f = f
(f . g) . h = f . (g . h)
構成（すなわち（.））は、2つの射を1つの射に結合しid、ある種の「アイデンティティ」遷移を示します。これは、私たちの同型写像が同一性射idに打ち消される場合、それらを互いに逆と考えることができることを意味します。
射が関数である特定のケースではid、恒等関数として定義されます。
id x = x
...そして構成は次のように定義されます：
(f . g) x = f (g x)
id...そして2つの関数は、それらを構成するときに恒等関数に相殺される場合、同型です。
ただし、2つのオブジェクトが同型である可能性がある複数の方法があります。たとえば、次の2つのタイプがあるとします。
data T1 = A | B
data T2 = C | D
それらの間には2つの同型があります。
f1 t1 = case t1 of
A -> C
B -> D
g1 t2 = case t2 of
C -> A
D -> B
(f1 . g1) t2 = case t2 of
C -> C
D -> D
(f1 . g1) t2 = t2
f1 . g1 = id :: T2 -> T2
(g1 . f1) t1 = case t1 of
A -> A
B -> B
(g1 . f1) t1 = t1
g1 . f1 = id :: T1 -> T1
f2 t1 = case t1 of
A -> D
B -> C
g2 t2 = case t2 of
C -> B
D -> A
f2 . g2 = id :: T2 -> T2
g2 . f2 = id :: T1 -> T1
そのため、同型の法則を満たす2つのオブジェクト間には必ずしも一意の関数のペアが存在するとは限らないため、2つのオブジェクトではなく、2つのオブジェクトに関連する特定の関数の観点から同型を説明する方が適切です。
また、関数を反転可能にするだけでは不十分であることに注意してください。たとえば、次の関数ペアは同型ではありません。
f1 . g2 :: T2 -> T2
f2 . g1 :: T2 -> T2
作成時に情報が失われることf1 . g2はありませんが、最終的な状態が同じタイプであっても、元の状態に戻ることはありません。
また、同型は具体的なデータ型の間にある必要はありません。これは、2つの標準的な同型写像が具体的な代数的データ型の間になく、代わりに関数を単純に関連付ける例curryですuncurry。
curry . uncurry = id :: (a -> b -> c) -> (a -> b -> c)
uncurry . curry = id :: ((a, b) -> c) -> ((a, b) -> c)
同型写像の1つの使用法は、データ型を関数としてチャーチエンコードすることです。たとえば、は：Boolと同型です。forall a . a -> a -> a
f :: Bool -> (forall a . a -> a -> a)
f True = \a b -> a
f False = \a b -> b
g :: (forall a . a -> a -> a) -> Bool
g b = b True False
それとを確認しf . g = idますg . f = id。
チャーチエンコードデータ型の利点は、実行速度が速くなることがあり（チャーチエンコードは継続渡しスタイルであるため）、代数的データ型をまったくサポートしていない言語で実装できることです。
ある機能のあるライブラリの実装を別のライブラリの実装と比較しようとすることがあります。それらが同形であることを証明できれば、それらが同等に強力であることを証明できます。また、同型写像は、あるライブラリを別のライブラリに変換する方法を記述します。
たとえば、ファンクターの署名からモナドを定義する機能を提供する2つのアプローチがあります。1つはパッケージによって提供される無料のモナドであり、もう1つはfreeパッケージによって提供される操作的意味論operationalです。
2つのコアデータ型を見ると、特に2番目のコンストラクターは異なって見えます。
-- modified from the original to not be a monad transformer
data Program instr a where
Lift :: a -> Program instr a
Bind :: Program instr b -> (b -> Program instr a) -> Program instr a
Instr :: instr a -> Program instr a
data Free f r = Pure r | Free (f (Free f r))
...しかし、実際には同型です！つまり、両方のアプローチは同等に強力であり、一方のアプローチで記述されたコードは、同型を使用してもう一方のアプローチに機械的に変換できます。
また、同型写像は関数に限定されません。それらは実際にはすべてに対して定義されてCategoryおり、Haskellには多くのカテゴリがあります。これが、データ型よりも射の観点から考える方が便利な理由です。
たとえば、Lensタイプ（from data-lens）は、レンズを作成してIDレンズを使用できるカテゴリを形成します。したがって、上記のデータ型を使用して、同型である2つのレンズを定義できます。
lens1 = iso f1 g1 :: Lens T1 T2
lens2 = iso g1 f1 :: Lens T2 T1
lens1 . lens2 = id :: Lens T1 T1
lens2 . lens1 = id :: Lens T2 T2
2つの同型が関係していることに注意してください。1つは、各レンズ（つまりf1、g1）を構築するために使用される同型であり（これが、その構築関数が呼ばれる理由でもありますiso）、レンズ自体も同型です。上記の定式化では、.使用される合成（）は関数合成ではなくレンズ合成であり、idは恒等関数ではなく、恒等レンズであることに注意してください。
id = iso id id
つまり、2つのレンズを構成すると、その結果はそのアイデンティティレンズと見分けがつかなくなるはずです。
同型とは、 逆u :: a -> bを持つ関数です。つまり、次 の関係が成り立つ別の関数です。v :: b -> a
u . v = id
v . u = id
満足しています。それらの間に同型がある場合、2つのタイプは同型であると言います。これは基本的に、それらを同じタイプと見なすことができることを意味します - 一方でできることは、もう一方でもできます。
2つの機能タイプ
(a,b) -> c
a -> b -> c
と書くことができるので、同形です。
u :: ((a,b) -> c) -> a -> b -> c
u f = \x y -> f (x,y)
v :: (a -> b -> c) -> (a,b) -> c
v g = \(x,y) -> g x y
あなたはそれを確認することができu . v、v . u両方idです。実際、関数uとは、とvという名前の方がよく知られています。curryuncurry
newtype 宣言を使用するときはいつでも同形を利用します。たとえば、状態モナドの基礎となる型は、s -> (a,s)考えるのが少し混乱する可能性があります。newtype 宣言を使用すると、次のようになります。
newtype State s a = State { runState :: s -> (a,s) }
State s aに同形であり、それを使用するときに明確になる新しい型を生成しs -> (a,s)ます。変更可能な状態を持つ関数について考えています。新しい型の便利なコンストラクターStateとゲッターも取得します。runState
より高度な観点から、上で使用したcurryとuncurryを使用した同形を考えてみましょう。Reader r a型には newtype 宣言があります
newType Reader r a = Reader { runReader :: r -> a }
したがって、モナドのコンテキストではf、リーダーを生成する関数は型シグネチャを持ちます
f :: a -> Reader r b
これはと同等です
f :: a -> r -> b
これは、カレー/アンカレー同形の半分です。CoReader r aタイプを定義することもできます。
newtype CoReader r a = CoReader { runCoReader :: (a,r) }
コモンにすることができます。cobind という関数があります。=>>これは、coreader を受け取り、生の型を生成する関数を受け取ります。
g :: CoReader r a -> b
に同型である
g :: (a,r) -> b
a -> r -> bしかし、とが同型であることは既に見たので(a,r) -> b、自明でない事実が得られます: リーダー モナド (モナド バインドを使用) とコアリーダー コモナド (コモナド cobind を使用) も同型です! 特に、これらは両方とも同じ目的で使用できます。つまり、すべての関数呼び出しを介してスレッド化されるグローバル環境を提供するという目的です。
データ型の観点から考えてください。たとえば Haskell では、2 つのデータ型が同形であると考えることができます。これは、2 つのデータ型の間で一意の方法でデータを変換する関数のペアが存在する場合です。次の 3 つの型は互いに同型です。
data Type1 a = Ax | Ay a
data Type2 a = Blah a | Blubb
data Maybe a = Just a | Nothing
それらの間で変換される関数は、同型と考えることができます。これは、同型のカテゴリの考え方に適合します。betweenType1とwithのType22 つの関数が存在する場合f、その 2 つの関数はこれら 2 つの型 (オブジェクト) 間の同型です。gf . g = g . f = id