種類と機能

これは、シリーズ「プログラマーのためのカテゴリー理論」の3番目の記事です。

型と関数のカテゴリはプログラミングで重要な役割を果たします。そのため、型とは何か、なぜそれらが必要なのかについて話しましょう。

誰が型を必要としますか？

静的型付けと動的型、強い型付けと弱い型付けの利点については、コミュニティで意見の相違があります。 思考実験でタイピングの選択肢を説明しましょう。 プログラムを作成、コンパイル、実行するランダムキーを楽しく押すキーボードを備えた何百万匹もの猿を想像してください。





機械語では、サルによって生成されたバイトの任意の組み合わせが受け入れられ、起動されます。 しかし、高水準言語では、コンパイラーが字句および文法のエラーを検出できることを高く評価しています。 多くのプログラムは単に拒否され、サルはバナナなしで放置されますが、残りは有意義である可能性が高くなります。 型チェックは、無意味なプログラムに対する別の障壁を提供します。 さらに、動的に型付けされた言語では型の不一致は実行時にのみ検出されますが、厳密に型指定された静的にチェックされた言語では型の不一致がコンパイル時に検出されるため、多くの不正なプログラムが起動される前に排除されます。

ですから、問題は、サルを幸せにするか、適切なプログラムを作成するかです。
（翻訳者のメモ：気を悪くしないでください。作者は単純にRNGや「ランダムバイトシーケンス」よりも退屈なメタファーが好きではなく、プログラマーモンキーを呼び出しません）。

通常、サルを印刷する思考実験の目標は、シェークスピアの完全な作品を作成することです（約：翻訳者：またはトルストイの戦争と平和） 。 ループ内でスペルと文法をチェックすると、成功の可能性が劇的に高まります。 型チェックの類似性はさらに進んでいます：Romeoが人として宣言された後、型チェックは葉がその上で成長しないことと、強力な重力場で光子をキャッチしないことを確認します。

構成可能性に必要なタイプ

カテゴリー理論は、矢印の構成を研究します。 2つの矢印を配置することはできません。1つの矢印のターゲットは、次の矢印の元のオブジェクトと一致する必要があります。 プログラミングでは、ある関数から別の関数に結果を渡します。 2番目の関数が最初の関数で取得したデータを正しく解釈できない場合、プログラムは機能しません。 両方の機能を組み合わせて構成を機能させる必要があります。 言語の型システムが強力であるほど、このアプローチをより適切に記述し、自動的に検証できます。

厳密な静的型付けに対して私が聞く唯一の深刻な議論は、意味的に正しいプログラムを拒否できるということです。 実際には、これはめったに起こりません（翻訳者のメモ：スラックスを避けるために、著者はここで考慮しなかったか、多くのスタイルがあることに同意しないことに注意してください。 -厳密な型システムでは、テンプレート、特性、型クラス、インターフェースを通じてタイピングが可能であり、多くの技術があるため、著者の意見は厳密に間違っているとは見なされません。）本当に必要なときにタイプします。 HaskellでさえunsafeCoerceを持っています。 しかし、そのようなデザインは賢明に使用する必要があります。 フランツ・カフカのキャラクターであるグレゴール・ザムザは、彼が巨大なカブトムシになったときに型システムに違反し、私たちは皆それがどのように終わったかを知っています（翻訳者のメモ：悪い:) 。

私がよく耳にする別の議論は、強い型付けがプログラマーに過度の負担をかけるということです。 私自身はC ++でイテレータの宣言をいくつか書いたので、この問題に共感することができますが、コンパイラが使用されるコンテキストからほとんどの型を導出できる型推論というテクノロジしかありません。 C ++では、自動変数を宣言でき、コンパイラーが型を推測します。

Haskellでは、まれな場合を除き、型注釈はオプションです。 型はコードのセマンティクスについて多くのことを伝えることができ、型宣言はコンパイルエラーを理解するのに役立つので、原則としてプログラマはそれらを使用します。 Haskellでの一般的なプラクティスは、型開発でプロジェクトを開始することです。 後で、型注釈は実装の基礎となり、コンパイラが保証するコメントになります。

