κeenのHappy Hacκing Blog | Lispエイリアンの狂想曲

幽霊型を知った

κeenです。かねてより気になっていた幽霊型(Phantom Type)について知ったのでアウトプット。 このPDFがベースになって ます。

余談ですが英語がファントム・タイプと中々中二な名前なので和訳も幻影型とかそういう方向に走って欲かったな。

「幽霊型」で調べると真っ先にこのサイトが出てくるのですが、ミスリーディングと言われていました。 別に間違ったことを書いている訳ではないのですが、幽霊型の応用例なのでこれこそが幽霊型だと思ってしまうと少し視野が狭くなってしまうようです。

モチベーション

ブーリアンと整数と条件分岐と足し算と比較が出来るミニ言語を考えてみます。自動で型変換は行わない(つまりintとboolの比較などは出来ない)言語とします。こんな感じでしょうか。

datatype exp
  = Int of int
  | Bool of bool
  | If of exp * exp * exp
  | Plus of exp * exp
  | Equal of exp * exp

fun mkInt x = Int x
fun mkBool x = Bool x
fun mkIf cnd thn els = If(cnd, thn, els)
fun mkPlus x y = Plus(x, y)
fun mkEqual x y = Equal(x, y)

exception Type

fun evalIf cnd thn els =
  case eval cnd of
      Bool x => if x then eval thn else eval els
    | _ => raise Type

fun evalPlus x y =
  case (eval x, eval y) of
      (Int x', Int y') => Int(x' + y')
    | _  => raise Type

fun evalEqual x y =
  case (eval x, eval y) of
      (Int x', Int y') => Bool(x' = y')
    | (Bool x', Bool y') => Bool(x' = y')
    | _  => raise Type

fun eval exp =
  case exp of
      If(cnd, thn, els) => evalIf cnd thn els
    | Plus(x, y) => evalPlus x y
    | Equal(x, y) => evalEqual x y
    | e => e

さて、この定義に従うと次のような自明に間違ったプログラムもコンパイルを通ってしまいます1

mkEqual (mkInt 1) (mkBool false)

勿論、評価するとエラーになります。

eval (mkEqual (mkInt 1) (mkBool false));

uncaught exception Type

こういうものを極力コンパイル時に発見出来ないかとうのがモチベーションです。因みにこのモチベーションは変な型変換を行わない言語なら動的型付き言語でも同じで、SBCLで(+ 1 t)を評価するとちゃんとコンパイルエラーになります。

問題の分析

今回、IntだとかBoolだとかの型情報をタグ、つまり値として持たせました。しかしコンパイル時に値にはアクセス出来ません。コンパイル時にアクセスできるのは型です。ということでメタデータとして型を付与しましょう。

幽霊型

メタデータとして型を付けたのが幽霊型です。名前的に'a texpではなく'aの部分が幽霊型なんですかね。

使い方は割と分かりやすくて、datatypeに余計な型をつけます。この'aは使われていませんがメタデータなのでそういうもんです。

datatype 'a texp = E of exp

次に、mkXxx にも型を付けます。

まず、mkIntなら返り値はIntなので'aの部分にその情報を詰め込みます。今回はintが宜しいようです。 毎回Eがつくのが面倒ですが我慢して下さい。

fun mkInt x: int texp = E (Int x)

mkBoolも同じです。

fun mkBool x: bool texp = E (Bool x)

次はmkIfですが、condにはBool型、thenとelseには同じ型が来て欲しいです。そして返り値というかこのIfを evalした型はthenやelseと同じ型なのでこのような型になります。Ifに渡す為に一旦Eを剥がしてます。

