単純な代数データ型

これは、プログラマシリーズのカテゴリ理論の6番目の記事です。 以前の記事はすでにHabréで公開されています。
0.プログラマーのカテゴリー理論：序文
1.カテゴリ：構成の本質
2.タイプと機能
3.大小のカテゴリ
4.クレイズリーのカテゴリー
5.作品と副産物

前の記事では、型の基本操作である製品と連産品が考慮されました。 ここで、これらのメカニズムの組み合わせにより、日常のデータ構造の多くを構築できることを示します。 このような構造は、重要な応用価値があります。 たとえば、基本データ型の同等性をチェックでき、製品と連産品の同等性をコンポーネントの同等性に減らす方法を知っている場合、複合型の同等性演算子は自動的に導出できます。 Haskellでは、複合型の広範なサブセット、等価演算子と比較演算子、文字列との変換、および他の多くの操作が自動的に表示されます。

プログラミングにおける製品と型副産物の場所をより詳細に検討してみましょう。

製品の種類

プログラミング言語での型の積の標準的な実装はいくつかあります。 Haskellでは、カップルはプリミティブ型のコンストラクタですが、C ++では、標準ライブラリの比較的複雑なテンプレートです。

厳密に言えば、型の積は可換ではありません。同じデータが含まれていても(Bool, Int)代わりに型(Int, Bool)ペアを置き換えることはできません。 ただし、積は、 swap関数によって定義された同型まで可換であり、それ自体と逆です。

 swap :: (a, b) -> (b, a) swap (x, y) = (y, x) 

このようなペアは、ビッグエンディアンやリトルエンディアンなど、同じ情報を保存するための異なる形式と考えることができます。

あるペアを別のペアに投資することにより、好きなだけタイプを組み合わせることができます。 ネストされたペアがタプルと同等であることに気付くと、同じことが簡単に得られます。 これは、ペアの異なる埋め込み順序が互いに同型であるという事実の結果です。 （所定の順序で）3つのタイプa 、 b 、 c積に結合する2つの可能な方法があります。 すなわち

 ((a, b), c) 

または

 (a, (b, c)) 

これらの型は、最初の型の引数を予期する関数に2番目の型の引数を渡すことができないという意味で異なりますが、型の値は1対1で対応しています。 この表示を一方向に設定する関数は次のとおりです。

 alpha :: ((a, b), c) -> (a, (b, c)) alpha ((x, y), z) = (x, (y, z)) 

そして、これはその逆です：

 alpha_inv :: (a, (b, c)) -> ((a, b), c) alpha_inv (x, (y, z)) = ((x, y), z) 

したがって、型同型があります。 これらは、同じデータを再パッケージ化する異なる方法です。

型の積を二項演算として考えると、上記の同型はモノイドの連想法則に非常に似ていることがわかります。

 (a * b) * c = a * (b * c) 

唯一の違いは、モノイドでは両方の積が完全に同一であり、型については同型まで等しいことです。

この違いを重要でないと考えると、モノイドとの類推をさらに拡張し、singleton ()が型の乗算に関して中立要素であることを示すことができます。1が数値の乗算に関して中立であるように。 実際、タイプa要素に()を付加しても、情報は追加されません。 種類

 (a, ()) 

aと同型で、同型は関数によって与えられます

 rho :: (a, ()) -> a rho (x, ()) = x 

 rho_inv :: a -> (a, ()) rho_inv x = (x, ()) 

私たちの観察は、集合Setのカテゴリがモノイドである 、つまりオブジェクトの乗算（この場合はデカルト積）に関してモノイドであるというステートメントとして形式化できます。 厳密な定義を以下に示します。

Haskellには作品を定義するより一般的な方法があります。特に便利なのは、それらがタイプの合計と組み合わされるとすぐにわかるからです。 いくつかの引数を持つ名前付きコンストラクタを使用します。 たとえば、ペアの代替定義は次のようになります。

 data Pair ab = P ab 

