構造的部分型と有界量化に関する型推論

  • 27
    Like
  • 4
    Comment

数式が多いためPDFで書いてしまいました.置き場所は今後変わるかもしれません:

文書本体(PDF, 約345KB.いきなりダウンロードされる場合もありますので注意)
http://github.com/gfngfn/Macrodown/wiki/pdf/subtyping/subtyping.pdf

更新履歴 備考
2016/12/24 公開
2016/12/29 誤植修正 (@magicant さんのご指摘により)
2017/01/02 誤植・内容修正 (@nekketsuuu さんのご指摘により)
2017/01/02 同上

(建設的な誤謬・誤植の指摘等,大変歓迎致します.)

以下にPDFの冒頭を念のため貼っておきます:

言語処理系を自らの手で実装するとなれば,レコード構造的部分型を入れたくなるのが人の性です.そして折角ならできるだけ強い型推論と多相型の機能を持たせてみたい,と考えるのも至極当然なことです.

ここまではほとんどの方が認める前提かと思いますが[要出典],それなりに古くから研究されているのに反して意外に構造的部分型に関する型推論の知見は和文で共有されていません.例えば原著・和訳ともに良書として広く知られている Types and Programming Languages と『型システム入門』は,構造的部分型の理論は登場するものの,構造的部分型を含めた型推論の実装については述べられていないようです.

「論文を探してみようか」と思っていたところ,和文でも『プログラミング言語の基礎理論』(絶版)に記述があるという旨を @fetburner さんから教えてもらい,たまたま該当書物を所持していながら前の方しか読んでいなかった筆者は嬉々として該当箇所を参照し,今回この文書に簡単にまとめることとしました.また,元来の個人的目的は理論的興味だけではなく実際に構造的部分型に関する型推論を実装してみることでしたし,絶版とはいえ既存の書物の受け売りだけではやり甲斐がないということもあるので,Macrodownという拙作の言語に実際に構造的部分型に関する型推論を組み込みました.これについても簡単に追記します.できるだけ多くの部分をself-containedにすることに努めてはいますが,時間と労力の都合により,広く共有されていると思われる基礎的な事項についてはかなり走り書きになっています.以下のいずれかがあてはまる方は,1章は斜め読みでも差し支えないかと思います:

  • 『型システム入門』の前半程度に目を通している
  • OCamlやStandard MLなどのML系言語を書き,型システムに多少慣れている
  • 単純型つきλ計算の基礎的理解がある
This post is the No.15 article of 言語実装 Advent Calendar 2016