在哈斯克尔教会数字的减法 [英] Subtraction of church numerals in haskell

问题描述

我试图在Haskell中实施教会数字，但我遇到了一个小问题。 Haskell抱怨无限类型：

发生检查：无法构造无限类型：t =（t - > t1） - >（t1 - > t2） - > t2当我尝试做减法时，

。我99％肯定我的lambda微积分是有效的（尽管如果不是，请告诉我）。我想知道的是，是否有任何事情可以让haskell在我的函数中工作。

  module教会其中
 
类型（教会a）=（（a  - > a） - >（a  - > a））
 
 makeChurch :: Int  - > （Church a）
 makeChurch 0 = \f  - > \x  - > x 
 makeChurch n = \f  - > \x  - > f（makeChurch（n-1）fx）
 
 numChurch x =（x succ）0 
 
 ShowChurch x =显示$ numChurch x 
 
 succChurch = \\\
  - > \f  - > \x  - > f（n f x）
 
 multChurch = \f2  - > \x2  - > \f1  - > \x1  - > f2（x2 f1）x1 
 
 powerChurch = \exp  - > \\\
  - > exp（multChurch n）（makeChurch 1）
 
 predChurch = \\\
  - > \f  - > \x  - > （\ u  - > u）
 
 subChurch = \m（n）（\ g  - > \ h  - > h（gf）） - > \\\
  - > （n predChurch）m 
  

解决方案

问题在于 predChurch 是太多态，可以通过Hindley-Milner类型推断正确推断。例如，写下以下内容很诱人：

  predChurch :: Church a  - >教堂
 predChurch = \\\
  - > \f  - > \x  - > （\ u  - > u）
  

但这种类型不正确。 A Church a 以第一个参数作为 a - >一个，但是你传递了 n 一个两个参数函数，显然是一个类型错误。

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

  foo :: Church Int 
 foo fx = fx`mod` 42 
  code> 

这种类型检测，但 foo 肯定不是教会的数字。我们需要限制类型。教会的数字需要为 a ，而不仅仅是特定的 a 。正确的定义是：

  type Church = forall a。 （a  - > a） - > （a  - > a）
  

您需要 { - ＃LANGUAGE RankNTypes＃ - } 来启用这样的类型。

现在我们可以给出我们期望的类型签名： p>

  predChurch :: Church  - > Church 
  - 与之前相同
  

You 必须给出因为更高等级的类型不能被Hindley-Milner推断出来。

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

 无法匹配预期类型'Church'
与推断类型'（a  - > a） - > a  - > a'
  

我不是100％确定为什么发生这种情况，我认为 fopell 被typechecker过于宽松地展开。尽管如此，我并不感到意外;由于它们向编译器呈现的困难，更高等级的类型可能有点脆弱。此外，我们不应该为抽象使用类型，我们应该使用 newtype （这给了我们更多的定义灵活性，帮助编译器进行类型检查，并标记我们使用抽象实现的地方）：

  newtype Church = Church {unChurch :: forall a。 （a  - > a） - > （a  - > a）} 
  

我们必须修改 predChurch 根据需要进行滚动和展开：

  predChurch = \\\
  - >教会$ 
 \f  - > \x  - > （\ u  - > u）
  

与 subChurch 相同：

  subChurch = \m  - > \\\
  - > unChurch n predChurch m 
  

但我们不再需要类型签名 - 滚动/展开以再次推断类型。

创建新抽象时，我总是推荐 newtype s。定期类型同义词在我的代码中很少见。

I'm attempting to implement church numerals in Haskell, but I've hit a minor problem. Haskell complains of an infinite type with

Occurs check: cannot construct the infinite type: t = (t -> t1) -> (t1 -> t2) -> t2

when I try and do subtraction. I'm 99% positive that my lambda calculus is valid (although if it isn't, please tell me). What I want to know, is whether there is anything I can do to make haskell work with my functions.

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

解决方案

The problem is that predChurch is too polymorphic to be correctly inferred by Hindley-Milner type inference. For example, it is tempting to write:

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

but this type is not correct. A Church a takes as its first argument an a -> a, but you are passing n a two argument function, clearly a type error.

The problem is that Church a does not correctly characterize a Church numeral. A Church numeral simply represents a number -- what on earth could that type parameter mean? For example:

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

That typechecks, but foo is most certainly not a Church numeral. We need to restrict the type. Church numerals need to work for any a, not just a specific a. The correct definition is:

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

You need to have {-# LANGUAGE RankNTypes #-} at the top of the file to enable types like this.

Now we can give the type signature we expect:

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

You must give a type signature here because higher-rank types are not inferrable by Hindley-Milner.

However, when we go to implement subChurch another problem arises:

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

I am not 100% sure why this happens, I think the forall is being too liberally unfolded by the typechecker. It doesn't surprise me though; higher rank types can be a bit brittle because of the difficulties they present to a compiler. Besides, we shouldn't be using a type for an abstraction, we should be using a newtype (which gives us more flexibility in definition, helps the compiler with typechecking, and marks the places where we use the implementation of the abstraction):

newtype Church = Church { unChurch :: forall a. (a -> a) -> (a -> a) }

And we have to modify predChurch to roll and unroll as necessary:

predChurch = \n -> Church $ 
    \f -> \x -> unChurch n (\g -> \h -> h (g f)) (\u -> x) (\u -> u)

Same with subChurch:

subChurch = \m -> \n -> unChurch n predChurch m

But we don't need type signatures anymore -- there is enough information in the roll/unroll to infer types again.

I always recommend newtypes when creating a new abstraction. Regular type synonyms are pretty rare in my code.

这篇关于在哈斯克尔教会数字的减法的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！