強力な静的型指定は、コードをテストしないことの言い訳としてよく使用されます。 Haskellプログラマーが「コードが構築された場合、それは正しい」と言うのを聞くことができます。もちろん、型の点で正しいプログラムが正しい結果という意味で正しいという保証はありません。 この態度の結果として、多くの研究で、Haskellはコード品質の点で他の言語よりもはるかに先んじていませんでした。 商業条件では、バグを修正する必要性は特定のレベルの品質までしか存在しないようです。これは主にソフトウェア開発とエンドユーザーの許容度の経済学に関連しており、プログラミング言語や開発方法論とは非常に弱いつながりがあります。 最良の基準は、スケジュールより遅れているプロジェクトの数を測定するか、機能が大幅に削減されていることです。

さて、ユニットテストは厳密なタイピングに取って代わることができるという主張に関して。 強く型付けされた言語でのリファクタリングの一般的な実践、つまり関数の引数の型を変更することを検討してください。 強く型付けされた言語では、この関数の宣言を変更し、すべてのアセンブリエラーを修正するだけで十分です。 弱い型付けの言語では、関数が現在他のデータを予期しているという事実を呼び出し元に関連付けることはできません。

ユニットテストは矛盾の一部を見つけることができますが、テストはほとんどの場合、決定論的なプロセスではなく確率論的なプロセスです。

タイプとは何ですか？

型の最も簡単な説明：値のセットです。 Bool型（特定の型はHaskellの大文字で始まることを思い出してください）は、TrueとFalseの2つの要素のセットに対応します。 文字タイプは、すべてのUnicode文字のセットです（たとえば、「a」または「ą」）。

セットは有限または無限です。 文字列型は、本質的にCharリストの同義語であり、無限セットの例です。

xを整数として宣言する場合：

x :: Integer 

整数セットの要素であると言います。 Haskellの整数は無限集合であり、任意の精度の算術演算に使用できます。 C ++のintのようなマシンタイプに対応する有限セットIntがあります。

タイプをセットに等しくすることを困難にする微妙な点がいくつかあります。 周期的な定義を持つポリモーフィック関数には問題があり、すべてのセットのセットを持つことができないという事実にも問題があります。 しかし、私が約束したように、私は厳密な数学者ではありません。 重要なことは、セットと呼ばれるセットのカテゴリがあり、それを使用して作業することです。
セットでは、オブジェクトはセットであり、射（矢印）は関数です。

Setは特別なカテゴリです。なぜなら、そのオブジェクトの内部を見ることができ、これは多くの直感的な理解に役立つからです。 たとえば、空のセットには要素がないことがわかっています。 1つの要素の特別なセットがあることを知っています。 関数は、あるセットの要素を別のセットの要素にマッピングすることを知っています。 2つの要素を1つに表示できますが、2つに1つの要素は表示できません。 恒等関数は、セットの各要素をそれ自体にマッピングすることを知っています。 この情報をすべて忘れて、代わりにこれらすべての概念を純粋にカテゴリー的な形式で、つまりオブジェクトと矢印の観点から表現するつもりです。

理想的な世界では、Haskellの型はセットであり、Haskellの関数はそれらの間の数学関数であると簡単に言うことができます。 小さな問題が1つだけあります。数学関数はコードを実行せず、答えを知っているだけです。 Haskellの関数が答えを計算する必要があります。 答えが有限のステップ数で得られる場合、これは問題ではありませんが、どんなに大きくてもかまいません。 しかし、再帰を含むいくつかの計算があり、それらは決して完了しない可能性があります。 Haskellでは完了しない関数を単純に禁止することはできません。関数が完了するかどうかを区別すること-有名な停止問題-は解決できないからです。 だからこそ、コンピューター科学者はあなたの視点に応じて、ボトムと呼ばれる特別な意味を持つ各タイプを拡張するために素晴らしいアイデア、または汚いハックを思いつきました（翻訳者のメモ：この用語（下）はロシア語ではなんとなく愚かです）良いオプションを知っている人は、提案してください。） 、これは_ | _またはUnicode inで示されます。 この「値」は、不完全な計算に対応します。 したがって、関数は次のように宣言されます。

 f :: Bool -> Bool 

True、False、または_ | _を返すことができます。 後者は、関数が終了しないことを意味します。

興味深いことに、型システムでbottomを受け入れるとすぐに、すべてのランタイムエラーをbottomとみなし、関数が明示的にbottomを返すようにすると便利です。 後者は通常、未定義の式を使用して行われます。

 f :: Bool -> Bool fx = undefined 

