単純な代数データ型

これは、プログラマシリーズのカテゴリ理論の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に感謝しています。