Note

サイト
最近のコメント
 | 

2009-04-01

[] 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

camlspottercamlspotter 2009/04/01 21:28 チュー*リ*ングってことでヨロ!

ytqwertyytqwerty 2009/04/01 23:37 ありがとうございます。修正しました。我ながらひどいtypo……。

camlspottercamlspotter 2009/04/08 17:37 面白いですね。GCaml 作ったときはこんなこと全然考えてなかったので、目から鱗です。
型レベルなんとかで発表していただけませんか?

ytqwertyytqwerty 2009/04/17 01:17 発表することになってしまいました。http://atnd.org/events/451
当日はお手柔らかにツッコミお願いいたします。

 | 
カレンダー
2004 | 01 | 02 | 03 | 04 | 05 | 06 | 07 | 08 | 09 | 10 | 11 | 12 |
2005 | 01 | 02 | 03 | 04 | 05 | 06 | 07 | 08 | 09 | 10 | 11 | 12 |
2006 | 01 | 02 | 03 | 04 | 05 | 06 | 07 | 08 | 09 | 10 | 11 | 12 |
2007 | 01 | 02 | 03 | 04 | 05 | 06 | 07 | 08 | 09 | 10 | 11 | 12 |
2008 | 01 | 02 | 03 | 04 | 05 | 06 | 07 | 08 | 09 | 10 | 11 | 12 |
2009 | 01 | 02 | 03 | 04 | 05 | 06 | 07 | 08 | 09 | 10 | 11 | 12 |
2010 | 01 | 02 | 03 | 04 | 05 | 06 | 07 | 08 | 09 | 10 | 11 | 12 |
2011 | 01 | 02 | 03 | 04 | 05 | 06 | 07 | 08 | 09 | 10 | 11 | 12 |
2012 | 01 | 02 | 03 | 04 | 05 | 06 | 07 | 08 | 09 | 10 | 11 | 12 |
2013 | 01 | 02 | 03 |