昔の仕事を引っ張り出してみる。
id:ytqwerty さんが GCaml での type level programming の可能性にチャレンジされていた。正直六年前の事なので覚えていない事が多いし、そもそも type level programming をするつもりの拡張じゃないのでいろいろアレだが勘弁してほしい。全ソースは最後にまとめてあります。
型で計算する場合、その型に対応する値をいちいち作らなきゃいけないのが面倒だよね。assert false や Obj.magic は型 '_a だが、実行すると問題が生ずる。型レでコメントしたように、型τ をそのまま扱うのではなくて、'a t のパラメータにτを入れてあげる (τ t) という形にすると少し見通しがよろしい。'a t は 'a option でも 'a list でもでもよいけど、どうせ 'a t の値自体は使わないんだから、'a t を phantom type にして、実装を () にする:
module T : sig type 'a t val t : 'a t val of_val : 'a -> 'a t val (%) : ('a -> 'b) t -> 'a t -> 'b t (* lift *) end = struct type 'a t = unit let t = () let of_val _ = t let (%) _ _ = t end open T
signature を使って τ t と τ' t が勝手に unify されないようにしている事に注意。τ t の型を持つ値は (t : τ t) と書けばおkなのでスコブル楽チン:
type true_ type false_ let true_ : true_ t = t let false_ : false_ t = t let not = generic | : (true_ -> false_) t => t | : (false_ -> true_) t => t
なんでも右辺は t だね。型の計算から値を取り出す場合は流石に t ではない:
let to_val = generic | : true_ t -> bool => fun _ -> true | : false_ t -> bool => fun _ -> false let static_assert : true_ t -> unit = fun _ -> ()
型上の自然数:
module Nat = struct type z type 'a s let z : z t = t let s : ('a -> 'a s) t = t let d : ('a s -> 'a) t = t
Successor s は関数では無いので、所謂 S Z を計算するには (%) operator を使う: s % z。ここが面倒臭いが、ほぼ trivial なので、phantom type を使いつづけることにしよう。
let rec to_val = generic | : z t -> int => fun _ -> 0 | : 'a s t -> int => fun (n : 'a s t) -> to_val (t : 'a t) + 1 (* unfortunately we cannot use the type at the left of => *)
to_val で τ s t から τ t を得て、再帰的に to_val を呼び出すんだけど、残念ながら => の左辺の 'a を右辺で利用することが出来ません。確か利用できるようにしたはずなんだけど、現在のソースには残ってないみたいだ。
型上の計算では右辺は t の原則で add も書ける:
let rec add = generic | : (z -> z -> z) t => t | : ('a s -> z -> 'a s) t => t | : ('a -> 'b s -> 'c s) t => (* need to write the relationship between 'a 'b and 'c using an expression, which uses add as ('a s -> 'b -> 'c s) t *) ignore (add : ('d s -> 'e -> 'f s) t); (t : ('d -> 'e s -> 'f s) t)
流石に最後のケースは 'a -> 'b s -> 'c s だけでは計算にならないので、この足し算の前提、'a s -> 'b -> 'c s が必要。これは add 自身をこの前提の形に type constraint を使って instantiate してあげた上で、その constraint の型から結果の型を作ってやるという形になる。ここでも => の左辺にある型変数を constraint に使えればもう少し短く書けるはずだ。
さてさて、ここで Bool と Nat で to_val という関数を作ったけど、こいつらを overload してあげた方が何かと格好よいよね:
let to_val = generic Bool.to_val | Nat.to_val
この overload された to_val、 to_val (add % z % z) は黙っていても計算できるが、to_val (add % z % (s % z)) が出来ない。GCaml にとって式が複雑過ぎるからだ。基本的に OCaml に取り敢えず type class のない overloading を入れよう、が目標であった GCaml では overload された値同士の型上でのインタラクションは余り深く考えられていない。一応ちょっとは試してみるので to_val (add % z % z) はうまくいくが、ちょっと難しいとすぐ諦める仕様になっている。
こういう場合は overloaded value 同士のインタラクションが無くなるように、 overload resolution を強制してやればよろしい:
let one = add % z % (s % z) in assert (to_val one = 1);
ここで(GCaml では) one は polymorphic な値になれない。右辺式が expansive なので value restriction が働くためである。そこで、右辺の型に対して overloading の resolution が発生する。右辺の型は
{ (z -> z s -> '_f) t < [| (z -> z -> z) t | ('b s -> z -> 'b s) t | { ('c s -> 'd -> 'e s) t < 'a } => ('c -> 'd s -> 'e s) t |] as 'a } => '_f t
(z -> z s -> '_f) は三番目のケースの => の右側、 (c' -> 'd s -> e' s) t にしかマッチしない。'c = z, 'd = z, '_f = 'e s が得られて、それで前提条件である => の左側を解いて、、、といろいろ計算していくと '_f = z s って事が判る。暇だったら手でやってみな。嫌んなるから。
GCaml が出来たころは普通の value restriction しか無かったので、この expansive let による overload resolution は統一感があって、こうした workaround にはなかなかに有効だったのだが、この頃の GCaml は restricted value polymoprhism のおかげで expansive な let を使っても resolution が走らないことがある。が、この例では関係ないからいいか。
さて、型が同じかどうか判定できないのではないかという話があったけれども、これは、マァ出来る、という主張をしておきたい:
# TComp.compare % of_val 1 % of_val 2;; - : Bool.true_ t = <abstr> # TComp.compare % of_val 1 % of_val 2.0;; - : Bool.false_ t = <abstr>
ほらね。上の式をもうちょっと考えてみよう:
# fun () -> TComp.compare % of_val 1 % of_val 2;; - : { (int -> int -> 'd) t < [| ('a -> 'a -> Bool.true_) t | ('b -> 'c -> Bool.false_) t |] } => unit -> 'd t = <generic>
Non expansive にすると polymorphic な型のママになった。これが expansive のママだと resolution が行われて Bool.true_ t にまで落ちる。すごいすごい。
でも何で？ Bool.false_ t に落ちてもいいじゃないですか？だって、 (TComp.compare % of_val 1 % of_val 2 : Bool.false_ t) は型エラーになりませんよ？
これは GCaml の変態的 overload resolution priority のおかげ。Overload resolution しなくちゃいけないけど、複数のケースがマッチするときは、先に宣言された方を勝手に GCaml が選んでくれる。正直キモいが、便利な時もある。とういう訳で、型が同じかどうか、というか、 unifiable かどうかは、GCaml では expansive let による auto overload resolution を使えば可能、ということです:
# (fun x y -> TComp.compare % x % y) (of_val 1);; - : int t -> Bool.true_ t = <fun>
上の例は、も一つの引数が int ならハッピーなのに、という計算をしてくれています。false_ の事は考えたらあかんねん。ポジティブや！
そんな感じ。
という訳でD論を書き終えて季節も頭ン中も春の君達も、その内容は黒歴史にせず、ある程度覚えておこうな。約束だぜ！
全ソース
module T : sig type 'a t val t : 'a t val of_val : 'a -> 'a t val (%) : ('a -> 'b) t -> 'a t -> 'b t (* lift *) end = struct type 'a t = unit let t = () let of_val _ = t let (%) _ _ = t end open T module Bool = struct type true_ type false_ let true_ : true_ t = t let false_ : false_ t = t let not = generic | : (true_ -> false_) t => t | : (false_ -> true_) t => t let to_val = generic | : true_ t -> bool => fun _ -> true | : false_ t -> bool => fun _ -> false let static_assert : true_ t -> unit = fun _ -> () end module Nat = struct type z type 'a s let z : z t = t let s : ('a -> 'a s) t = t let d : ('a s -> 'a) t = t let rec to_val = generic | : z t -> int => fun _ -> 0 | : 'a s t -> int => fun (n : 'a s t) -> to_val (t : 'a t) + 1 (* unfortunately we cannot use the type at the left of => *) let _ = assert (to_val z = 0); assert (to_val (s % z) = 1) let is_zero = generic | : (z -> Bool.true_) t => t | : ('a s -> Bool.false_) t => t let rec add = generic | : (z -> z -> z) t => t | : ('a s -> z -> 'a s) t => t | : ('a -> 'b s -> 'c s) t => (* need to write the relationship between 'a 'b and 'c using an expression, which uses add as ('a s -> 'b -> 'c s) t *) ignore (add : ('d s -> 'e -> 'f s) t); (t : ('d -> 'e s -> 'f s) t) let rec sub = generic | : (z -> z -> z) t => t | : ('a s -> z -> 'a s) t => t | : ('a s -> 'b s -> 'c) t => ignore (sub : ('d -> 'e -> 'f) t); (t : ('d s -> 'e s -> 'f) t) (* type error: let _v : Bool.false_ t = is_zero % (add % z % z) *) let _v : Bool.true_ t = is_zero % (add % z % z) let _ = assert (to_val (add % z % z) = 0); (* This does not work because of the cut problem between to_val and its argument assert (to_val (add % z % (s % z)) = 1) we need a expansive let to fixate the type of the argument *) let one = add % z % (s % z) in assert (to_val one = 1); let two = add % (s % z) % (s % z) in assert (to_val two = 2); let zero = sub % (s % z) % (s % z) in assert (to_val zero = 0); (* let two = sub % (add % one % two) % one in *) let three = add % one % two in let two = sub % three % one in assert (to_val two = 2) end module TList = struct type nil type ('a, 'b) cons let nil : nil t = t let rec cons = generic | : ('a -> nil -> ('a, nil) cons) t => t | : ('a -> ('b, 'c) cons) t => t let rec length = generic | : (nil -> Nat.z) t => t | : (('a, 'b) cons -> 'c Nat.s) t => ignore (length : ('e -> 'c) t); (t : (('d, 'e) cons -> 'f Nat.s) t) end module TComp = struct open Bool let compare = generic | : ('a -> 'a -> true_) t => t | : ('a -> 'b -> false_) t => t open Nat let _ = static_assert (compare % of_val 0 % of_val 1); static_assert (Bool.not % (compare % of_val 0 % of_val 0)) end let to_val = generic Bool.to_val | Nat.to_val (* the overloaded to_val cannot find its return type automatically, since it was considered too complex. *) let _ = (to_val Nat.z : int) let _ = assert (to_val Nat.z = 0); assert (to_val (Nat.s % Nat.z) = 1)