G'Camlの販促です。

どうもこんばんは。この不況の折路頭に迷うことになり、G'Camlの路上販売に商売替えをしたYTです。
今日はモニタの前の皆様に、G'Camlの型レベルプログラミング能力についてご紹介したいと思います。

まず、G'Camlの型レベル言語はチューリング完全であるそうです。チューリング完全ということは、ありとあらゆる計算が、コンパイル時にできるということです。(サクラの拍手)

例えば、こんなものを用意すれば、Lispみたいなセル操作をコンパイル時に行うことができます。

type ('a, 'b) cell
type nil = unit
val nil: unit
val cons: 'a -> 'b -> ('a, 'b) cell
val car: ('a, 'b) cell -> 'a
val cdr: ('a, 'b) cell -> 'b

……実体？そんなものは(Obj.magic 0)を使って定義しましょう。(Obj.magic 0)でごまかしている箇所は、勿論実行すると落ちますが、コンパイル時の型付けに関して実行時の値は関係ありません。従って、型レベルプログラミングを問題無く行うことができます。
そうはいっても実際のコードは実行時にも動きますので、実行時エラーを出さないようにするためにも、また、実行時に型レベルで行った計算を繰り返させないためにも、一工夫必要です。
具体的にはlazyや関数を使い、型だけ利用します。

#let tlv = lazy (cons 1 (cons "" nil))
val tlv : (int, (string, unit) cell) cell lazy_t = <lazy>

こうしてタイプリストが作れるようになりました。ここまでは純正O'Camlでもできます。純正O'Camlにできないものは、分岐や再帰です。
G'Camlの力を持ってすれば、それも可能になります。
例えば、自然数計算。

type 'a ord = (nil, 'a) cell
type zero = nil
type one = zero ord
val zero: zero
val one: one
val succ: 'a -> 'a ord
val pred: 'a ord -> 'a
val is_zero: [| zero -> one | 'a ord -> zero |]
val add: [| zero -> zero -> zero
          | zero -> 'b ord -> 'b ord
          | 'c ord -> zero -> 'c ord
          | {'d -> 'e ord ord -> 'f ord < 'a} => 'd ord -> 'e ord -> 'f ord |] as 'a
...

数が扱えるということはC++のtemplate class中のenumみたいなことも真似できるわけで、Lokiみたいなことも可能です。
例えばタイプリスト操作関数。

val length: [| nil -> zero
             | {'b -> 'c < 'a} => ('d, 'b) cell -> 'c ord |] as 'a
...

typelist_of_tupleやtuple_of_typelistも書けちゃいますので、O'Camlでは面倒だったタプルに1要素追加する操作もあらこんなに簡単に！

static_assertなどなど応用は無限大に広がっております。
さああなたも一家にひとつG'Camlいかがですか！？

↓↓↓続きはWebで↓↓↓
http://panathenaia.halfmoon.jp/alang/typelevel/
追記
型レ用の資料も置いてあります。自分でも説明不足がありありとわかる……。今からでも直せるだけ直しますorz