Изваждане на църковни цифри в haskell

Проблемът е, че 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

Вие трябва да дадете сигнатура на типа тук, защото типовете от по-висок ранг не могат да бъдат изведени от Hindley-Milner.

Въпреки това, когато преминем към внедряване на 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

Но вече не се нуждаем от сигнатури на типове -- има достатъчно информация в преобръщането/развиването, за да изведем типовете отново.

Винаги препоръчвам newtypes, когато създавате нова абстракция. Редовните type синоними са доста редки в моя код.

Тази дефиниция на predChurch не работи в просто въведено ламбда смятане, само в нетипизираната версия. Можете да намерите версия на predChurch, която работи в Haskell тук.

Сблъсквал съм се със същия проблем. И го реших без добавяне на подпис на типа.

Ето решението с 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 е толкова кратък! :-)