既存の問題点
Dialyzerのアルゴリズム success typingには独特のユルさがあります。その１つがcase式の型導出規則です。
次のerlangコードを見てください。
run(N) ->
case N of
0 -> 'foo';
1 -> 100
end + 3.
この関数 run は N=0の場合に 'foo' + 3 となってしまうため型エラーになって欲しい気がしますがDialyzerはこれをパスします。
Success Typingがこれを許すメカニズム
型推論木は次のようになります
$$
\frac{
\displaystyle\frac{}{\texttt{+}:\texttt{number()}^2\to\texttt{number()}}
\displaystyle\frac{
\displaystyle\frac{}{A\vdash \texttt{N} : \alpha_N}
\displaystyle\frac{}{\texttt{0:0}}
\displaystyle\frac{}{\texttt{1:1}}
\displaystyle\frac{}{\texttt{'foo':'foo'}}
\displaystyle\frac{}{\texttt{100:100}}
\displaystyle\frac{}{\texttt{}}
}
{A\vdash \texttt{case N of ... end} : \beta_c, (\beta_c=\texttt{'foo'}\wedge\alpha_N=0)\vee(\beta_c=100\wedge(\alpha_N=1)}
\displaystyle\frac{}{\texttt{3:3}}
}
{A\vdash \texttt{case N of 0 -> 'foo'; 1 -> 100 end + 1} : \beta_+, ...\wedge(\beta_c\subseteq \texttt{number()}) \wedge (↑)}
$$
得られる型制約は次のようになります
- Conj
- ...
- $\beta_c \subseteq \texttt{number()}$
- Disj
- ($\beta_c=\texttt{'foo'}) \wedge (\alpha_N=0)$
- ($\beta_c=100) \wedge(\alpha_N=1)$
この制約は次のように解かれ、型チェックは通ります。
- $\beta_c \mapsto 100$
- $\alpha_N \mapsto \texttt{0 | 1}$
主な原因は casek規則に置いて、各パターンの制約を $\vee$ で結合してしまっていて、どこか１つの場合で型制約が通るものがあればよいとしてしまっているところにあると思います。
$$
[CASE]
\frac{A\vdash e:\tau, C_e A\cup \{ v\mapsto \alpha_v | v\in Var(p_i) \}\vdash p_i:\tau_i,C_i^p b_i:\sigma_i,C_i^b}
{A\vdash \texttt{case } e \texttt{ of } p_i \to b_i \texttt{ end} :\beta ,
C_e\wedge
\displaystyle\bigvee_i
\left(
(\beta=\sigma_i)\wedge(\tau=\tau_i)\wedge C_i^p \wedge C_i^b
\right)
}
$$
改善案
[CASE]規則を次で置き換えます。
$$
[CASE']
\frac{A\vdash e:\tau, C_e A\cup \{ v\mapsto \alpha_v | v\in Var(p_i) \}\vdash p_i:\tau_i,C_i^p b_i:\sigma_i,C_i^b}
{A\vdash \texttt{case } e \texttt{ of } p_i \to b_i \texttt{ end} :\beta ,
C_e \wedge \left(\tau \subseteq \displaystyle\bigsqcup_{i} \tau_i\right) \wedge \displaystyle\bigwedge_{i} \left(\sigma_i \subseteq \beta \wedge C_i^p \wedge C_i^b \right)}
$$
この規則への変更で、得られる型制約は次のように変わります
- Conj
- $\beta_c \subseteq \texttt{number()}$
- $\texttt{'foo'} \subseteq \beta_c$
- $\texttt{100} \subseteq \beta_c$
これで、この run 関数を型エラーにできるようになります。
新しい問題点
上記で与えた[CASE']への修正によって、通って欲しいコードが型エラーになってしまう困った事例があります。次のコードを見てください
run(X) ->
case X of
X when is_integer(X) -> X + 1;
'ok' -> 0
end.
このコードは X when is_integer(X) -> の場合の右辺では Xが integer() 型であることを使ってパターンごとで違う制約を与えています。すごいです依存型みたいですね。このコードは型エラーにしたくないですが、我々の修正案を入れると型エラーにしてしまいます。
参考文献
- Lindahl, Tobias & Sagonas, Konstantinos. (2006). Practical type inference based on success typings. 2006. 167-178. 10.1145/1140335.1140356.
- amutake. (2017). 静的に型がつく Erlang を目指して. 進捗大陸01. 31-46. 技術書典2 う-17
宣伝
dialyzerより軽くて早いErlangの型検査ツールをOCamlで開発しています。