#haskell #lambda-calculus
Вопрос:
Я следую руководству в Википедии о том, как обращаться с церковными буквами. В соответствии со статьей есть фрагмент Хаскелла:
Ссылка на Вики Здесь
type Church a = (a -> a) -> a -> a
church :: Integer -> Church Integer
church 0 = f -> x -> x
church n = f -> x -> f (church (n-1) f x)
unchurch :: Church Integer -> Integer
unchurch cn = cn ( 1) 0
Однако, когда я пытаюсь запустить его через GHCI, я получаю следующую ошибку :
main.hs:3:15: error:
* Expecting one more argument to `Church'
Expected a type, but `Church' has kind `* -> *'
* In the first argument of `Show', namely `Church'
In the instance declaration for `Show Church'
|
3 | instance Show Church where
Я пытался использовать deriving show
этот тип, а также
instance Show Church Integer where
show = church
И, к сожалению, оба привели к большему количеству ошибок. Я не уверен, что Church Integer
означает объявление функции или это та часть, из-за которой я не могу вывести show?
Как я могу заставить эту функцию печатать?
Комментарии:
1. Попробовать
instance Show (Church Integer) where
?2. Можете ли вы добавить ссылку на учебник, пожалуйста? Я не уверен, понимаю ли я, как вы можете создать экземпляр Show для функции.
3. @DimaKurilo Хорошая мысль, отредактировал ОТ
4. Что ж, похоже, в этом руководстве нет примера показа. И вы не можете определить его для типа (без расширения языка). Так что, скорее всего, вы хотите показать не Церковь, а что-то вроде (unchurch . церковь) 5
Ответ №1:
Идиоматический способ-определить его как новый тип, a
который также должен быть универсально количественно определен
>> church 10
10
{-# Language GADTs #-}
{-# Language InstanceSigs #-}
{-# Language RankNTypes #-}
{-# Language ScopedTypeVariables #-}
{-# Language StandaloneKindSignatures #-}
{-# Language TypeApplications #-}
import Data.Kind
type Church :: Type
newtype Church where
Church :: (forall a. (a -> a) -> (a -> a)) -> Church
church :: Integer -> Church
church n = Church (ch n) where
ch :: Integer -> forall a. (a -> a) -> (a -> a)
ch 0 succ zero = zero
ch n succ zero = succ (ch (n-1) succ zero)
unchurch :: Church -> Integer
unchurch (Church church) = church @Integer ( 1) 0
instance Show Church where
show :: Church -> String
show = show . unchurch
Комментарии:
1. Я не уверен, что правильно это понимаю. Запуск
church 10
должен возвращать что-то вродеf(f(f(f(f(f(f(f(f(x)))))))))
не просто 10. Или я неправильно понял?2. Вот что вы получите, если измените
show
определение:show (Church church) = church (x -> "f(" x ")") "x"