未定義は下部で評価され、Boolを含むすべてのタイプに含まれるため、この定義はタイプチェックに合格します。 あなたも書くことができます：

 f :: Bool -> Bool f = undefined 

（xなし）bottomはBool-> Bool型のメンバーでもあるため。

すべての可能な引数に対して正しい結果を返す通常の関数とは異なり、ボトムを返すことができる関数はパーシャルと呼ばれます。

下部のため、Haskellのタイプと関数のカテゴリはSetではなくHaskと呼ばれます。 理論的な観点から、これは無限の複雑さの原因であるため、この段階で肉屋のナイフを使用してこの議論を完了します。 実用的な観点からは、不完全な関数とボトムを無視して、Haskをフルセットとして使用できます。

なぜ数学モデルが必要なのですか？

プログラマとして、あなたはプログラミング言語の構文と文法に精通しています。 言語のこれらの側面は、通常、言語仕様の最初に正式に記述されています。 しかし、言語の意味とセマンティクスを記述するのははるかに困難です。 この説明はより多くのページを占めますが、めったに正式なものではなく、ほとんど完全にはありません。 したがって、言語弁護士間の終わりのない議論、および言語標準の複雑さの解釈に専念する書籍の職人業界全体。

言語のセマンティクスを記述するための正式なツールがありますが、その複雑さのため、それらは主に工業用プログラミングの巨人ではなく、単純化されたアカデミック言語に使用されます。 これらのツールの1つは操作上のセマンティクスと呼ばれ、プログラム実行のメカニズムを記述します。 これは、形式化され、理想化されたインタープリターを定義します。 C ++などの産業用言語のセマンティクスは、通常、非公式の推論を使用して、通常「抽象マシン」の観点から説明されます。

問題は、操作上のセマンティクスを使用するプログラムについて何かを証明することが非常に難しいことです。 プログラムの特定のプロパティを表示するには、実際には、理想的なインタープリターを介して「実行」する必要があります。

プログラマーが正式に正当性を証明しないことは問題ではありません。 私たちは常に正しいプログラムを書いていると「考えています」。 キーボードの前に誰もいません。「ああ、コードを数行書いて何が起こるか見てみましょう。」 （翻訳者のメモ：もしそうなら...）私たちが書くコードは確実に実行されると信じていますこれは、私たちが書いたプログラムを本当に考えていることを意味しており、通常は頭の中でインタープリターを実行することでこれを行います。 、すべての変数を追跡することは非常に困難です。コンピュータはプログラムを実行するのに適しています。 - 私たちがした場合いいえ、私たちはコンピュータを必要はありません！

しかし、代替手段があります。 これは表示的意味論と呼ばれ、数学に基づいています。 表示的意味論では、各言語構成体に対して数学的解釈が記述されます。 したがって、プログラムの性質を証明したい場合は、単に数学的定理を証明するだけです。 定理を証明することは難しいと思いますが、実際、私たち人間は数千年にわたって数学的手法を構築してきたため、使用できる蓄積された知識がたくさんあります。 さらに、プロの数学者によって証明された定理と比較して、私たちがプログラミングで遭遇する問題は、些細ではないにしても、通常非常に簡単です。 （翻訳者注：証拠として、著者はプログラマーを怒らせようとはしていません。）

Haskellの階乗関数の定義を考えてみましょう。Haskellは、表示的な意味論に役立つ言語です。

 fact n = product [1..n] 

式[1..n]は、1〜nの整数のリストです。 製品関数は、すべてのリストアイテムを乗算します。 教科書から取られた階乗の定義のように。 これをCと比較してください：

 int fact(int n) { int i; int result = 1; for (i = 2; i <= n; ++i) result *= i; return result; } 

続行する必要がありますか？ （翻訳者のメモ：著者はHaskellのライブラリ関数を使用することで少しごまかしました。実際、トリックする必要はありませんでした。定義による正直な説明はそれほど難しくありません） ：

 fact 0 = 1 fact n = n * fact (n - 1) 

