Реализация арифметических птиц Смулляна в Хаскеле

Question

В поисках информации о книге Рэймонда Смулляна " Чтобы издеваться над пересмешником" я наткнулся на код Хаскелла Стивена Тетли для основных комбинаторов. Я подумал, что это интересная идея, и решил реализовать "птиц, которые могут делать арифметику" из главы 24 " Пересмешить пересмешника", используя эти комбинаторы. Я дошел до определения истинности, ложности, преемника, предшественника и комбинаторов нулевой проверки, а также функций для преобразования комбинаторных логических значений в логические значения Haskell и наоборот. Но когда я пытаюсь создать функцию, которая принимает комбинаторное число и возвращает целое число, я продолжаю сталкиваться с проблемами. Я хотел бы знать, как заставить эту функцию работать. Вот что у меня так далеко:

-- | The first 7 combinators below are from Stephen Tetley's Data.Aviary.Birds
-- | (http://hackage.haskell.org/package/data-aviary-0.2.3/docs/Data-Aviary-Birds.html),
-- | with minor modifications.


-- | S combinator - starling. 
-- Haskell: Applicative\'s @(\<*\>)@ on functions.
-- Not interdefined.
st :: (a -> b -> c) -> (a -> b) -> a -> c
st f g x = f x (g x)

-- | K combinator - kestrel - Haskell 'const'.
-- Corresponds to the encoding of @true@ in the lambda calculus.
-- Not interdefined.
ke :: a -> b -> a
ke a _b = a 

-- | I combinator - identity bird / idiot bird - Haskell 'id'.
id' :: a -> a 
id' = st ke ke 

-- | B combinator - bluebird - Haskell ('.').
bl :: (b -> c) -> (a -> b) -> a -> c
bl = st (ke st) ke

-- | C combinator - cardinal - Haskell 'flip'.
ca :: (a -> b -> c) -> b -> a -> c
ca = st(st(ke st)(st(ke ke)st))(ke ke)

-- | T combinator - thrush.
-- Haskell @(\#)@ in Peter Thiemann\'s Wash, reverse application.
th :: a -> (a -> b) -> b
th = ca id'

-- | V combinator - vireo.
vr :: a -> b -> (a -> b -> d) -> d
vr = bl ca th




-- | The code I added begins here. 




-- | Truth combinator. Functionally superfluous since it can  
-- | be replaced with the kestrel. Added for legibility only.
tr :: a -> b -> a
tr = ke

-- | Falsity combinator.
fs :: a -> b -> b
fs = ke id'

-- | Successor combinator.
sc :: a -> ((b -> c -> c) -> a -> d) -> d
sc = vr fs 

-- | Predecessor combinator.
pd :: ((((a -> a) -> b) -> b) -> c) -> c
pd = th (th id')

-- | Zerocheck combinator.
zc :: ((a -> b -> a) -> c) -> c
zc = th ke



-- | Below are 2 functions for changing combinatory booleans 
-- | to Haskell booleans and vice versa. They work fine as 
-- | far as I can tell, but I'm not very confident about 
-- | their type declarations. I just took the types 
-- | automatically inferred by Haskell.

-- | Combinatory boolean to Haskell boolean.
cbhb :: (Bool -> Bool -> Bool) -> Bool
cbhb cb  = cb True False

-- | Haskell boolean to combinatory boolean.
hbcb :: Bool -> a -> a -> a
hbcb hb | hb     = tr
        | not hb = fs




-- | Combinatory number to Haskell number. 
-- | This is the problematic function that I'd like to implement. 
-- | I think the function is logically correct, but I have no clue
-- | what its type would be. When I try to load it in Hugs it 
-- | gives me a "unification would give infinite type" error. 
cnhn cn | cbhb (zc cn) = 0
        | otherwise    = 1 + cnhn (pd cn)

Вот мое очень грубое предположение о том, что не так с кодом: функция 'cnhn' принимает любое комбинаторное число в качестве аргумента. Но разные комбинаторные числа имеют разные типы, такие как

ноль) id':: a -> a

один) vr(ke id')id':: ((a -> b -> b) -> (c -> c) -> d) -> d

два) vr(ke id')(vr(ke id')id'):: ((a -> b -> b) -> (((c -> d -> d) -> (e -> e) -> е) -> е) -> г) -> г

и так далее. Таким образом, функция, которая принимает любое комбинаторное число в качестве аргумента, должна иметь возможность принимать бесконечно много типов аргументов. Но Haskell не позволяет такие функции.

Чтобы сделать это кратко, вот мои 3 основных вопроса:

1) Что не так с функцией 'cnhn'? (Правильно ли мое предположение выше?)

2) Можно ли это исправить?

3) Если нет, какой другой язык я могу использовать для реализации арифметических птиц Смулляна?

Спасибо за чтение длинного вопроса.

Answer 1

Похоже, что наследник комбинатор не совсем правильно. Вот кодировка церковной арифметики в Хаскеле, unchurch функция это то, что cnhn (Номер церкви в номер Хаскеля, я полагаю?) Пытается осуществить.

tr :: a -> b -> a
tr x y = x

fl :: a -> b -> b
fl x y = y

succ :: ((a -> b) -> c -> a) -> (a -> b) -> c -> b
succ n f x = f (n f x)

unbool :: (Bool -> Bool -> t) -> t
unbool n = n True False

unchurch :: ((Int -> Int) -> Int -> a) -> a
unchurch n = n (\i -> i + 1) 0

church :: Int -> (a -> a) -> a ->a
church n =
  if n == 0
  then zero
  else \f x -> f (church (n-1) f x)

zero :: a -> b -> b
zero = fl

one :: (a -> a) -> a -> a
one = succ zero

two :: (a -> a) -> a -> a
two = succ one

ten :: (a -> a) -> a -> a
ten = succ (succ (succ (succ (succ (succ (succ (succ (succ (succ zero)))))))))

main = do
  print (unchurch ten)
  print (unchurch (church 42))

Таким образом, функция, которая принимает любое комбинаторное число в качестве аргумента, должна иметь возможность принимать бесконечно много типов аргументов. Но Haskell не позволяет такие функции.

Ах, но это так, поскольку Haskell допускает параметрический полиморфизм. Если вы посмотрите на кодировку чисел, все они имеют подпись ((a -> a) -> a -> a) поэтому аргумент функции, принимающей церковный номер, должен иметь только первый аргумент, объединяющий переменные типа своего первого аргумента с функцией, кодирующей церковный номер.

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

mult :: (a -> b) -> (c -> a) -> c -> b
mult m n f = m (n f)

test :: (a -> a) -> a -> a
test = mult ten ten

main = print (unchurch test) -- 100