型！ 型！

誰？

　minamiyama1994です、不審者です

これは何？

　comb meet up!というLT大会で発表した型！　型！という同名のスライドに関する補足記事的なものです
　U22が中心ですが、中高生から社会人まで幅広く参加する勉強会ということで基本的なことを説明しました、分かる人にはつまらない話かと思います

まず、型って何よ？

「TAPLの第1章読め」の一言で済む話なのですが、それではあまりに無慈悲なので少し解説します(TAPL読めって言ってたらそもそもこの発表や記事なくてもいいもんね)
　型というのは

• 値の取りうる集合
• データに対するメタ情報

です
　……何を言っているかわからないと思うので具体例を出します

• 「0」は「整数型」です
• 「"hoge"」は「文字列型」です
• 「http://b-world.org」は「URL型です」です

　要するにこういうのが型です

「値の取りうる集合」とは？

　例えばint型であれば
int = { -2147483648 , -2147483647 , ... , -1 , 0 , 1 , ... , 2147483646 , 2147483647 }
みたいな感じです
　「どんな値を取りうるか？」というのを制限するのが型なので、逆に言えば型というのはどんな値を取りうるかの集合なわけです

「データに対するメタ情報」とは？

　0という値に対してはintと言うメタ情報が付いているわけです、このメタ情報のことを「型」と呼ぶわけです

型があると何が嬉しいのか？

　「エラー検知」です、「プログラムに対する保証」とも言います
　どういうことかというと、簡単にいえば「URL×文字列」と言った「そもそも意味が不明な計算」を、実際に計算が行われる前に、「型」と言うメタ情報を元に未然に弾くことができる、ということです

動的型付け静的型付け

　「型」というのは「エラー検知システム」であり「プログラムに対する保証を行う仕組み」なわけですけれども、問題として「いつそのエラー検知/保証を行うのか」というのがあります
　これに関して

• 実行しながら動的に行うのが動的型付け言語
• 実行前にコンパイル次に静的に行うのが静的型付け言語

と言う大別して2種類の戦略があるわけです

動的型付け言語

　エラー検知が実行時まで遅れます、肝心の型の存在意義(エラー検知)を打ち消すような特性です、なにせ実行しないとエラーにならないのですから
　ただ、ホットスワップ(動いているプログラムに対して動的にモジュールを入れ替える操作)などに対して強くしやすい、とか、「全体として整合性がとれているわけではないけどとりあえず動かしたい」と言う時に動かしやすい、とか、メリットが皆無なわけではないです

静的型付け言語

　エラー検知を実行前にコンパイル時に行います、型の強みが十全に行かせる戦略といえるでしょう
　しかし、ホットスワップや「壊れた状態で動かしたい」と言う時に柔軟性が無いことが多いです、「とりあえず今は動かせればいい」という時にはちょっと型がうるさいかもしれません

型に関する諸概念

　発表では

• ダックタイピング
• 多相型
• 代数的データ型
• 依存型
• 線形型

について説明しました、なんでこういうセレクションなんだというツッコミに関してはノーコおメントでお願いしたいと思います

ダックタイピング

　Rubyなど動的型付け言語で多用される戦略です
　例えば以下のコードを見てみましょう

def to_string(value)
  value.to_s
end

　何の変哲もない、引数を文字列にする関数です
　しかしここで大事なのは、「valueに対して型を指定していない」ということです
　ここでvalueに要求されるのは「to_sというメソッドを持っていること」だけです、それさえ満たしていればほかがどうであろうと関係ありません
　こういう「ある属性を保持していればなんでもいい」というのを「動的に」行うのをダックタイピングといいます
　「アヒルのように泣き、アヒルのように振る舞うのはアヒルである」という考え方に基づいているためこう呼ばれます

多相型

　本来なら「パラメトリック多相」と呼ぶべきものなのですが、ツッコミはナシでお願いします＞＜
　ダックタイピングが「要件を満たしていればなんでもいいや(実行時)」だったのに対し、こちらは「要件を満たしていればなんでもいいや(コンパイル時)」みたいなものです
　ダックタイピングだと目的のメソッドが無かったりしたら「実行時に」エラーが投げられたりするわけですが、パラメトリック多相だとコンパイル時に目的の操作が許可されているかどうかチェックされます
　以下は例です

toString :: Show a => a -> String
toString value = show value

