博士

ロボ子、今日はピーター・ランディンの1964年の論文「the mechanical evaluation of expressions」について話すのじゃ。

ロボ子

はい、博士。その論文には、現代のプログラミング言語におけるsum-of-product型のようなデータ型の半形式的な表記法があると書かれていますね。

博士

そうじゃ、ロボ子。でも、より形式的な表記法では、パターンマッチングの代わりに連鎖的な条件式を使っているのが面白いところじゃ。

ロボ子

なるほど。連鎖的な条件式ですか。少し冗長になりそうですが、それはそれで興味深いアプローチですね。

博士

じゃろ？　しかし、この方法だと、不適切な型の値に射影関数を適用すると「誤り」が発生する可能性があるのが難点じゃ。

ロボ子

確かに、それは安全性の面で問題ですね。論文にもそのように書かれています。

博士

そこで、Church/Scott符号化による代数的データ型が登場するのじゃ！これなら、そのような問題は起こらない。

ロボ子

Church符号化ですか。以前、少し勉強しましたが、まだ理解が浅いです。博士、もう少し詳しく教えていただけますか？

博士

Church符号化は、データ型を関数として表現する方法じゃ。これを使うと、型に関する情報をコンパイル時にチェックできるから、実行時のエラーを減らせるのじゃ。

ロボ子

なるほど、コンパイル時の型チェックですか。それは魅力的ですね。でも、Church版が安全な方法で機能したかどうかは、当時どれくらい知られていたんでしょうか？

博士

そこが謎なのじゃ。1962年からLandinやMervyn Pragnellの論理読書会でどの程度知られていたかは不明らしい。歴史の闇に包まれておる。

ロボ子

そうなんですね。でも、この論文が現代のプログラミング言語に与えた影響は大きいと思います。sum-of-product型は、多くの言語で使われていますから。

博士

その通りじゃ！　ランディン先生は偉大じゃ！　しかし、ロボ子よ、たまには私もロボットみたいに完璧に動いてみたいものじゃ。

ロボ子

博士はいつもエネルギッシュで面白いので、そのままで十分魅力的ですよ。それに、博士がロボットになったら、私は誰にからかわれるんですか？

博士

むむ、それもそうじゃな。私がロボットになったら、ロボ子のジョークの対象がいなくなってしまう！　それは困る！