型推論の理論

handler は effect の名前が一致しても、その effect を捕まえてはならない場合がある。 f(g x) の中で g x が last を起こした場合、f の内側にある last handler は、呼び出し元が持ち込んだ effect をそのまま外へ通さなければならない。 effect の所有者は呼び出し元である。

Yulang はこの区別を handler hygiene と呼ぶ。 このページは、effect と handler に関する公開の型推論 model を説明する。 完全な solver 仕様ではなく、CLI、Playground、language server が出す型を読むための地図である。

subtype solver は、この境界を directed stack weight で表す。 handler は、その weight を通して見える effect family だけを row から引ける。

式は値型と effect row を持つ

公開型に残る 2 つの要素から見ていく。 Yulang の式は、値の型と effect row を持つ。

e : A ! rho

これは「式 e は値 A を返し、その途中で effect row rho の effect を起こす可能性がある」という意味である。

表面の型表示では、この 2 つをまとめて次のように書く。

[console] str

これは、console effect を起こす可能性があり、最後に str を返す computation 値である。

関数型では、返り値側に effect row が付く。

() -> [console] str

これは「unit を受け取り、呼ぶと console effect を起こしうる str を返す関数」である。

普通の subtyping

Yulang の推論器は、型をただ等号で揃えるだけではなく、subtyping constraint として扱う。

actual <: expected

effect row も同じ graph の中を流れる。

