@elpinal ありがとうございます。こういうフィードバックがもらえる機会はあまりないので、ありがたいです
@elpinal ありがとうございます。こういうフィードバックがもらえる機会はあまりないので、ありがたいです
@elpinal scope があるのはあくまで変数生成においてであって、変数のインスタンス化が起こるところではなく、これは Algorithm W でも取り入れられると思っています (Algorithm W も、単一化で変数を生成しているわけではなく、また別に生成した変数を最後まで残す必要はないので。逆に bidirectional typing で残す実装にしてもいいはずです)
@elpinal Sub 規則では、基本 G |- e <= t1 の parameter G, e, t1 が全て入力になるわけですが、そこから G |- e => t2 で、e の型 t2 を synthesize して、synthesize した t2 から入力の t1 が subtyping 関係を満たせるかという検証を行います。これは、例えば subtyping が equal しかないならまさに unification で、t1, t2 が変数を全く含まない場合も、変数を複数含むことも、どちらも単なる変数でない大きな型であることもありえます。実際、https://dl.acm.org/doi/10.1145/2500365.2500582 では、subtyping の検証で変数と型の比較以上のことをしていて、その過程で変数のパターンマッチを行うため、hat{a} = t みたいな制約を環境に入れてます。変数の cyclic 使用のチェックなども入っていて、個人的には MM unification algorithm の純粋な拡張に思えました
@elpinal 確かに、Agda のコードを読んでましたが、あまり双方向検査やってないように思えてきましたね。ちょっと修正しときます
ついでに、bidirectional typechecking で単一化が必要ないって話ってどこが発祥かご存知ですか？少なくとも、https://dl.acm.org/doi/10.1145/2500365.2500582 を読んだ感じは、単一化相当のものは sub 規則で必要になってましたし、単一化アルゴリズムを直接使うような構成方法も普通にできるように思えました。また、今のところ単一化が入ってないことを要件にしている文献が見つけられていません
@elpinal ただ、Agda はそこまで使ったことはないので、あまり自信がなくて、https://github.com/agda/agda/blob/71a6396ba727768910ed48e2da910532fdb66a63/src/full/Agda/TypeChecking/CheckInternal.hs は双方向検査 (unification あり) が入ってそうですし、bidirectional type checker とコメントに書いてあるので、共通認識がありそうな気がするんですが、こいつが表層レベルの推論で使われているかは https://github.com/agda/agda/blob/71a6396ba727768910ed48e2da910532fdb66a63/src/full/Agda/TypeChecking/Rules/Term.hs 見てもよくわからないなって感じでした
@elpinal なるほど？僕個人は unification を使わないことは、bidirectional typing の定義には含んでいませんでした。実際、さっき書いた記事は unification っぽいことは普通にしてますね
https://arxiv.org/pdf/1908.05839.pdf でも、
> Another extension to ... use bidirectional typing to produce GADT-related
annotations, which provide the missing information for non-bidirectional type inference. OutsideIn ... also use bidirectional typing for
GADTs. Both use unification to propagate equality information.
とあり、unification を使わないことは bidirectional typing の要件に入ってないように思えます
@elpinal Scala の方は嘘だった... 訂正しました。申し訳ないです。指摘ありがとうございます。
Agda の方は合ってそうです。一応注釈つけときました。https://github.com/agda/agda/blob/71a6396ba727768910ed48e2da910532fdb66a63/src/full/Agda/TypeChecking/CheckInternal.hs を軽く流し読みした感じは、双方向に検査する実装使ってそうですね
@elpinal 嘘かもしれない。https://plfa.github.io/20.07/Inference/#bidirectional-inference-in-agda を見て雑にそうなんだとか思ってたが、そういや後でちゃんと調べようと思ってそのままにしてた... ちょっと調べて後で参考注釈足しときます
書いた | 続くといいな日記 – 双方向型検査: 検査と構築の融合 https://mizunashi-mana.github.io/blog/posts/2023/02/bidirectional-typing/