　aと言うのは具体的な型ではありません、「何か型」ぐらいの意味合いです
　Show a =>と言うのは「Showという要件を満たしている型aに対して」ぐらいの意味合いで、aに対する制約条件のようなものです
　これは型としてあって、コンパイル時に静的にチェックされます
　こういう制約条件が書けない(or難しい)言語もあります、C++とか
　以下がC++での例です

template < typename T >
auto to_string ( const T & value ) -> std::string
{
    return boost::lexical_cast < std::string > ( value ) ;
}

　ここで、「T型の値はboost::lexical_castが適用できる」という条件は型には書いてありません
　しかしそういう言語でも、結局型がおかしいとコンパイル時にエラーになったりします、この場合だと関数本体のコードで結局boost::lexical_castを適用させているので、適用できない型Tだとその部分でコンパイルエラーになります

代数的データ型

　集合論では「直和」とか「直積」とかあったりします
　これを型にも活かした考え方が「代数的データ型」です、Haskellなどで実用的に使われています
　直和型とか直積型とかのワードで検索すると幸せになれるかも

依存型

　「値に型が依存している型」です、Coq、やC++などでありますor実現できます
　型の中に「0」や「"hoge"」などの「値」が含まれており、これらの値が違うと型としても違うものとして認識されます
　HogeType 0とHogeType 1は違うということです

線形型

　「その値が何回使われうるか」というのを型情報に含めたものです
　最適化に使われたりするそうです

定理証明系

　定理証明系と呼ばれる一群の言語があります
　CoqとかAgdaとかIdrisとかです
　これらの言語はどういうものかというと「型を使って証明を行う」というものです
　まず前提知識として「カリーハワード対応」というものを知っておく必要があります

カリーハワード対応

　「命題は型に対応し、証明はプログラムに対応する」というものです
　これだけだと何が何やらわからないので、具体例を出します

hoge :: [ a ] -> Int
hoge l = length l

　リストの長さを求める関数です
　この関数の型を見てみましょう、「何かリストを受け取り整数を返す関数型」ですね
　これが実装可能ということは、「何かリストがあればそれを元に整数を返す妥当な処理が存在する」ということです、この場合であればlength関数ですね
　読み替えると「「リスト」というのが成り立てば「整数」というのが導き出せる」となります
　一般化しましょう

hoge :: a -> b

　こういう型の関数があるとして、ここから分かるのは「aが与えられたらbを求める妥当な処理(プログラム)がある」ということです
　読み替えると「aが成り立てばbが成り立つ」ということです
　これが「型が命題に対応する」と言うことです
　そして、こういう型の関数が存在するということは、それを導き出す処理(プログラム)が存在するわけです
　読み替えると、こういう命題が存在するということは、それを導き出す証明が存在するということです
　型↔命題
　プログラム↔証明
　これが「カリーハワード対応」というものです

定理証明系―具体例

　カリーハワード対応という武器があるので、型で証明できることがわかりました
　そして、これを実現し、型で証明するための専用の言語があります、先程も述べたCoqなどです
　具体例をあげます

Goal forall A B C : Prop , ( A -> B ) -> ( B -> C ) -> ( A -> C ).
Proof.
  intros.
  apply H0.
  apply H.
  apply H1.
Qed.

　何をしているのかというと、いわゆる三段論法が成り立つことの証明です
　こういった言語では型の表現力が強く、「等号」「不等号」といったものまで型として表現されていたりします

定理証明系で嬉しい事

　定理証明系では型で証明を行います
　型はコンパイラが機械的にチェックを行います
　つまり、証明がコンパイラにより機械的にチェックされるのです
　手書きの証明だと、読み逃しや記述ミス等が発生しえますが(実際にフェルマーの最終定理ではその手のミスで1年間が潰れたりなどありましたね)、定理証明系による証明であればその手のミスは発生し得ないということです

定理証明系の実用例

　実用的な意味だと、例えば4色問題がCoqにより証明されていたりします
　また、手前味噌ながら、先日僕がqsortアルゴリズムの実装とその性質についての証明を行ったものを紹介しておきます
https://gist.github.com/minamiyama1994/bffdb2fa0be211302b92

終わりに

　以上が、comb meet up!で発表した型！　型！という同名のスライドに関する補足記事です
　スライドは150枚を5分ですっ飛ばすというものだったので、頭に入ってこない人もいたと思いますが、こちらの記事も参考にしていただければと思います
　質問はコメントかもしくはminamiyama1994でお願いします