教会のコード変換機能がGADTでコンパイルできない

Question

ここには示されていない無関係のコード部分に使用するGADT拡張機能でコンパイルするときに、タイプエラーが発生するため、以下の関数が拒否されます。

newtype Church = Church { unC :: forall a. (a -> a) -> a -> a } 
to_c :: Int -> Church 
to_c 0 = let f0 f c = c in Church f0 
to_c n = 
    let fn f c = iterate f c !! n in Church fn 

エラーメッセージ：

Couldn't match type ‘a0’ with ‘a’ because type variable ‘a’ would escape its scope 
    This (rigid, skolem) type variable is bound by 
    a type expected by the context: 
     (a -> a) -> a -> a 

    Expected type: (a -> a) -> a -> a 
    Actual type: (a0 -> a0) -> a0 -> a0 
    In the first argument of ‘Church’, namely ‘fn’ 

は、私は仕事もチェックして入力します直接の再帰的なスタイルで関数を書き換えることができます。しかし、なぜこの反復的なアプローチに欠陥があるのか​​、そしてそれが巧妙な型の注釈で救済できるのかどうか不思議でした。

Answer 1

これは実際にはGADTとは関係ありません。-XGADTsの拡張子は-XMonoLocalBindsを意味します。これは実際の問題です。ローカルバインディングfnは明示的な署名を持たないため、環境よりも多型ではない型を与えたいからです。つまり、この場合はは多態性ではありません。です。しかし、もちろんはが多形でなければならないので、実際にはChurchタイプで使用できるので、それは良いことではありません。

あなたはまだ明示多型署名与えることができます：

{-# LANGUAGE RankNTypes, MonoLocalBinds #-} 
newtype Church = Church { unC :: forall a. (a -> a) -> a -> a } 
to_c :: Int -> Church 
-- to_c 0 = ... -- the base case is redundant. 
to_c n = 
    let fn :: (a -> a) -> a -> a 
     fn f c = iterate f c !! n 
    in Church fn 

をもっと簡単ソリューションは、ちょうどすべてでを結合し、-XMonoLocalBindsが遊びに来ていない任意のをしないことです。

to_c :: Int -> Church 
to_c n = Church (\f c -> iterate f c !! n) 

...または、あなたがバインド作るのですかあればそこ環境がすでに多型であるため、Churchコンストラクタの中でそれを実行します。

to_c n = Church (let fn f c = iterate f c !! n in fn)