ここで、 Pair abは他の2つの型aおよびbによってパラメーター化される型コンストラクターの名前であり、 Pはデータコンストラクターの名前です。 Pair型コンストラクターに2つの型を渡すことで特定の型を定義し、対応する型付きの値をPコンストラクターに渡すことでこの型のペアを作成します。 たとえば、 stmtをStringとBoolペアとして定義します。

 stmt :: Pair String Bool stmt = P "This statement is" False 

最初の行は型宣言です。 aとb代わりにStringとBool持つPair型コンストラクターで構成されます。 2行目は、データコンストラクターPを特定の行と論理値に適用することによって取得される変数の値を定義します。 繰り返しますが、型コンストラクタは型の構築に使用され、データコンストラクタは値の構築に使用されます。

Haskellの型とデータの名前空間は重複しないため、多くの場合、両方のコンストラクターに同じ名前が使用されます。 例えば

 data Pair ab = Pair ab 

Leninist squintのペアの組み込み型を見ると、実際には最後の宣言のトピックのバリエーションであることが認識され、 Pairコンストラクターのみが二項演算子(,)置き換えられます。 プレフィックス表記では、他の名前付きコンストラクターと同様に(,)を使用できます。

 stmt = (,) "This statement is" False 

同様に、 (,,)トリプルなどを構成します。

ジェネリックペアまたはタプルを使用する代わりに、特定のタイプの製品に個別の名前を入力できます。 例えば

 data Stmt = Stmt String Bool 

StringとBool製品ですが、独自の名前とコンストラクターがあります。 この定義の利点は、同じコンテンツで多くの型を持つことができますが、セマンティクスと機能が異なるため、型システムでは相互に混合できないことです。

タプルと複数引数コンストラクターのプログラミングは、混乱とエラーにつながることがよくあります。これは、どのコンポーネントが何に対して責任があるのか​​を追跡する必要があるためです。 コンポーネントに適切な名前を付けることができればより良いでしょう。 名前付きフィールドを持つ型の積はHaskellと呼ばれ、Cではstructです。

投稿

簡単な例を考えてみましょう。 化学要素は、2つの行（ラテン語名と記号）と原子質量に対応する整数で構成される単一の構造として説明します。 これを行うには、タプル(String, String, Int)を使用し、どのコンポーネントが何を担当するかを常に念頭に置くことができます。 タプルからコンポーネントを抽出するには、パターンマッチングを使用します。 次の関数は、化学元素の記号がラテン名の接頭辞であるかどうかをチェックします（たとえば、 Heは接頭辞のヘリウムです ）：

 startsWithSymbol :: (String, String, Int) -> Bool startsWithSymbol (name, symbol, _) = isPrefixOf symbol name 

このコードは間違いを犯しやすく、読み取りや保守が困難です。 タプルの代わりにレコードを定義する方がはるかに良いです：

 data Element = Element { name :: String , symbol :: String , atomicNumber :: Int } 

これらの表現は同型であり、次の相互逆変換を使用して検証できます。

 tupleToElem :: (String, String, Int) -> Element tupleToElem (n, s, a) = Element { name = n , symbol = s , atomicNumber = a } 

 elemToTuple :: Element -> (String, String, Int) elemToTuple e = (name e, symbol e, atomicNumber e) 

レコードフィールド名もアクセサ関数であることに注意してください。 たとえば、 atomicNumber eは、レコードe atomicNumberフィールドを返します。 したがって、 atomicNumber関数のタイプは次のとおりです。

 atomicNumber :: Element -> Int 

Element型のエントリを使用すると、 startsWithSymbol関数がより読みやすくなります。

 startsWithSymbol :: Element -> Bool startsWithSymbol e = isPrefixOf (symbol e) (name e) 

Haskellでは、 isPrefixOf関数を中置演算子に変え、逆アポストロフィでフラッシュするトリックを実行できます。 これにより、コードが読みやすくなります。

 startsWithSymbol e = symbol e `isPrefixOf` name e 

中置演算子の優先度は関数呼び出しの優先度よりも低いため、括弧を省略できました。

タイプの合計

