Djinn

で、上の話と関係しなくもないけど、与えられた型を持つhaskellの関数を返してくれるらしい
http://lambda-the-ultimate.org/node/1178

原理がよく分からん。

For the curious, Djinn uses a decision procedure for intuitionistic
propositional calculus due to Roy Dyckhoff. It's a variation of
Gentzen's LJ system. This means that (in theory) Djinn will always
find a function if one exists, and if one doesn't exist Djinn will
terminate telling you so.

んー、例えば型( (a,b) , (c,d) ) -> (b,c)があったら、命題(A and B) and (C and D)=>(B and C)の証明を探索して、見つかったら、証明を関数に翻訳するという感じなのかな

System Fで、型forall x.x->x->xを持つclosed termを全部見つけるとか、そういうことできないのかなぁ。全部っても、forall x.(x->x)->x->xとかだと、普通に無限個あるんで、停止しないわけだけど。まぁ、普通に考えて無理そうだよなぁ。更にHaskellでは、fix(定義:fix f = f (fix f))とかseqのおかげで、forall x.xとか、forall a b.a->bみたいなキモイ型を持つclosed termが存在したりするわけだけど。