哈斯克尔教会数字减法

Question

我正试图在哈斯克尔实现教会数字，但我遇到了一个小问题。 Haskell的抱怨无限型与

的发生检查：无法构造无限类型：T =（T - > T1） - 当我尝试做减法> T2

- >（T1 - > T2）。我99％肯定我的lambda微积分是有效的（尽管如果不是，请告诉我）。我想知道的是，是否有任何事情可以让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

这个定义的predChurchdoesn't work in simply typed lambda calculus，只有在非类型化版本。你可以找到一个在Haskell here工作的predChurch版本。

Answer 2

问题是predChurch是太多态性由Hindley-Milner类型推断正确推断。例如，人们很容易写：

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

但这种类型是不正确的。 A Church a将第一个参数设为a -> a，但您传递的是n两个参数函数，显然是一个类型错误。

问题是，Church a没有正确描述教会的数字。教会的数字只是一个数字 - 这个类型参数究竟意味着什么？例如：

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

这typechecks，但foo肯定不是一个教会的数字。我们需要限制类型。教会数字需要为任何a工作，而不仅仅是一个特定的a。正确的定义是：

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

你需要有{-# LANGUAGE RankNTypes #-}在文件的顶部，使种这样。

现在我们可以给类型签名我们预计：

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

您必须这里举一个类型签名，因为较高等级的类型不被辛德米尔纳inferrable。

然而，当我们去实现subChurch产生了另一个问题：

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

我不是100％肯定，为什么出现这种情况，我认为forall正在被typechecker过于随意展开。尽管如此，我并不感到意外;由于它们向编译器呈现的困难，更高等级的类型可能有点脆弱。此外，我们不应该使用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 

但我们并不需要类型签名了 - 没有在卷/ UNROLL再次推断类型的足够信息。

我总是建议newtype S创建一个新的抽象时。定期type同义词在我的代码中很少见。

Answer 3

我遇到了同样的问题。我解决了它，但没有添加类型签名。

以下是解决方案，其中conscar从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 

你可以找到完整的来源here。

我写sub m n = n pred m后感到惊讶，并在ghci中载入它没有类型的错误！

Haskell代码是如此简洁！ :-)