セットのカテゴリ内の製品がタイプの製品を誘導する方法と同様に、coproductはタイプの合計を生成します。 Haskellの型の合計の標準的な実装は次のとおりです。

 data Either ab = Left a | Right b 

ペアと同様に、 Either可換（同型まで）でネストでき、埋め込みの順序は重要ではありません（同型まで）。 たとえば、3つのタイプの合計は次のようになります。

 data OneOfThree abc = Sinistral a | Medial b | Dextral c 

Setは、剰余演算操作に関して（対称）モノイダルカテゴリを形成することがわかります。 二項演算の場所は互いに素な和で占められ、中立要素が初期オブジェクトです。 タイプに関して、 Eitherはモノイドの操作であり、無人タイプVoidは中立的な要素です。 Eitherが加算で、 Voidがゼロであると仮定します。 実際、型の合計にVoidを追加しても、型の値のセットは変更されません。 例えば

 Either a Void 

a同型 実際、 Voidタイプには値が設定されていないため、 Right値を作成する方法はありません。 したがって、 Either a Void住民はLeft値のみで、これは型a値の単なるラッパーです。 象徴的に、これはa + 0 = aと書くことができます。

Haskellでは、型の合計は非常に一般的です。 C ++では、それらの類似体（アソシエーションまたはバリアント）は、いくつかの理由で使用される頻度がはるかに少なくなります。

まず、最も単純な型の合計はenumを使用してC ++で実装されるenumです。 同等の

 data Color = Red | Green | Blue 

C ++では

 enum { Red, Green, Blue }; 

型のさらに単純な合計

 data Bool = True | False 

C ++では、プリミティブ型のboolです。

さらに、値の有無をエンコードする型の合計は、空の文字列、負の数、nullポインターなど、「不可能な」値を持つさまざまなトリックを使用してC ++で実装されます。Haskellでは、 Maybe ：

 data Maybe a = Nothing | Just a 

Maybeタイプは、2つのタイプの合計です。 コンストラクターを精神的に別の型に変えます。 最初の形式は次のとおりです。

 data NothingType = Nothing 

このリストには、 Nothing単一の値が含まれています。 つまり、これはtype ()と同等のシングルトンです。 第二部

 data JustType a = Just a 

タイプaのラッパーです。 Maybe

 data Maybe a = Either () a 

型のより複雑な合計は、ポインターを使用してC ++で作成されます。 ポインターは、nullまたは特定の型の値を指すことができます。 たとえば、Haskellでは、リストは型の（再帰的な）合計として定義されます。

 List a = Nil | Cons a (List a) 

