ファンクターのフィックスポイントがある場合:
Fix f = Con (f (Fix f))
が ではない場合、(たとえば を使用して) 無限ループを簡単に記述できるため、関数out : Fix f -> f (Fix f)を使用するのは安全ではありません。fFunctorf x = x -> x
Fix私の質問:メンドラー スタイルのパラモーフィズムでしか排除できない場合 (fが でなくてもFunctor)、無限ループを書くことは可能ですか?
Mendler スタイルのパラモーフィズムでは、次のタイプを考えています。
mpara : (forall r. (r -> Fix f) -> (r -> t) -> f r -> t) -> Fix f -> t
が実際にファンクタであるout場合にのみ記述できるため、答えはノーです。f
out : Functor f => Fix f -> f (Fix f)
out = mpara (\expose rec y. fmap expose y)
つまり、mpara任意の で安全に使用できfます。私は正しいですか？