Arantium Maestum

プログラミング、囲碁、読書の話題

TaPL

パラメトリック多相と型コンストラクタ

前回の記事で これを書いていて「あれ、多相って関数だけじゃなくて型に対しても使う?型コンストラクタってそれ自体が多相?」とふと疑問を抱いた。この点に関しても別の記事で書きたいが、現在の自分のスタンスとしては、特殊な例を除いて「パラメトリック…

高カインド型・高階多相についてのメモ

前回に続いてカインドについてのメモ。 TaPLとともに、"Functional Programming with Overloading and Higher-Order Polymorphism"という資料をかなり参考にしている。 高カインド型 高カインド型(Higher Kinded Types)については以下のStack Overflowの返…

型システムのカインドという概念についてのメモ

Types and Programming Languagesの最後のほうに「カインド」という概念が出てくる。 System Fをさらに拡張したSystem Fωという型システムが存在していて、その「拡張の方向」がカインドだということらしい。(ちなみにSystem FωはF-ing Modules論文のベース…

Impredicative Typesについてのメモ

最近なかなかブログを更新できずにいて、気持ちとしては しかしブログは「シリーズ物の記事」と考えて書こうとすると、シリーズ最後あたりは本当に書くのがつらくなるな— zehnpaard (@zehnpaard) February 21, 2022 で少し自分の首を絞めている感覚がある。 …

OCamlで存在型を試してみた(その4ーーGADT)

ここまで zehnpaard.hatenablog.com zehnpaard.hatenablog.com zehnpaard.hatenablog.com とモジュール関連の機能で存在型を扱う話をしてきた。 しかし、OCamlでもっとも直接的に存在型をエンコードしたいならGADTが使える。 ダメな例 まずはうまくいかない…

OCamlで存在型を試してみた (その3ーーモジュール)

シリーズ前々回と前回に続いて存在型を探っていく。 今回はパラメトリックな機構はまったく使わないただのモジュールと存在型について。 第1級モジュールやファンクタによる抽象化機能と存在型について書いてきたが、型としての「存在型」はどちらの場合で…

OCamlで存在型を試してみた (その2ーーファンクタ)

zehnpaard.hatenablog.com の続き。 前回は第1級モジュールを非常に綺麗に存在型に対応させられることが示せた。 しかし第1級モジュールを使わずとも、OCamlだとモジュールのシグニチャ自体が存在型的だ。(ただし微妙だが重要な差異もある) 今回はファン…

OCamlで存在型を試してみた (その1ーー第1級モジュール)

Types and Programming Languagesの24章の主題は存在型(Existential Types)である。 私は何回読んでもここでつまづく。 この章に到達するまでに部分型やら再帰型やら型推論やら全称型やら出てくるが、まあ難しくとも、なんとなくどういった言語機能に関連…

TaPLの公式実装をduneでビルドする時にハマったこと

非常に限定された一部界隈では非常に有名なことで有名なTypes and Programming Languagesの公式サイトから、本に出てくる型システムの実装がダウンロードできる: www.cis.upenn.edu 以前も気になった部分を落として実装を覗いてみたりはしたのだが、コンパ…