haskell-jp / random #105 at 2024-01-23 11:33:14 +0900

Tc.Pluginで制約解消アルゴリズムにヒューリスティクスを適用することって、理論上可能ですかね？GPTなど
調べた限りでは類似したものは見当たらなかったのですが

ヒューリスティクスの定義によると思いますが、普通に副作用を出せるので出来ますね

何をもってヒューリスティクスと呼んでいるのかわかりませんが、SMTソルバをヒューリスティクスに数えてよいのであれば、こんなのがあります

https://github.com/bgamari/the-thoralf-plugin
https://hackage.haskell.org/package/sbvPlugin

これらや Liquid Haskell の Plugin 版は外部の Z3 を呼び出して処理しているので、同じようにして tcPluginIO 関数などを使って GPT の API と通信しようとすれば基本的に何でも組込めると思います。とはいえ、ちゃんとしたソルバではなくて GPT とかが生成した制約の「証明」がちゃんと証明になっているかどうかは出力をバリデートする必要があると思います

@Hiromi ISHII / mr_konn
なるほど。ヒューリスティックというのは、統計的手法による型推論をイメージしていましたが、SMTソルバも参考になります。

GHCの型推論はすでに十分強力なので、これを利用して逆に制約から項を自動生成できないかなどを考えています

なるほどなるほど

型クラス制約までは考慮に入れてくれたかどうかは覚えていませんが、単純な型から項を自動生成プラグインとしては、（今メンテされているかはわかりませんが）ghc-justdoit というのがありますね

https://github.com/nomeata/ghc-justdoit

ありがとうございます

何か面白い物ができたらぜひ教えてください :+1: