Вычитание церковных цифр в хаскеле

Question

Я пытаюсь ввести церковные цифры в Хаскеле, но у меня возникла небольшая проблема.Haskell жалуется на бесконечный тип с

Происходит проверка: не может создать бесконечный тип: t = (t -> t1) -> (t1 -> t2) -> t2

, когда я пытаюсьи сделать вычитание.Я на 99% уверен, что моё лямбда-исчисление действительно (хотя, если это не так, пожалуйста, скажите мне).Что я хочу знать, так это то, что я могу сделать, чтобы Haskell работал с моими функциями.

module Church where

type (Church a) = ((a -> a) -> (a -> a))

makeChurch :: Int -> (Church a)
makeChurch 0 = \f -> \x -> x
makeChurch n = \f -> \x -> f (makeChurch (n-1) f x)

numChurch x = (x succ) 0

showChurch x = show $ numChurch x

succChurch = \n -> \f -> \x -> f (n f x)

multChurch = \f2 -> \x2 -> \f1 -> \x1 -> f2 (x2 f1) x1

powerChurch = \exp -> \n -> exp (multChurch n) (makeChurch 1)

predChurch = \n -> \f -> \x -> n (\g -> \h -> h (g f)) (\u -> x) (\u -> u)

subChurch = \m -> \n -> (n predChurch) m

Answer 1

Проблема в том, что predChurch является слишком полиморфным , чтобы быть правильно выведенным из вывода типа Хиндли-Милнера. Например, заманчиво написать:

predChurch :: Church a -> Church a
predChurch = \n -> \f -> \x -> n (\g -> \h -> h (g f)) (\u -> x) (\u -> u)

но этот тип неверен. Church a принимает в качестве первого аргумента a -> a, но вы передаете n функцию с двумя аргументами, явно ошибку типа.

Проблема в том, что Church a неправильно характеризует церковную цифру. Церковная цифра просто представляет число - что может означать этот тип параметра? Например:

foo :: Church Int
foo f x = f x `mod` 42

Этот тип проверяет, но foo, безусловно, не является церковной цифрой. Нам нужно ограничить тип. Церковные цифры должны работать для любого a, а не только для конкретного a. Правильное определение:

type Church = forall a. (a -> a) -> (a -> a)

Вам нужно иметь {-# LANGUAGE RankNTypes #-} в верхней части файла, чтобы включить такие типы.

Теперь мы можем дать ожидаемую подпись типа:

predChurch :: Church -> Church
-- same as before

Вы должны поставить здесь сигнатуру типов, потому что Хингли-Милнер не может выводить типы более высокого ранга.

Однако, когда мы приступаем к реализации subChurch, возникает другая проблема:

Couldn't match expected type `Church'
       against inferred type `(a -> a) -> a -> a'

Я не уверен на 100%, почему это происходит, я думаю, что forall слишком либерально разворачивается проверщиком типов. Это не удивляет меня все же; типы более высокого ранга могут быть немного ломкими из-за трудностей, которые они представляют для компилятора. Кроме того, мы не должны использовать type для абстракции , мы должны использовать newtype (что дает нам большую гибкость в определении, помогает компилятору проверять типы и отмечает места, где мы используем реализацию абстракции):

newtype Church = Church { unChurch :: forall a. (a -> a) -> (a -> a) }

И мы должны изменить predChurch, чтобы катиться и развертываться по мере необходимости:

predChurch = \n -> Church $ 
    \f -> \x -> unChurch n (\g -> \h -> h (g f)) (\u -> x) (\u -> u)

То же самое с subChurch:

subChurch = \m -> \n -> unChurch n predChurch m

Но нам больше не нужны сигнатуры типов - в броске / развертывании достаточно информации, чтобы снова выводить типы.

Я всегда рекомендую newtype с при создании новой абстракции. Обычные type синонимы довольно редки в моем коде.

Answer 2

Это определение predChurch не работает в простом типе лямбда-исчисления , только в нетипизированной версии. Вы можете найти версию predChurch, которая работает в Haskell здесь .

Answer 3

Я столкнулся с той же проблемой.И я решил это без добавления подписи типа.

Вот решение, с cons car, скопированным с SICP .

cons x y = \m -> m x y
car z = z (\p q -> p)
cdr z = z (\p q -> q)

next z = cons (cdr z) (succ (cdr z))
pred n = car $ n next (cons undefined zero)

sub m n = n pred m

Вы можете найти полный источник здесь .

Я действительно поражен после написания sub m n = n pred m и загрузки его в ghci без ошибки типа!

Код на Haskell настолько лаконичен!: -)