交差型 (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 にも）それは入れていない。

続きを読む →

型システムの勉強

1件のフィードバック

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

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

Haskell でオレオレ Num クラスを作るための考察

コメントを残す

以前の記事に書いたように、 Haskell 標準の Num クラスには色々と不満がある：

Haskell の Num クラスに対する不満

結論としては「過去に遡って Num クラスの定義を変えるしかない」だったわけだが、時間干渉も因果律への反逆もできない我々としてはその選択肢は現実的ではないので、独自の Num クラス（オレオレ Num クラス）を作ることにする。この記事は、筆者がオレオレ Num クラスを作った際に考えたことをまとめたものである。

続きを読む →

C++ から OpenCL を使う（その0）：準備

21世紀を生きる者として、並列コンピューティング技術の一つや二つは扱えなければならない。

この間書いた Haskell で並列評価する記事は CPU のマルチコアを活用するものだったが、今度は CPU 以外のデバイス（GPU を念頭に置く）を活用できる技術を使いたい。いわゆる GPGPU をやりたい。（技術に入門するのが目的であって、計算能力を活かして特にこれがしたいという訳ではない。そもそも筆者の手持ちの GPU の計算能力などたかが知れているが……）

N 社の GPU を前提にするなら CUDA という選択肢もあるだろうが、ここでは移植性を重視して OpenCL を試すことにする。（というか、 Mac ユーザー的には CUDA という選択肢は存在しないも同然）

続きを読む →