fun mkIf (E cnd: 'b texp) (E thn: 'a texp) (E els: 'a texp): 'a texp = E (If(cnd, thn, els))

同じように考えたらmkPlusmkEqualも型付け出来ます。

fun mkPlus (E x: int texp) (E y: int texp): int texp = E (Plus(x, y))
fun mkEqual (E x: 'a texp) (E y: 'a texp): bool texp = E (Equal(x, y))

これ以後は変更ありません。一応修正後のプログラムを載せると、

datatype exp
  = Int of int
  | Bool of bool
  | If of exp * exp * exp
  | Plus of exp * exp
  | Equal of exp * exp

datatype 'a texp = E of exp

fun mkInt x: int texp = E (Int x)
fun mkBool x: bool texp = E (Bool x)
fun mkIf (E cnd: 'b texp) (E thn: 'a texp) (E els: 'a texp): 'a texp = E (If(cnd, thn, els))
fun mkPlus (E x: int texp) (E y: int texp): int texp = E (Plus(x, y))
fun mkEqual (E x: 'a texp) (E y: 'a texp): bool texp = E (Equal(x, y))

exception Type

fun evalIf cnd thn els =
  case eval' cnd of
      Bool x => if x then eval' thn else eval' els
    | _ => raise Type

and evalPlus x y =
    case (eval' x, eval' y) of
        (Int x', Int y') => Int(x' + y')
      | _  => raise Type

and evalEqual x y =
    case (eval' x, eval' y) of
        (Int x', Int y') => Bool(x' = y')
      | (Bool x', Bool y') => Bool(x' = y')
      | _  => raise Type

and eval' exp =
    case exp of
        If(cnd, thn, els) => evalIf cnd thn els
      | Plus(x, y) => evalPlus x y
      | Equal(x, y) => evalEqual x y
      | e => e

fun eval (E x) = eval' x

となります。ユーザインターフェースレベルでの変更はありません。 さて、ということで先の式をもう一度評価してみましょう。

mkEqual (mkInt 1) (mkBool false);
stdIn:1.2-1.34 Error: operator and operand don't agree [tycon mismatch]
  operator domain: int texp
  operand:         bool texp
  in expression:
    (mkEqual (mkInt 1)) (mkBool false)

ちゃんとエラーが出ました。楽しいですね。

発展1 - 任意の型

任意の型を作る手段としてタグ1つ、引数無しのタグ付き共用体を使う方法があります。それを使った技が先のPDFに載ってます。

datatype tcp = TCP
datatype udp = UDP
datatype 'a safe_socket = W of Word32.word

fun mkTCP ....
fun mkUDP ....
fun sendTCP ...
fun sendUPD ...
fun close ...

のように型安全に、そしてcloseのように可能なものはジェネリックにプログラムを書くことが出来ます。

発展2 - サブタイプ

次のようにヒエラルキーがある場合の話です。面倒なので言語を縮小しますね。

datatype num
  = Int of int
  | Real of real

datatype exp
  = Num of num
  | Bool of bool
  | Plus of exp * exp

この場合、こうなります。

datatype num
  = Int of int
  | Real of real

datatype exp
  = Num of num
  | Bool of bool
  | Plus of exp * exp

datatype 'a tnum = N
datatype 'a texp = E of exp

exception Type

fun mkInt x: (int tnum texp) = E (Num  (Int x))
fun mkReal x: (real tnum texp) = E (Num (Real x))
fun mkBool x: (bool texp) = E (Bool x)


fun mkPlus (E x: 'a tnum texp) (E y: 'a tnum texp): 'a tnum texp =
  case (x, y) of
      (Num (Int x'), Num (Int y')) => E (Num (Int (x' + y')))
    | (Num (Real x'), Num (Real y')) => E (Num (Real (x' + y')))
    | _ => raise Type  

疲れてきたので説明省略しますが型パラメータを入れ子にしたら上手い具合にサブタイプの親子関係を表せるよねって話です。

まとめ

幽霊型を使うと値レベルの話を一部型レベルに持ち上げれる(ってことで良いのかな?)

最後に

どうしても

datatype 'a texp = E of exp

としている所のEが気になりますね。型システム上必要っぽい(type 'a texp = expとしてもダメだった)ので必要なコストだとは思うのですが 少くとも内部的にはゼロオーバーヘッドであって欲しいです。最適化で消せそうですが実際に消してる処理系はどれほどあるのでしょう。

type 'a texp = expでダメだった(型がミスマッチしてるのにコンパイルが通ってしまった)のも気になります。smlのtypeってただのエイリアスなんでしたっけ?

若干のモヤモヤは残るものの一応幽霊型について知りました。


  1. 因みにこのコードをSML#のREPLで評価すると返ってこなくなります。イシューに上がってます。 [return]
Written by κeen