C ++では、同じタイプが次のように記述されます。

 template<class A> class List { Node<A> * _head; public: List() : _head(nullptr) {} // Nil List(A a, List<A> l) // Cons : _head(new Node<A>(a, l)) {} }; 

ここでのNULLポインターは空のリストをエンコードします。

HaskellのNilおよびConsコンストラクターは、同様の引数を持つ2つのオーバーロードされたListクラスコンストラクターになっていることに注意してください： Nilの場合は引数なし、 Cons値とリスト。 Listクラスには、タイプの合計のコンポーネントを区別するラベルは必要ありません。 代わりに、 _headに特別なnullptr値を使用してNilを表します。

HaskellとC ++の型の重要な違いは、Haskellではデータ構造が不変であることです。 オブジェクトが特定のコンストラクターを使用して作成された場合、どのコンストラクターとどの引数が使用されたかを永久に記憶します。 したがって、 Just "energy"として作成されたMaybeクラスのインスタンスは、 NothingラップすることはありNothing 。 同様に、空のリストは常に空のままであり、3要素リストには常に同じ3要素が格納されます。

イミュニティは、コンストラクターをリバーシブルにします。オブジェクトはいつでもコンポーネント部分に分解できます。 このような分解は、このコンストラクタまたはそのコンストラクタであるサンプルと比較することにより実行されます。 コンストラクター引数は変数名（または他のパターン）に置き換えられます。

List型には2つのコンストラクターがあるため、任意のList分解は2つの一致するパターンで構成されます。 最初のサンプルは空のNilリストに一致し、2番目のサンプルはCons作成されたリストに一致します。 たとえば、単純な関数を定義します。

 maybeTail :: List a -> Maybe (List a) maybeTail Nil = Nothing maybeTail (Cons _ t) = Just t 

maybeTail定義の最初の部分は、マッチングの参照としてNilコンストラクターを使用し、 Nothingを返します。 2番目の部分では、例としてConsコンストラクターを使用します。 サンプルの最初の引数はダッシュで表されます。これは、サンプルに含まれる意味に関心がないためです。 2番目の引数Consは変数t関連付けられています（以降、変数について説明しますが、厳密に言えば、変数は変更されません：値に関連付けられた変数が変更されない場合）。 このサンプルの関数の値はJust tです。 したがって、タイプList値の作成方法に応じて、パターンのいずれかに一致します。 Consを使用して作成された場合、関数はこの場合に使用される両方の引数を受け取ります（最初の引数は無視されます）。

より複雑な型の合計は、ポリモーフィッククラスの階層によってC ++で実装されます。 共通の祖先を持つクラスファミリは、仮想関数のテーブルがコンポーネントの暗黙的なラベルとして機能するタイプの合計として解釈できます。 Haskellがパターンマッチングとして機能するものは、ディスパッチ関数を呼び出すことでC ++で実装されます。

リーダーは、その過剰制限のために、型の合計としてunionを使用するC ++でめったに見つかりません。 このクラスにはコピーコンストラクターがあるため、 std::stringをunion入れることさえできません。

型代数

それとは別に、タイプの動作と合計により、多くの有用なデータ構造を定義できますが、実際の力はそれらの組み合わせにあります。

以上をまとめます。 型システムの基礎となる2つの可換モノイド構造を調べました。 これは、中立要素Voidを持つ型と中立要素を持つ型の積()の合計です。 それらを加算と乗算として想像すると便利です。 この場合、 Voidゼロで、 ()は1です。

この類推がどこまで広がっているか見てみましょう。 たとえば、ゼロを掛けるとゼロになるのは本当ですか？ 言い換えると、 Void上の型はVoid型と同型ですか？

たとえば、 IntとVoid構成されるペアはありますか？ ペアを作成するには、両方の値が必要です。 Int型の値は問題ではありませんが、 Voidには問題があります。この型には値が設定されていません（この型の値はありません）。 したがって、すべてのタイプaタイプ(a, Void)も設定されないため、 Voidと同等です。 つまり、 a*0 = 0です。

数値の加算と乗算は、分布法則によって関連付けられています。

 a * (b + c) = a * b + a * c 

タイプの和と積に対して実行されますか？ はい、同型まで。 IDの左側はタイプに対応します

 (a, Either bc) 

そして正しいもの

 Either (a, b) (a, c) 

型を相互に変換する関数を提示します：

 prodToSum :: (a, Either bc) -> Either (a, b) (a, c) prodToSum (x, e) = case e of Left y -> Left (x, y) Right z -> Right (x, z) 

 sumToProd :: Either (a, b) (a, c) -> (a, Either bc) sumToProd e = case e of Left (x, y) -> (x, Left y) Right (x, z) -> (x, Right z) 

コンストラクトのcase of 、関数内のパターンマッチングに使用されます。 矢印は、パターンとそれに対応する式を分離します。 たとえば、引数を指定してprodToSumを呼び出す場合

 prod1 :: (Int, Either String Float) prod1 = (2, Left "Hi!") 

e case e ofのe変数はLeft "Hi!" 。 "Hi!"置き換えて、 Left yパターンと一致し"Hi!" y代わりに。 変数x以前2に関連付けられていたため、構築のcase of結果（および関数全体）は、予想どおり、 Left (2, "Hi!")ます。

上記の関数が相互に逆であることの証明は、演習として読者に委ねられます。 あるフォーマットから別のフォーマットに同じデータを再パッケージするだけです。

分布則によって接続された2つのモノイドは、数学では半環と呼ばれます。 型の減算を決定できないため、これは完全なリングではありません。 自然数の半環に当てはまる一連のステートメントは、型に転送できます。 以下に例を示します。

数字	種類
0	Void
1	()
a + b	Either ab = Left a | Right b
a * b	(a, b)またはPair ab = Pair ab
2 = 1 + 1	data Bool = True | False
1 + a	data Maybe = Nothing | Just a

リストタイプは、方程式の解として定義されているため、特に興味深いものです。 定義されているタイプは、等式の両側にあります。

 List a = Nil | Cons a (List a) 

通常の置換を実行し、 List aをx置き換えて、取得します

 x = 1 + a * x 

型は減算または除算できないため、この方程式は従来の代数的手法では解決できません。 右側のx代わりに式(1 + a*x)再帰的に代入して、分布によって括弧を開きましょう。 ゲット

 x = 1 + a*x x = 1 + a*(1 + a*x) = 1 + a + a*a*x x = 1 + a + a*a*(1 + a*x) = 1 + a + a*a + a*a*a*x ... x = 1 + a + a*a + a*a*a + a*a*a*a... 

最終的に、無限の量の製品（タプル）に到達します。これは次のように解釈できます。リストは空、 1いずれかです。 いずれかが1つの要素で構成されます; いずれかのペア、 a*a構成されます。 またはトリプル、 a*a*aなどから正式に取得された定義は、文字列の代わりにリストの直感的なアイデアに完全に対応します。文字の代わりにタイプa値があります。

ファンクターと固定小数点を調べた後、リストとその他の再帰構造にさらに戻ります。

シンボリック変数で方程式を解くことは代数です！ したがって、そのようなデータ型は代数（ADT）と呼ばれます。

まとめると、型代数の非常に重要な解釈を与えます。 タイプaとタイプb積には、タイプb値とタイプb値の両方が含まれている必要があり、これは両方のタイプの母集団を意味することに注意してください。 一方、型の合計には、型b値または型b値のいずれかが含まれているため、少なくとも1つが入力されていれば十分です。 論理積と論理和の論理演算は、型環と以下の対応関係にある半環によって形成されます。

ロジック	種類
偽	Void
本当	()
|| b	Either ab = Left a | Right b
a && b	(a, b)

この類似性は深めることができ、論理と型理論の間のカリー-ハワード同型の基礎になります。 機能タイプを検討する場合、この問題に戻ります。

演習

1. Maybe aとEither () a同型であることを示す。
   
2. Haskellの次のタイプの合計を考えます。
   

    data Shape = Circle Float | Rect Float Float 

   
   Shapeタイプでarea関数を定義するには、パターンマッチングを使用します。
   

    area :: Shape -> Float area (Circle r) = pi * r * r area (Rect dh) = d * h 

   
   インターフェイスとしてC ++またはJavaでShapeを実装し、 CircleとRect 2つのクラスを作成します。 次に、 areaを仮想関数として書き込みます。
   
3. （続き） Shape周囲を計算する新しいcirc関数を簡単に追加できます。 Haskellでは、 Shapeタイプの定義は変更されません。 次のコードは、プログラムのどこにでも追加できます。
   

    circ :: Shape -> Float circ (Circle r) = 2.0 * pi * r circ (Rect dh) = 2.0 * (d + h) 

   
   C ++またはJavaプログラムにcircを追加します。 元のプログラムのどの部分を修正する必要がありましたか？
   
4. （続き）新しいSquareシェイプをShapeタイプに追加し、残りのコードを適切に更新します。 Haskellで何を変更する必要がありましたか？ C ++またはJavaはどうですか？ （Haskellを知らなくても、変更はかなり明白なはずです。）
   
5. 正式なアイデンティティa + a = 2 * aが型に対して成り立つことを示します（同型まで）。 型言語の2はBool対応することを思い出してください（上記の表を参照）。
   

謝辞

著者は、投稿と有用なコメントをレビューしてくれたGershom Bazermanに感謝しています。