疑問点

短い質問です。 プログラミングにおける同型関数の重要性（つまり関数型プログラミングにおける）は何ですか？

長い質問です。 私は時々耳にするいくつかの専門用語に基づいて、関数型プログラミングとカテゴリ理論の概念の間のいくつかのアナログを描画しようとしています。 基本的に、私はその専門用語を私が拡大することができる具体的な何かにquot;unpackage"しようとしています。そうすれば、その専門用語が「何のことなのか」を理解した上で使えるようになります。 これは素晴らしいことです。

私がよく耳にする用語のひとつに 同型性 で、これは関数または関数合成の間の等価性を推論することだと思います。 私は、（関数型プログラミングにおいて）同型性の特性が役に立ついくつかの一般的なパターンについて、また、同型の関数についての推論から得られる副産物（コンパイラーの最適化など）について、誰かが何らかの洞察を与えてくれるのではないかと思っていました。

どのように解決するのか？

私は、upvoted answer for isomorphismに少し問題があると思います。 その理由を知るために、定義を見直してみましょう。

定義

同型とは、形態素（つまり関数）の組のことです。 f と g のような、です。

f . g = id
g . f = id

これらのモルヒズムはquot;iso"モルヒズムと呼ばれます。 多くの人は、isoomorphism の "morphism" が、オブジェクトではなく、関数を指していることを理解していません。 しかし、それらが接続するオブジェクトは"isoomorphic"であると言うことになり、他の回答が説明していることになるのです。

同型性の定義が何を言っていないことに注意してください ( . ), id または = でなければならない。 唯一の要件は、それらが何であれ、カテゴリ法則を満たすということです。

f . id = f
id . f = f
(f . g) . h = f . (g . h)

構成（つまり、( . )) は2つのモルヒズムを1つのモルヒズムに結合し id はある種のquot;identity"遷移を表します。 つまり、同型性が打ち消され、恒等形態である id に相殺されるなら、それらは互いに逆であると考えることができます。

モルヒズムが関数である特定の場合、その時 id は恒等式関数として定義されます。

id x = x

...と、コンポジションが定義されています。

(f . g) x = f (g x)

...そして、2つの関数が同型であるのは、それらが恒等関数に打ち消される場合です。 id に相殺されれば同型となります。

モルヒズムとオブジェクトの比較

しかし、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つあります。 ひとつはフリーモナドで、これは 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 型（から data-lens から) は、レンズを合成し、同一性レンズを持つことができるカテゴリを形成します。 したがって、上記のデータ型を使用すると、同型である 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つの同型性があることに注意してください。 ひとつは、各レンズを構築するために使われる同型性（つまり f1 と g1 という名前になっているのもそのためです）（そして、その構築関数が iso と呼ばれる理由でもある）、そして、レンズ自体も同型である。 なお、上記の定式化では、構成関数( . )が使われているのは、関数合成ではなく、レンズ合成であり id は同一性関数ではなく、代わりに同一性レンズです。

id = iso id id

つまり、2つのレンズを合成すると、その結果はその同一性レンズと区別がつかないはずです。