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の型推論はこれでやっていきます