「正整数を2つ受け取り、その最大公約数を返す関数」の型が付くことを確認してもらえばよいです。「正整数を2つ受け取り、その公約数を返す関数」の型を付けるところまでを目指します。複雑な型を読み解くのは難しいので、最初は弱い簡単な型を付けて、徐々に強くしていく方針で説明します。整数を2つ受け取って整数を返す関数であってほしいです。限らないという断り書きです。型の値を返す」という意味の型になります。あるプログラミング言語の関数の型の意味と同じです。intの型を持つかどうかF*コンパイラにチェックしてもらいます。a上のコードは無事型検査が通ります。型の値を返す関数」の型になります。停止して答えを返す関数であってほしいので、型シグネチャの部分を以下のように書き換えます。intこの例では残念ながら型検査を通りません。0などは停止せずに無限ループし続けるので当然です。そもそもそんな入力は受け付けたくないので、関数の定義域を絞ります。この種の型は型の中に値の情報が現れており、値に依存しているので、依存型と呼ばれます。値域を正整数に限ればたしかに停止するのですが、残念ながら型検査器はその証明を思いつけていないのです。そこで、人間がヒントを与える必要があります。停止性の証明のためには再帰的な呼び出しごとに真に減少するが無限減少列はないような値があることを型検査器に教えてあげればよいです。大きいことは確定しているし、良さそうです。このヒントを付けた型シグネチャが以下になります。%[a+b])これでもまだ型検査が通りません。辺りで証明が回らないよ!?などと、どこで検査に失敗したか教えてくれます。b)のペアで考えてみて!」と教えることにします。b])今度は無事に型がつきました。これでこの関数が確実に停止することが保証されました。いう別名が定義されています。よって、以下のように書くことも出来ます。公約数かどうか判定する関数を定義します。0)この関数を使って、欲しい仕様に対応する型シグネチャは以下のように書けます。b])なのですが、やっぱり型検査器は証明を見つけられません。公約数になってるかどうかわからないよ!とのことです。割り切ることは即座にわかります。割り切るかどうかの確認ではないかと予測します。割り切る」という補題を仮定します。必要な場所でコンパイラに教えてあげます。aこれをコンパイルすると無事に型がつきました。公約数を返すことが証明されました。b)くらいにすっきりさせることができます。意味がわかりやすくなりました。完成したプログラムはこちらです。あとがきなんとなく複雑な型を持つ言語の雰囲気が伝わったら幸いです。ちなみに今日は新暦七夕です。starの記事を書きました。myuon.github.io毎日興味深い話題がありドキドキがとまりません。*1:この場合でもコンパイラはヒントを鵜呑みにせず、そのヒントが正しいかどうかを検査してくれるので正しさは保証されます。整数を受け取って整数を返す関数のつもりで、私が以下の関数を書いたとします。"hello!"上のプログラムは当然コンパイルできますし、私は仕様どおり正しい実装を書けた気がしています。何も問題ありません...ほんとに?心配になったのでコメントに書かれていた仕様を型で書きなおすことにしました。"hello!"これをコンパイルしようとすると、コンパイラは以下のように間違いを指摘してくれます。整数型の式を書いてくれると思っていた場所に、文字列型の"hello!"という式が書いてあるよ!たったしかに〜〜〜!!全然気づかなかった!!!...というように、型を明示することで、式にその型を付けられるかどうかコンパイラがチェックしてくれます。型には「コンパイラからも読める仕様」「コンパイラがチェックしてくれる仕様」としての一面があるのです。プログラミング注意きちんとしたテストをしようと思ったのですが、途中でめんどくさくなりました。条件を揃えたりILを読んだりしてないので余り意味はないかもしれませんが、結果だけここにおいときます。処理をする関数を幾つかの方法で書き、速度を比較。与えられた整数列から十進表記中に"3"を含むものを除き5の倍数を除き十進表記中に現れる"57"を"91"に書き換え7の倍数を除きその数から始まるコラッツ列が1に到達するまでの長さを求めその和を返す比較項目LINQ/For文のどちらを使うかParallelにするかしないかOptimizationを有効にするかしないか与えられた仕様を素朴に書き下すか/やや工夫するかなどの条件を変えて実行時間を比較。以下値はいずれも[秒]。debugとreleaseの差はほとんどなかったので一部割愛。04.71ちゃんとした比較実験にするためにしなければならないこと各メソッドの内容をきちんと考える。何を固定して何を動かすのかIL(.netの中間言語)を読んで議論する思ったこと無駄の多いコードを書くと来世はきらら系4紙がない世界に転生してしまう。ブログを報告するスターをつけました引用をストックしましたストック一覧を見る閉じる引用するにはまずログインしてくださいログイン閉じる引用をストックできませんでした。再度お試しください閉じる限定公開記事のため引用できません。