タグ別アーカイブ: 型システム

交差型 (intersection types)

型システムの勉強の続き。

有界量化を持つ体系 System F<: (Fsub) に続いて、交差型を持つ体系 F (Finter) を実装する。

作ったものは、前と同じ GitHub に置いてある:

https://github.com/minoki/LambdaQuest

TaPL でも交差型について言及されているが、あまり詳しく書いてあるとは言えない。そこで、B. C. Pierce の Programming with Intersection Types and Bounded Polymorphism (1991) という論文を参考にした。著者のサイトにPDFが置いてある。似たようなトピックの論文が他にもあるようだが、それらとの関係は確認していない。

論文の Finter では有界量化の上界に関して反変な部分型関係を入れているが、それをやると(TaPLにもあるように)部分型関係が決定手続きでなくなるらしいので、今回実装した Finter には(前回実装した Fsub にも)それは入れていない。

続きを読む

型システムの勉強

型システムを自分で設計したいと思ったので「型システム入門 プログラミング言語と型の理論」(原題:Types and Programming Languages, 略して TaPL)を読んで勉強している。

この記事は私の雑な理解を吐き出したものであり、あまりまとまっていない。しかし、何かしらをアウトプットすることに意義がある(キリッ 続きを読む

Union Typesは直和型ではない

TypeScript 1.4について、 TypeScript 1.4.1 変更点 – Qiita という記事が目に留まった。で、その中の
直和型(Union Types)
という項目に引っかかりを感じた。

なぜ引っかかりを感じたかというと、TypeScriptに今回導入されたUnion Typesと、巷に言う直和型というのは、異なる概念であるからだ。

注意:以下の話は型理論の専門家でもないフツーの学生が適当に書いた程度の信憑性しかありません。

続きを読む