Функция преобразования церковного кодирования не компилируется с GADT

Question

to_c Приведенная ниже функция отклонена из-за ошибки типа при компиляции с расширением 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

Это действительно не имеет ничего общего с ГАДЦ, только -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)