[console] str <: [console; 'e] str

具体的な console effect は open row に入る。 handler が effect を消した後に残る residual も、普通の row として同じ graph の中を流れる。

単純な row subtraction だけでは足りない理由

直接的なコードだけを見ると、catch は内側の row から effect を引いているだけに見える。

act console:
    our read: () -> str

our run_console(action: [console; 'e] 'a): ['e] 'a = catch action:
    console::read(), k -> run_console(k "42")
    v -> v

ざっくり言えば、action の row が [console; 'e] なら、catch の外側には ['e] だけが残る。

冒頭の不一致は、小さな高階関数にも現れる。

my compose f g x = f(g x)

g x が last effect を起こしても、f の内部にある last handler はそれを捕まえてはならない。 g の effect は compose の呼び出し元が持ち込んだものであり、f の所有物ではない。 これが冒頭で示した handler hygiene である。

directed stack weight

推論器の内部では、型に stack wrapper を付けることがある。

stack(T, S)

これは source language に stack という型コンストラクタがあるという意味ではない。 どの handler 境界が、どの effect family を引いてよいかを覚えるための内部表現である。

subtype constraint は、左右に向きを持つ重みを持つ。

T @L <: @R U

• 左重み L は active な take(H) を持てる。
• 右重み R は pure pop だけを持つ。
• take(H); pop は cancel するが、pop; take(H) は cancel しない。
• 関数引数は反変なので、そこへ入ると左右の向きが入れ替わる。

この向きが重要である。 row head を handler が消費できるかを決める前に、左右の重みを一つに潰してはならない。

catch はどう effect を引くか

catch が effect 集合 H を処理するとき、推論器は row constraint を次の形で見ることがある。

alpha @L <: @R [H; beta]

この row head から実際に消費できる集合は次である。

J = H ∩ Common(L)

Common(L) は、左重みに残る active な take(...) family の交差である。 右側の pop は handler に effect を見せない。 filter や legacy 互換 marker も active push ではない。

J が空なら、この handler はその row から何も消費できない。 handler があるというだけで residual を作ったり、未知 row を勝手に開いたりしない。

J が空でなければ、solver は row を分ける。

alpha <: [J; gamma]
gamma @(L - J) <: NWeight(R, beta)

NWeight(R, beta) は、右側 pop の evidence を residual tail に残す内部 wrapper である。 row head を見せるためには使わない。

同じ subtraction slot には同じ residual 変数 gamma を再利用する。 これにより、recursive handler が fresh な tail を無限に作り続けることを避ける。

型引数を持つ effect family は family path で突き合わせるが、引数は捨てない。 ref_update int と ref_update alpha が出会った場合、family match と同時に、引数同士を整合させる普通の型 constraint も生成する。

effect 注釈の意味

effect 注釈は、表層 row を説明すると同時に、高階境界を越えて何を handler へ見せるかを決める。 注釈の省略と [_] は異なる contract である。

注釈 slot	内部的な意味
高階 callback 境界で注釈なし	新しい capture contract を与えない。callback 由来の effect は空の可視性 evidence で守られうる。
高階 callback 境界の [_]	surface contract。その境界で推論された表層 row を見せる。
反変な computation 位置の [console]	capture contract。console だけを内側 handler に見せる。
共変な result 位置の省略または [_]	escape filter を足さず、row を open なままにする。
共変な result 位置の [console]	外へ出る effect が console だけであることを検査する。

wildcard row [_] は注釈 placeholder である。 effect row 型そのものの標準構文ではなく、boundary を消すものでもない。 g: _ -> [_] _ のような callback result では、g(x) の普通の表層 effect を受け取り側の計算へ意図的に見せる。 これを書かない場合、callback 由来の effect は hygienic に保たれ、#id[Empty] のような evidence 付きで表示されることがある。

共変位置の具体 effect 注釈は filter である。 filter は static check であり、runtime marker でも residual row でもない。 check が登録された後、保存される solver weight からは消える。

handler に消費されてはいけない fresh internal residual は、概念的には take(Empty) で守る。 推論コアには、別個の protected variable set はない。

表示される型の stack evidence

stack id や pop count は推論 evidence であり、source-level の型構文ではない。 ただし、compiler-oriented な表示では、高階 scheme を説明するためにその evidence が残ることがある。 通常の API 文書として読むときは、値型と effect row の構造を中心に読む。

alpha [nondet; beta] -> [beta] alpha

これは「引数 computation は nondet と residual effect beta を起こしうるが、handler が見えている nondet を消費した後は beta だけが残る」という意味である。 residual beta は公開型の本物の一部であり、表示ノイズとして消してよいものではない。

隠れるのは、その境界で nondet を消費してよい理由を説明する weighted evidence の方である。

高階関数では、空の可視性 evidence 自体が推論 scheme の重要な一部になることがある。 概略的には、注釈なしの compose には次のような protected occurrence が必要になる。

compose_plain :
  (alpha [gamma#u[Empty]] -> [delta] beta)
  -> (epsilon -> [gamma#u[Empty]] alpha)
  -> epsilon
  -> [delta#u] beta#u

#u[Empty] は新しい effect family ではない。 その occurrence の gamma は boundary u で subtract できない、という証拠である。 g(x) の表層 effect を f に意図的に見せたい場合は、programmer が contract を書く。

our compose(f, g: _ -> [_] _, x: [_] _) = f g(x)

その場合、公開型の形は普通の row-polymorphic compose として読める。

compose_surface :
  (alpha [gamma] -> [delta] beta)
  -> (epsilon -> [gamma] alpha)
  -> epsilon
  -> [delta] beta

data-position 関数の private evidence

標準ライブラリには、data 値の中に effectful 関数を保持する抽象化がある。 local reference が代表例で、公開される ref 値の内部には、返り effect に ref_update が関わる関数がある。

solver は、この保存された関数の latent return-effect tail を private evidence として扱い、ordinary residual row だけを公開型へ projection する。 そうしないと、synthetic field getter 経由で AllExcept(ref_update ...) のような内部 stack id が public scheme に漏れてしまう。

公開型には、たとえば ref update なら次のような ordinary row だけが出るべきである。

ref(e & b, a) -> (a -> [b] a) -> [e, b] unit

変数名そのものは読み替えられる。 保存された関数の hygiene を支える private stack evidence ではなく、普通の residual row が public scheme に出ることが要点である。

replay の停止性は型等式ではない

solver は subtype graph の bounds を、正確な directed label 付きで replay する。 「pop が 1 個でも複数個でも同じ」という surface rule は使わない。

停止性のため、同じ endpoint、同じ subtract id、同じ effect family で同じ static boundary を再訪する bound は、bounds table の保存時に subsume できる。 これは同じ replay cycle を永遠に回さないための実装規則であり、ユーザーに見える型の簡約規則ではない。

実行時の見方

specialize 後の runtime は、row 文字列から hygiene を推測して復元することはできない。 関数値、thunk、構造値は、実行される前に handler 境界を越えて移動しうる。

そのため runtime は、値と一緒に guard marker を運ぶ。 概念的には、この marker が推論重みの実行時版である。

• 推論では、どの handler 境界がどの effect family を消費してよいかを決める。
• 実行時 marker は、実際に effect が発生したときの handler search に同じ境界を守らせる。

filter は runtime marker にならない。 solver が静的に検査する。

まとめ

Yulang の現行 effect 推論は、次の分担で成り立つ。

• 普通の値型と effect row は subtyping で推論する。
• handler hygiene は directed weighted inequality T @L <: @R U で表す。
• catch は row head から H ∩ Common(L) だけを引く。
• 右側 pop は head を見せるために使わず、residual tail へ運ぶ。
• handler があるからといって、未知 row を勝手に開かない。
• residual row variable は公開型の一部であり、黙って消さない。
• #id[Empty] のような空の可視性 evidence は、その row occurrence がその boundary で subtraction から守られている証拠であり、新しい effect ではない。
• data 値に保存された effectful 関数の private stack evidence は、ordinary public row へ projection してから表示する。
• replay-cycle subsumption は solver の停止性規則であり、公開型の等式ではない。
• specialize 後は runtime guard marker が同じ hygiene を保つ。

これにより、表示される型は普通の row 型に近く保ちながら、内側 handler が呼び出し元の effect を勝手に奪うことを防いでいる。