Core Erlangにおける型の内部表現

Dialyzerが生成するPLT(Persistent Lookup Table)ファイルではAPIの型情報として、変換したCore Erlangの内部形式をそのままバイナリにしている。このPLTを解析するためにCore Erlangの型の内部表現を調べた。

仮定するバージョン

• erlang/OTP 21

想定する読者

• pltファイルを解析したい人
• erlangの型表現を深く理解したい人

いろいろな型表現

any() 型

単一のatomで内部表現される三銃士の一人。
全てのデータの型。 term() 型とも表記する。subtyping関係においてもっとも大きい型に位置する。

spec表記	内部表現
any()	'any'
term()	'any'

シングルトン型

Erlangの型システムでは定数値一つだけからなる型を構成することができる。例えば 型 1は値1だけからなる型を表す。任意の定数値でこのシングルトン型を作れるわけではないので注意が必要だ。シングルトン型が構成できるものは以下の通り。

	例	内部表現
数値	123	{'c', 'number', {'int_set', [123]}, 'integer'}
atom	ok	{'c', 'atom', ['ok'], 'unknown'}
空リスト	[]	{'c', 'nil', [], 'unknown'}
空文字列	""	{'c', 'nil', [], 'unknown'}
空マップ	#{}	{'c', 'map', [], 'unknown']

数値型

Numberタグを持つ数値型は integer() や float() 以外にも範囲を表す int_rng指定、 特定の有限集合内を表す int_set 指定などができる。

例	内部表現
integer()	{'c', 'number', 'any', 'integer'}
float()	{'c', 'number', 'any', 'float'}]
char()	{'c', 'number', {'int_rng', 0, 1114111}, 'integer'}
1..255	{'c', 'number', {'int_rng', 1, 255}, 'integer'}
1..12	{'c', 'number', {'int_set', [1,2,3,4,5,6,7,8,9,10,11,12]}, 'integer'}

Atom型(boolean型)

単一のatomだけの型やatom全体を表す型はいずれも atomタグの型で表現される。またatomだけからなるユニオン型の場合は特別に１つのatomタグの型で表現する様である。

spec表記	内部表現
not_found	{'c', 'atom', ['not_found'], 'unknown'}
false｜ignored｜true	{'c', 'atom', ['false', 'ignored', 'true'], 'unknown'}
boolean()	{'c', 'atom', ['false', 'true'], 'unknown'}
atom()	{'c', 'atom', 'any', 'unknown'}

例

prim_buffer.erl

-spec try_lock(Buffer :: prim_buffer()) -> acquired | busy.

{'contract', [{{'c', 'function', [{'c', 'product', ['any'], 'unknown'}, {'c', 'atom', ['acquired', 'busy'], 'unknown'}], 'unknown'}, nil}], ['any'], [{{'type', 121, 'fun', [{'type', 121, 'product', [{
'ann_type', 121, [{'var', 121, 'Buffer'}, {'user_type', 121, 'prim_buffer', nil}]}]}, {'type', 121, 'union', [{'atom', 121, 'acquired'}, {'atom', 121, 'busy'}]}]}, nil}]}

バイナリ型

spec表記	内部表現
binary()	{'c', 'binary', [8, 0], 'unknown'}
bitstring()	{'c', 'binary', [1, 0], 'unknown'}
<<_:1111, _*:2222>>	{'c', 'binary', [2222, 1111], 'unknown'}

関数型

引数側の型は必ずany()型またはproductタグの型になっている。

spec表記	内部表現
fun((binary()) -> binary())	{'c', 'function', [{'c', 'product', [{'c', 'binary', [8,0], 'unknown'}], 'unknown'}, {'c', 'binary', [8,0], 'unknown'}], 'unknown'}
function()	{'c', 'function', ['any', 'any'], 'unknown'}

例

erlang.erl

-spec spawn_link(Fun) -> pid() when
      Fun :: function().

{'contract', [{{'c', 'function', [{'c', 'product', [{'c', 'function', ['any', 'any'], 'unknown'}], 'unknown'}, {'c', 'identifier', ['pid'], 'unknown'}], 'unknown'}, [{'subtype', {'c', 'var', 'Fun', 'unknown'}, {'c', 'function', ['any', 'any'], 'unknown'}}]}], [{'c', 'function', ['any', 'any'], 'unknown'}], [{{'type', 2800, 'fun', [{'type', 2800, 'product', [{'var', 2800, 'Fun'}]}, {'type', 2800, 'pid', nil}]}, [{'type', 2801, 'constraint', [{'atom', 2801, 'is_subtype'}, [{'var', 2801, 'Fun'}, {'type', 2801, 'function', nil}]]}]}]}

識別子型(port(), pid(), reference())

port()型、pid() 型、reference()型および、これらのユニオンからなる型はIdentifierタグの型として扱われる。

