型推論

規則では、キャプチャの型集合を決定するために、条件式と出力式について型推論が行われます。

型推論の流れ

まず、条件式について型推論を行い、各キャプチャが取り得る型集合を推論します。
次に、出力式について型推論を行い、各キャプチャが取り得ない型を排除します。
ここで、キャプチャ間の型制約関係が見つかった場合、コンパイルエラーを出します。

条件式の型推論

条件式には、高々 1 種類のキャプチャのみを含むことができます。ここではそのキャプチャを $ とします。

ここで推論されるキャプチャの型集合は暫定的なものであり、この後の出力式の型推論でさらに絞り込まれます。

キャプチャ単体式の型推論

型ヒントがついているキャプチャ単体式であれば、キャプチャはその型として推論され、そうでない場合は全ての型の集合が $ の型集合として推論されます。

キャプチャ条件式の型推論

$ にあらゆる型を当てはめ、型チェックをパスした型の集合を $ の型集合として推論します。

出力式の型推論

推論アルゴリズム

出力式では、制約伝播による推論を行なっています。

条件式の型推論で得られたキャプチャの型集合に加えて、その規則の各出力式に含まれる全ての演算子を推論材料として使用し、以下の手順で行われます。

出力式に含まれる各演算子の初期状態として、結果の型には全ての型の集合が、更新フラグには true が設定されます。
各演算子のオペランドおよび結果の型集合を、その演算子の型シグネチャと照合し、取り得ない型をそれぞれの型集合から削除します。また、それによって直接的に影響を受けるノードの更新フラグを true にし、自分自身の更新フラグを false にします。
2.をすべての演算子ノードの更新が終わるまで繰り返します。
これによって推論されたキャプチャの型集合から、各出力式の型チェックをパスしないキャプチャの型の組み合わせがないかをチェックします。パスしない組み合わせがある場合、キャプチャ間の型制約関係を検出したとしてコンパイルエラーを出します。

キャプチャ間の型制約関係

キャプチャが取り得る型集合は、キャプチャごとに独立している必要があります。これは、規則がリソースキューを探索する上で計算量を軽減するための仕様です。

例えば、以下の規則は $a と $b が型制約関係を持っているため、コンパイルエラーになります。

. $a, $b # $a = $b  // NG

エラーメッセージは以下の通りです。

型エラー: キャプチャ間の型制約関係を検出しました。
各キャプチャは以下の型を取り得ます。
  $a:{bool, double, int, str, symbol}
  $b:{bool, double, int, str, symbol}
しかし $a:str, $b:int のとき、以下の = 演算が行えません。
  --> 2 行目 15 文字目
  |
2 | . $a, $b # $a = $b
  |               ^
ヒント: 型ヒント演算子を用いてキャプチャの型を絞ることで、このエラーを解消できます。

$a, $b の少なくともどちらか一方に型ヒントを加えることで、型制約関係を取り除くことができます。

. $a:str, $b:str # $a = $b  // OK

. $a:str, $b # $a = $b  // OK

. $a, $b # $a:str = $b  // OK

. $a, $b # $a = $b:str  // OK

また、型を str 型に限定したくない場合には、並列規則に分割してください。

// OK
. $a:bool,   $b # $a = $b
| $a:double, $b # $a = $b
| $a:int,    $b # $a = $b
| $a:str,    $b # $a = $b
| $a:symbol, $b # $a = $b

また、並列している別の規則に型の情報が含まれる場合、

. $a, $b # $a = $b  // NG
| $a, $b # $b[0]    // $b は str 型

ひとつの規則にまとめることで解消するケースもあります。

. $a, $b # $a = $b, $b[0]  // OK

型推論の流れ​

条件式の型推論​

キャプチャ単体式の型推論​

キャプチャ条件式の型推論​

出力式の型推論​

推論アルゴリズム​

キャプチャ間の型制約関係​