F#のコンピューテーション式の知識を前提としています
知らない方でもなるべくわかるように書こうと思います
関数型システムプログラミング言語Cargryを開発しています
今日は、Cargryの型推論ライブラリActoaについて解説しようと思います
Actoaって？
「Actoa」という名前はライブラリ名で、型推論の名前はMonadic Lambda Walk Type-Inference (MLW) です
私の知る限りでは、他の型推論とは異なるものです（そもそも仕組みから「推論」と言えるのやら...）
サンプルコード
見ただけでは何が何だかわからないと思いますが、とりあえず見てください
解説
MLWに登場する型は以下の4つです
-
PseudoPointer：推論の結果を記録・保持するものです -
MLWGrammarLeaf：そこまで意味はありません。以下2つをまとめるものです -
MLWTypeVar：型変数です -
MLWFunction：型変数に対して作用させるものです。引数はタプルで、自由に設定できます
まず、MLWTypeVar作成時に、PseudoPointerへ書き込みがなされます。サンプルコードでは以下になります
| 変数名 | 値 |
|---|---|
gl1 |
unknown some |
gl2 |
unknown none |
gl3 |
unknown none |
ここで、unknownは未確定の型、some、noneは型に付随する補足情報です（Rustで言うと、どこの型変数の借用なのか、何のトレイトを実装しているかなど）
そして、38行目から40行目にかけて型推論を行います
38行目
38行目は
let res = gl1.function.execute_function(gl1.type_var);
です
gl1のクロージャの定義から、PseudoPointerは
| 変数名 | 値 |
|---|---|
gl1 |
"Obj" some |
gl2 |
unknown none |
gl3 |
unknown some |
に変わります。この時、gl1がresに変わります
39行目
let (res2, _) = gl2.function.execute_function((gl2.type_var, res));
です
gl2のクロージャの定義から、PseudoPointerは
| 変数名 | 値 |
|---|---|
gl1 |
"Obj" some |
gl2 |
ref gl1 unknown none |
gl3 |
unknown some |
に変わります。gl2はres2に変わります
unifyを呼ぶと、selfと、selfを指す変数は、引数を指すようになります。元の値はそのまま放置されます
40行目
let (_, _) = gl3.function.execute_function((gl3.type_var, res2));
です
gl3のクロージャの定義から、PseudoPointerは
| 変数名 | 値 |
|---|---|
gl1 |
"Obj" some none |
gl2 |
ref gl1 unknown none |
gl3 |
ref gl1 unknown some |
に変わります
gl2とgl3がgl1を指していることがわかります
これによって、gl1とgl2、gl3は全て同じ型になります
なぜコンピューテーション式の知識が必要？
MLWのアイデアがこれから始まっているためです
サンプルコードは
R = lambda(
T,
[T = "Obj"]
=> lambda(
U,
[U <- T]
=> lambda(
S,
[
S <- U,
add(U, sub some)
]
=> S
) (unknown sub some)
) (unknown sub none)
) unknown sub some)
を表したものです
MLWの特徴
MLWの特徴としては「同じ型でも『違う型』とする」というところです
「この2つが同じ型」か、「あれはそれに関連する型」と言わなければいけません
また、「実行フローも表せる」という特徴もあります
サンプルコードで言えば
fn f(v1: Obj) -> Obj {
let v2 = v1;
v2
}
を表しています
gl1とgl3をみると、「v1が使われ、返り値になる」となります
fn f(v1: Obj) -> Obj {
let v2 = v1;
Obj::new()
}
となると、gl3はgl1を指さなくなります
終わりに
MLWはHindley-Milner型推論の実装が面倒くさくて生まれたものです
Cargryの型推論はこれでやっていきます