1940 年代的函数式编程：阶乘的简约实现

Question

我已经看过 John Hughes 题为 Why Functional Programming Matters 的精彩演讲几次，直到最近才决定实际尝试实现布尔值、整数，当然还有阶乘的“极简”版本，如 video 所示.

我实现了true、false、ifte、zero、one、two、iszero、decr，最后是facthere，如下所示：

-- boolean
true x y = x
false x y = y
ifte bool t e = bool t e

-- positive integers
three f x = f $ f $ f x
two f x = f $ f x
one f x = f x
zero f x = x 

-- add and multiplication
add m n f x = m f $ n f x
mul m n f x = m (n f) x 

-- is zero check
iszero n =  n (\_ -> false) true

-- decrement
decr n = 
  n (\m f x -> f (m f zero))
    zero
    (\x->x)
    zero


-- factorial
fact n =
  ifte (iszero n)
    one
    (mul n (fact (decr n)))

问题

我测试了每个函数，除了decr 和fact 之外，它们都可以完美地编译和工作。

尽管 John Hughes 在 6:37 承诺他的 decr 实现有效，但它无法编译并出现以下错误：

错误：变量不在范围内：incr

我不确定incr 应该如何在(\m f x -> f (m incr zero)) 中实现。

现在，如果我将它们定义为 incr = (+1) 并将 decr 的定义更改为以下内容，那么 decr 可以编译并正常工作，但 fact 仍然会导致编译失败。

decr n = 
  n (\m f x -> f (m incr x))
    zero
    (\x->x)
    zero'

decr 的定义中使用的 lambda (\m f x -> f (m incr zero)) 是否存在错误，或者是否应该以不同的方式定义 incr？

更新

当我将incr 定义为incr n = (\f x -> f (n f x)) 时，decr n 工作正常，但fact n 无法编译。这是错误消息的可读部分：

factorial.hs:30:1: 错误： • 发生检查：无法构造无限类型：

...

|事实 n =
| ^^^^^^^^...

...

factorial.hs:33:6: 错误： • 发生检查：无法构造无限类型：

...

• In the third argument of ‘ifte’, namely ‘(mul n (fact (decr n)))’
  In the expression: ifte (iszero n) one (mul n (fact (decr n)))
  In an equation for ‘fact’:
      fact n = ifte (iszero n) one (mul n (fact (decr n)))

...

| (mul n (fact (decr n)))
| ^^^^^^^^^^^^^^^^^^^^^

注意：完整的错误信息长达几页。

Answer 1

看起来你真的很亲密

我可以向你展示如何在 JavaScript 中使用 Church's encodings 来做到这一点，但在 Haskell 中却不行，因为我不知道如何在 Haskell 中进行一些简单的组合器类型检查（下面的U）

由于 JavaScript 是严格评估的，谓词分支必须包装在 lambda 中

继续运行 sn-p - 我们计算 8!

const True = a => b =>
  a ()
  
const False = a => b =>
  b ()
  
const IsZero = n =>
  n (x => False) (True)

const Succ = n =>
  f => x => f (n (f) (x))
  
const Pred = n =>
  f => x => n (g => h => h (g (f))) (u => x) (u => u)

const Mult = m => n =>
  f => m (n (f))
  
const Add = m => n =>
  m (Succ) (n)

const one = f => x =>
  f (x)
  
const two =
  Add (one) (one)
  
const four =
  Add (two) (two)
  
const eight =
  Add (four) (four)

const U = f => f (f)

const Fact = U (f => acc => n =>
  IsZero (n)
    (z => acc) // thunks used for predicate branches
    (z => U (f) (Mult (acc) (n)) (Pred (n)))) (one)
    
const result = 
  Fact (eight)
  
// convert church numeral result to a JavaScript number
console.log ('8! =', result (x => x + 1) (0))
// 8! = 40320

如果你稍微作弊，你可以通过使用 JavaScript 的 ?: 三元运算符来实现虚假的懒惰——我只是展示这个，以便你可以以更易读的形式看到 Fact；上面的实现只使用了 lambdas

const IsZero = n =>
  // cheat by returning JavaScript's true/false booleans
  n (x => false) (true)

const Succ = n =>
  f => x => f (n (f) (x))
  
const Pred = n =>
  f => x => n (g => h => h (g (f))) (u => x) (u => u)

const Mult = m => n =>
  f => m (n (f))
  
const Add = m => n =>
  m (Succ) (n)

const one = f => x =>
  f (x)
  
const two =
  Add (one) (one)
  
const four =
  Add (two) (two)
  
const eight =
  Add (four) (four)

const U = f => f (f)

const Fact = U (f => acc => n =>
  IsZero (n)
    ? acc // now we're sorta cheating using JavaScript's ternary here
    : U (f) (Mult (acc) (n)) (Pred (n))) (one)

const result = 
  Fact (eight)
  
console.log ('8! =', result (x => x + 1) (0))
// 8! = 40320

Answer 2

首先，让我们尝试显式键入所有内容。天真地，所有这些东西都是在 Church 函数处理的某种类型上参数化的：

type Logical a = a -> a -> a
type Nat a = (a->a) -> a->a

-- boolean
true, false :: Logical a
true x y = x
false x y = y

ifte :: Logical a -> a -> a -> a
ifte = id

incr :: Nat a -> Nat a
incr n f = f . n f

-- integer “literals”
zero, one, two, three :: Nat a
three = incr two
two   = incr one
one   = incr zero
zero _ = id

-- addition and multiplication
add, mul :: Nat a -> Nat a -> Nat a
add m n f = m f . n f
mul m n f = m $ n f

-- zero check
isZero :: Nat a -> Logical a
isZero n = n (const false) true

...好吧，这里我们遇到了第一个问题：

• Couldn't match expected type ‘Logical a’ with actual type ‘a’
  ‘a’ is a rigid type variable bound by
    the type signature for:
      isZero :: forall a. Nat a -> Logical a
    at /tmp/wtmpf-file7834.hs:25:1-28
• In the expression: n (const false) true

问题是我们尝试使用Nat-church-numbers 作为函数，而不是在结果Logical 应该使用的底层a 类型上，而是在这些逻辑本身上。 IE。其实是

isZero :: Nat (Logical a) -> Logical a

decr 变得更糟——这不起作用：

decr :: Nat a -> Nat a
decr n = n (\m f x -> f (m incr x))
           zero
           id
           zero

因为您试图将数字用于isZero 中的逻辑目的，这需要注入另一个Nat 层，但也用于传递/递增。在传统的 Hindley-Milner 中，您需要决定其中之一，因此无法对其进行类型检查。

在现代 Haskell 中，您可以对其进行类型检查，方法是将参数设为多态：

{-# LANGUAGE RankNTypes, UnicodeSyntax #-}
decr :: (∀ α . Nat α) -> Nat a

为了避免携带量词，我们可能会制作另一个同义词：

type ANat = ∀ α . Nat α

那就是

decr :: ANat -> Nat a

该技术也适用于阶乘：

fact :: ANat -> Nat a
fact n = ifte (isZero n)
      one
      (mul n $ fact (decr n))