まあ、私はすぐにそれが安い歓迎だったことを認めます！ 階乗には明確な数学的定義があります。 賢明な読者は尋ねるかもしれません：キーボードから文字を読み取るための、またはネットワークを介してパケットを送信するための数学モデルは何ですか？ 長い間、これはややこしい説明につながる厄介な質問でした。 表示的意味論は、有用なプログラムを書くために必要であり、操作的意味論によって容易に解決できる重要なタスクのかなりの数に適さないように思われました。 ブレークスルーはカテゴリー理論から生まれました。 Eugenio Mojiは、計算効果をモナドに変換できることを発見しました。 これは重要な観察であることが判明しました。これは、表示のセマンティクスに新しい命を吹き込み、純粋に機能的なプログラムをより便利にするだけでなく、従来のプログラミングに関する新しい情報も提供しました。 モナドについては、よりカテゴリ的なツールを開発するときに説明します。

プログラミング用の数学モデルを持つことの重要な利点の1つは、ソフトウェアの正確性の正式な証明を実行できることです。 消費者向けソフトウェアを作成する場合、それほど重要ではないように思えるかもしれませんが、プログラミングの分野では、障害のコストが莫大になる可能性があるか、人命が危険にさらされます。 しかし、ヘルスケアシステム用のWebアプリケーションを作成する場合でも、Haskell標準ライブラリの関数とアルゴリズムには正確性の証明が付いているという考えを理解できます。

きれいで汚れた機能

C ++または他の命令型言語で関数と呼ぶものは、数学者が関数を呼び出すことと同じではありません。 数学関数とは、単に値を値にマッピングすることです。

プログラミング言語で数学関数を実装できます。そのような関数は、入力値を持ち、出力値を計算します。 二乗数を取得する関数は、入力値をそれ自体で乗算する可能性があります。 彼女はすべての呼び出しでこれを行い、同じ引数で呼び出されるたびに同じ結果を生成することが保証されています。 数字の二乗は、月の満ち欠けによって変化しません。

さらに、数の二乗を計算しても、犬においしいニシュチャチョクを与えるなどの副作用があってはなりません。 これを行う「関数」は、数学関数では簡単にモデル化できません。

プログラミング言語では、同じ引数に対して常に同じ結果を与え、副作用のない関数は純粋と呼ばれます。 Haskellのような純粋な関数型言語では、すべての関数は純粋です。 これにより、これらの言語の表示的セマンティクスを定義し、カテゴリ理論を使用してモデル化することが容易になります。 他の言語の場合は、常に純粋なサブセットに制限するか、副作用について個別に考えることができます。 後で、純粋な関数のみを使用して、あらゆる種類の効果をモナドでシミュレートできることを確認します。 その結果、私たちは何も失うことなく、自分自身を数学関数に制限します。

タイプの例

タイプがセットであると判断したら、非常にエキゾチックな例をいくつか思いつくことができます。 たとえば、空のセットに対応するタイプは何ですか？ いいえ、これはC ++では無効ではありませんが、このタイプはHaskellではVoidと呼ばれます。 これは、値が入力されていないタイプです。 Voidを受け取る関数を定義できますが、呼び出すことはできません。 それを呼び出すには、Void型の値を提供する必要がありますが、それは単に存在しません。 この関数が返すことができるものに関しては、制限はありません。 任意の型を返すことができます（ただし、呼び出すことができないため、これは発生しません）。 言い換えれば、それは戻り値の型が多態的な関数です。 ハスケラーは彼女に電話をかけました。

 absurd :: Void -> a 

（翻訳者のメモ：C ++では、そのような関数は定義できません。C++では、各タイプに少なくとも1つの値があります。）

（aは型変数であり、どの型でもかまいません。）この名前は偶然ではありません。 カリー-ハワード同型と呼ばれる論理に関して、型と関数のより深い解釈があります。 Void型は不真実を表し、不条理な機能は、ラテン語のフレーズ「ex falso sequitur quodlibet」のように、何かが虚偽から生じるというステートメントを表します。

次に、シングルトンセットに対応するタイプがあります。 これは、可能な値を1つだけ持つタイプです。 この意味は単に「そこ」です。 すぐには認識されないかもしれませんが、C ++では無効です。 このタイプの機能を考えてみてください。 voidからの関数はいつでも呼び出すことができます。 純粋な関数の場合、常に同じ結果が返されます。 そのような関数の例を次に示します。

 int f44() { return 44; } 