reference()型は erlang runtimeの中でのプロセス間でのやり取りで使う参照値の型であり、MLなどにある破壊的代入を目的とした参照型('a ref) とは全く別物であることに注意。

spec表記	内部表現
pid()	{'c', 'identifier', ['pid'], 'unknown'}
pid()｜port()	{'c', 'identifier', ['pid', 'port'], 'unknown'}

例

erlang.erl

-spec exit(Pid, Reason) -> true when
      Pid :: pid() | port(),
      Reason :: term().

{'contract', [{{'c', 'function', [{'c', 'product', [{'c', 'identifier', ['pid', 'port'], 'unknown'}, 'any'], 'unknown'}, {'c', 'atom', ['true'], 'unknown'}], 'unknown'}, [{'subtype', {'c', 'var', 'Rea
son', 'unknown'}, 'any'}, {'subtype', {'c', 'var', 'Pid', 'unknown'}, {'c', 'identifier', ['pid', 'port'], 'unknown'}}]}], [{'c', 'identifier', ['pid', 'port'], 'unknown'}, 'any'], [{{'type', 782, 'fu
n', [{'type', 782, 'product', [{'var', 782, 'Pid'}, {'var', 782, 'Reason'}]}, {'atom', 782, 'true'}]}, [{'type', 783, 'constraint', [{'atom', 783, 'is_subtype'}, [{'var', 783, 'Pid'}, {'type', 783, 'u
nion', [{'type', 783, 'pid', nil}, {'type', 783, 'port', nil}]}]]}, {'type', 784, 'constraint', [{'atom', 784, 'is_subtype'}, [{'var', 784, 'Reason'}, {'type', 784, 'term', nil}]]}]}]}

タプルおよびレコード型

Erlangではレコードはタプルの一種である。
タプル型は基本的にTupleタグの型となる。各要素の型、長さの情報に加えて、レコードかもしれないときのための最初の要素のatomを保持している。純粋なタプルで1つめの要素がatomじゃなかった場合このフィールドはanyとなる。

spec表記	内部表現
{'ok', term()}	{'c', 'tuple', [{'c', 'atom', ['ok'], 'unknown'}, 'any'], {2, {'c', 'atom', ['ok'], 'unknown'}}}
tuple()	{'c', 'tuple', 'any', {'any', 'any'}}
-record(state, {}).	{'c', 'tuple', [{'c', 'atom', ['state'], 'unknown'}], {1, {'c', 'atom', ['state'], 'unknown'}}}

また、タプル(レコード)だけからなるユニオンの場合に特化したTupleSetというタグの型になるから注意が必要だ。TupleSetはTuple型を長さごとにまとめて次のような構造になっている。

erl_type.ml

| Tuple of tuple
| TupleSet of (int * tuple list) list

spec表記	内部表現
{atom(), any()}｜{atom(), any(), any()}	{'c', 'tuple_set', [{2, [{'c', 'tuple', [{'c', 'atom', 'any', 'unknown'}, 'any'], {2, 'any'}}]}, {3, [{'c', 'tuple', [{'c', 'atom', 'any', 'unknown'}, 'any', 'any'], {3, 'any'}}]}], 'unknown'}

Map

Map型はレコードのようにフィールド名に対応する型を持つデータ型である。レコードのように実態がタプルに潰されない違いがある。

リスト

Erlangのリストは組み込みで与えられるので、多相型(ジェネリクス)のないdialyzerでもリストの中身の型が型検査で考慮されることがある。
Erlangのリストは一列の要素列だけでなく、終端がNilにならない [1 | "hello"] みたいな値も書けるが、このことが型にも影響している。

Listタグの型は要素の型、終端の型、およびリストが空でないことを示すフラグを保持する。properなリストの時は終端の型は [] になる。

また、空リストだけからなる単一の型 [] のためのNilタグというのも用意されている。逆に言えばリストに関する定数値型は [] のみであり、 [1, 2, 3] や "ok" のような型は書けない。

spec表記	内部表現
[atom()]	{'c', 'list', [{'c', 'atom', 'any', 'unknown'}, {'c', 'nil', [], 'unknown'}], 'unknown'}
[]	{'c', 'nil', [], 'unknown'}
string()	{'c', 'list', [{'c', 'number', {'int_rng', 0, 1114111}, 'integer'}, {'c', 'nil', nil, 'unknown'}], 'unknown'}

None型とno_return()型

単一のatomで内部表現される三銃士の２人。

spec表記	内部表現
none()	'none'
no_return()	'unit'

公式マニュアルではno_return() は none() のエイリアスのように書かれているが内部形式は明確に違うものとなる。

例

escript.erl

-spec start() -> no_return().

{'contract', [{{'c', 'function', [{'c', 'product', nil, 'unknown'}, 'unit'], 'unknown'}, nil}], nil, [{{'type', 261, 'fun', [{'type', 261, 'product', nil}, {'type', 261, 'no_return', nil}]}, nil}]}

Opaque型の参照

-opaque 宣言により、実態は隠蔽して型の名前だけ公開されている型への参照を表す。隠蔽しているといいつつ内部表現としてはがっつり構造を保持している。

spec表記	内部表現
ets:tid()	{'c', 'opaque', [{'opaque', 'ets', 'tid', nil, {'c', 'identifier', ['reference'], 'unknown'}}], 'unknown'}

型変数

多相的な関数は書けないが、部分型制約や導出の過程で現れる型。

spec表記	内部表現
A	{'c', 'var', 'A', 'unknown'}

ユニオン型

ユニオン型。内部表現では none() 型が追加された形になっていることもある。

spec表記	内部表現
'undefined' ｜ pid()	{'c', 'union', [{'c', 'atom', ['undefined'], 'unknown'}, 'none', 'none', {'c', 'identifier', ['pid'], 'unknown'}, 'none', 'none', 'none', 'none', 'none', 'none'], 'unknown'}

宣伝

Erlangの静的型検査機 fialyzer をOCamlで開発しようとしています。

• https://github.com/dwango/fialyzer

最初の目標はdialyzerよりも甘くていいから省メモリで高速に動作することです。アドバイスやご意見ありましたら、issue, PR, twitter 大歓迎です。