Я изучаю Haskell и пытаюсь написать функцию, которая преобразует число Черча в Int. Мой код работает, только если я не пишу сигнатуру типа.
type Church a = (a -> a) -> a -> a
zero :: Church a
zero s z = z
c2i :: Church a -> Int -- This line fails
c2i x = x (+1) 0
У меня есть правильная подпись типа c2i с использованием :t c2i
c2i :: (Num a1, Num a) => ((a -> a) -> a1 -> t) -> t
но мне интересно, почему это?
Если вы используете a в подписи c2i, она должна работать с любым a. Другими словами, a выбирается вызывающим вашей функции. Конкретно, он должен работать с
c2i :: Church String -> Int
-- that is
c2i :: ((String -> String) -> String -> String) -> Int
Поскольку код не работает при a = String, полиморфный тип недействителен.
Если вы не добавите тип, компилятор сможет вывести какой-то тип, заставив код работать. Более простой тип может быть:
c2i :: Church Int -> Int
или, после включения нескольких расширений,
c2i :: (forall a. Church a) -> Int
В последнем случае мы указываем, что a выбирается c2i, а не вызывающим абонентом. Вместо этого вызывающая сторона должна передать аргумент, который должен иметь полиморфный тип: то есть он должен передать Church a для всех a, а не только Church String.
В качестве альтернативы можно даже объявить
type Church = forall a . (a->a)->a->a
и передавать только полиморфные значения.