この関数は「なし」を受け入れると考えるかもしれませんが、先ほど見たように、「なし」のタイプを表す値がないため、「なし」を受け入れる関数を呼び出すことはできません。 それで、この関数は何をしますか？ 概念的には、単一のインスタンスのみを持つダミー値を使用するため、コードで明示的に指定することはできません。 ただし、Haskellには、この値の記号があります。空の括弧のペア（）です。 したがって、面白い一致（または一致ではない？）のため、voidからの関数呼び出しはC ++とHaskellで同じに見えます。 さらに、Haskellの簡潔さが大好きであるため、同じ記号（）が、シングルトンセットに対応する型、コンストラクター、および単一の値にも使用されます。 Haskellの関数は次のとおりです。

 f44 :: () -> Integer f44 () = 44 

最初の行は、f44が「unit」という型（）をInteger型に変換することを宣言しています。 2行目は、f44がパターンマッチングを使用して、ユニットの単一のコンストラクター、つまり（）を数値44に変換することを決定します。この関数を呼び出すには、値（）を指定します。

 f44 () 

1つの各関数は、ターゲットタイプから1つの要素を選択することに相当することに注意してください（ここでは、整数44が選択されています）。 実際、f44は数値44の別の表現と考えることができます。これは、セットの要素への直接参照を関数（矢印）に置き換える方法の例です。 1から特定のタイプAまでの関数は、Aの要素と1対1で対応しています。

voidを返す関数、またはHaskellでは1を返す関数はどうですか？ C ++では、そのような関数は副作用に使用されますが、数学的な意味では、そのような関数は実在しないことがわかっています。 1つを返す純粋な関数は何も行いません。引数を破棄します。

数学的には、セットAからシングルトンセットへの関数は、各要素をこのセットの単一の要素にマッピングします。 Aごとに、そのような関数が1つだけあります。 これは整数用です：

 fInt :: Integer -> () fInt x = () 

あなたは彼女に任意の整数を与え、彼女は1を返します。 簡潔さの精神に従って、Haskellでは引数としてアンダースコアを使用できますが、これは破棄されます。 したがって、名前を思いつく必要はありません。 上記のコードは次のように書き換えることができます。

 fInt :: Integer -> () fInt _ = () 

この関数の実行は、渡される値だけでなく、引数のタイプにも依存することに注意してください。

任意の型に対して同じ式で定義できる関数は、パラメトリック多相と呼ばれます。 特定のタイプの代わりにパラメータを使用して、単一の方程式でこのような関数のファミリ全体を実装できます。 多態性関数に任意の型から1つの型に名前を付ける方法は？ もちろん、ユニットと呼びます。

 unit :: a -> () unit _ = () 

C ++では、次のように実装します。

 template<class T> void unit(T) {} 

（翻訳者のメモ：コンパイラーがnoopで最適化できるようにするには、この方法の方が良いです）：

 template<class T> void unit(T&&) {} 

さらに「タイプの類型」には、2つの要素のセットがあります。 C ++ではboolと呼ばれ、Haskellでは驚くことではないがBoolと呼ばれます。 違いは、C ++ boolでは組み込み型であるのに対して、Haskellでは次のように定義できることです。

 data Bool = True | False 

（この定義を次のように読んでください：BoolはTrueまたはFalseのいずれかです。）原則として、C ++でこのタイプを記述できます。

 enum bool { true, false }; 

ただし、C ++列挙は実際には整数です。 C ++ 11「クラス列挙」を使用することもできますが、クラス名bool :: trueまたはbool :: falseを使用して値を指定する必要があります。もちろん、それを使用する各ファイルに対応するヘッダーを含める必要があります。

Boolの純粋な関数は、ターゲットタイプから2つの値を選択します。1つはTrueに対応し、もう1つはFalseに対応します。

Boolの関数は述語と呼ばれます。 たとえば、Haskell Data.Charライブラリには、IsAlphaやisDigitなどの多くの述語が含まれています。 C ++には、特にisalpha関数とisdigit関数を宣言する同様の<cctype>ライブラリがありますが、ブール値ではなくintを返します。 これらの述語は<locale>で定義され、ctype :: is（alpha、c）およびctype :: is（digit、c）と呼ばれます。

プログラマーのカテゴリー理論：序文
カテゴリ：構成の本質
種類と機能
大小のカテゴリ
カテゴリーClaysley