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:pg2.erl
-type name() :: any().

-spec create(Name :: name()) -> 'ok'.
```
https://github.com/erlang/otp/blob/OTP-21.1.3/lib/kernel/src/pg2.erl#L44-L46

```erlang
{
  'contract',
  [{{'c', 'function', [{'c', 'product', ['any'], 'unknown'}, {'c', 'atom', ['ok'], 'unknown'}], 'unknown'}, nil}],
  ['any'],
  [{{'type', 46, 'fun', [{'type', 46, 'product', [{'ann_type', 46, [{'var', 46, 'Name'}, {'user_type', 46, 'name', nil}]}]}, {'atom', 46, 'ok'}]}, nil}]
}
```
-->

### シングルトン型

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'}` |

<!--
https://github.com/erlang/otp/blob/OTP-21.1.3/lib/stdlib/src/math.erl

```ceil
[SPEC: 0.000008[ms]] math:ceil/1  (TODO:number(...)) -> TODO:number(...)
{'contract', [{{'c', 'function', [{'c', 'product', [{'c', 'number', 'any', 'unknown'}], 'unknown'}, {'c', 'number', 'any', 'float'}], 'unknown'}, [{'subtype', {'c', 'var', 'X', 'unknown'}, {'c', 'number', 'any', 'unknown'}}]}], [{'c', 'number', 'any', 'unknown'}], [{{'type', 68, 'fun', [{'type', 68, 'product', [{'var', 68, 'X'}]}, {'type', 68, 'float', nil}]}, [{'type', 69, 'constraint', [{'atom', 69, 'is_subtype'}, [{'var', 69, 'X'}, {'type', 69, 'number', nil}]]}]}]}
```
-->

### 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'}` |


#### 例
https://github.com/erlang/otp/blob/OTP-21.1.3/erts/preloaded/src/prim_buffer.erl#L121

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

```erlang
{'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'}`|

#### 例

https://github.com/erlang/otp/blob/OTP-21.1.3/erts/preloaded/src/erlang.erl#L2801-L2802

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

```erlang
{'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'}` |

#### 例
https://github.com/erlang/otp/blob/OTP-21.1.3/erts/preloaded/src/erlang.erl#L782-L784

```erlang: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型を長さごとにまとめて次のような構造になっている。

```ocaml: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'}`  |

<!--
#### 例
```erlang:orddict.erl
```
[SPEC: 0.000005[ms]] orddict:new/0  () -> [{any(), any()}]

```
{'contract', [{{'c', 'function', [{'c', 'product', nil, 'unknown'}, {'c', 'list', [{'c', 'tuple', ['any', 'any'], {2, 'any'}}, {'c', 'nil', nil, 'unknown'}], 'unknown'}], 'unknown'}, nil}], nil, [{{'type', 39, 'fun', [{'type', 39, 'product', nil}, {'user_type', 39, 'orddict', nil}]}, nil}]}
```

```
[SPEC: 0.000011[ms]] inet:get_rc/0  () -> [{atom(), any()} | {atom(), any(), any()}]
{'contract', [{{'c', 'function', [{'c', 'product', nil, 'unknown'}, {'c', 'list', [{'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'}, {'c', 'nil', nil, 'unknown'}], 'unknown'}], 'unknown'}, nil}], nil, [{{'type', 168, 'fun', [{'type', 168, 'product', nil}, {'type', 168, 'list', [{'type', 168, 'union', [{'type', 168, 'tuple', [{'ann_type', 168, [{'var', 168, 'Par'}, {'type', 168, 'atom', nil}]}, {'ann_type', 168, [{'var', 168, 'Val'}, {'type', 168, 'any', nil}]}]}, {'type', 169, 'tuple', [{'ann_type', 169, [{'var', 169, 'Par'}, {'type', 169, 'atom', nil}]}, {'ann_type', 169, [{'var', 169, 'Val1'}, {'type', 169, 'any', nil}]}, {'ann_type', 169, [{'var', 169, 'Val2'}, {'type', 169, 'any', nil}]}]}]}]}]}, nil}]}
```

-->

### 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'}` |


<!--
[SPEC: 0.000006[ms]] code:modified_modules/0  () -> [atom()]
{'contract', [{{'c', 'function', [{'c', 'product', nil, 'unknown'}, {'c', 'list', [{'c', 'atom', 'any', 'unknown'}, {'c', 'nil', nil, 'unknown'}], 'unknown'}], 'unknown'}, nil}], nil, [{{'type', 978, 'fun', [{'type', 978, 'product', nil}, {'type', 978, 'list', [{'type', 978, 'module', nil}]}]}, nil}]}

[SPEC: 0.000005[ms]] io_lib:format_prompt/2  (any(), atom()) -> [[any()] | TODO:number(...)]
{'contract', [{{'c', 'function', [{'c', 'product', ['any', {'c', 'atom', 'any', 'unknown'}], 'unknown'}, {'c', 'list', [{'c', 'union', ['none', 'none', 'none', 'none', {'c', 'list', ['any', {'c', 'nil', nil, 'unknown'}], 'unknown'}, {'c', 'number', {'int_rng', 0, 1114111}, 'integer'}, 'none', 'none', 'none', 'none'], 'unknown'}, {'c', 'nil', nil, 'unknown'}], 'unknown'}], 'unknown'}, nil}], ['any', {'c', 'atom', 'any', 'unknown'}], [{{'type', 269, 'fun', [{'type', 269, 'product', [{'type', 269, 'term', nil}, {'type', 269, 'atom', nil}]}, {'user_type', 269, 'chars', nil}]}, nil}]}
-->

### None型とno_return()型

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

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

[公式マニュアル](http://erlang.org/doc/reference_manual/typespec.html#types-and-their-syntax)では`no_return()` は `none()` のエイリアスのように書かれているが内部形式は明確に違うものとなる。

#### 例
https://github.com/erlang/otp/blob/OTP-21.1.3/lib/stdlib/src/escript.erl#L261

```erlang: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](https://github.com/dwango/fialyzer/issues/new), [PR](https://github.com/dwango/fialyzer/pulls), [twitter](https://twitter.com/yoshihiro503) 大歓迎です。