haskell - FundepsとGADT：タイプチェックはいつ決定可能ですか？

Question

私はHaskellとHListがどのように実装されているかについての研究論文を読んでいて、説明されている手法がタイプチェッカーにとって決定可能であるかどうか疑問に思っていました。また、GADTでも同様のことができるので、GADTの型チェックは常に決定可能かと思いました。

説明を読んだり理解したりできるように、引用があればいいと思います。

ありがとう！

Answer 1

私は、GADT 型チェックは常に決定可能であると信じています。高次の統一が必要なため、決定できないのは推論です。しかし、GADT 型チェッカーは、たとえば、. コンストラクターが証明項を構築する Coq。たとえば、ラムダ計算を GADT に埋め込む古典的な例には、各縮約規則のコンストラクターがあるため、項の正規形を見つけたい場合は、どのコンストラクターがそれに到達するかを伝える必要があります。停止の問題はユーザーの手に委ねられました :-)

Answer 2

おそらく既にご覧になっていると思いますが、この問題に関する一連の論文が Microsoft research: Type Checking papersにあります。最初のものは、Glasgow Haskell コンパイラで実際に使用されている決定可能なアルゴリズムについて説明しています。