教会编码(条件)

ant*_*ter 1 haskell church-encoding

我正在尝试写出一些lambda演算,但我不能让教会条件工作.我应该说我是Haskell noob.

我已经在网上和SO上看过解决方案,但它们都涉及引入新类型和其他技巧,但我希望尽可能接近原始语法.例如:

tru :: Integer -> Integer -> Integer
tru = \x -> \y -> x

fals :: Integer -> Integer -> Integer
fals = \x -> \y -> y

main = do
  print (tru 2 3)
  print (fals 5 6)
Run Code Online (Sandbox Code Playgroud)

匹配教堂布尔的确切语法:

\a.\b.a
\a.\b.b 
Run Code Online (Sandbox Code Playgroud)

有没有什么方法可以匹配教堂if/else的确切语法?我正在尝试复制\p.\a.\b.p a b,但我不确定我做错了什么:

ifelse :: Integer -> Integer -> Integer -> Integer -> Integer -> Integer
ifelse = \p -> \a -> \b -> p -> a -> b

main = do
  print (tru 2 3)
  print (fals 5 6)
  print (ifelse tru 42 58)
Run Code Online (Sandbox Code Playgroud)

chi*_*chi 7

你想要的东西

ifelse :: (Integer -> Integer -> Integer) -> Integer -> Integer -> Integer
ifelse = \p -> \a -> \b -> p a b
Run Code Online (Sandbox Code Playgroud)

甚至

ifelse = id
Run Code Online (Sandbox Code Playgroud)

还要记住,你的教会布尔只能应用于整数,这可能是限制性的.您可以通过赋予它们多态类型来使您的编码更加通用.

-- Warning: untested
{-# LANGUAGE RankNTypes #-}
type Cbool = forall a. a->a->a
tru :: Cbool
tru = const
fals :: Cbool
fals = const id
ifelse :: Cbool -> a -> a -> a
ifelse = id
type Cnat = forall a. (a->a)->a->a
zero :: Cnat
zero = \s z -> z   -- const id
-- etc
Run Code Online (Sandbox Code Playgroud)

  • @AndrásKovács对于所有的教堂数字,所有教堂数字都必须是RankNType,`CNum = forall c.(c - > c) - > c - > c`.否则,你可以使用OP的代码来破坏参数并返回一个不是教堂数字的东西,比如`-1`. (3认同)
  • 我在这里注意到,如果我们想对教会数字进行取幂,那么实际上需要rank-n类型. (2认同)