将定点运算符翻译成 Haskell 语言

Posted 2023-03-28

【中文标题】将定点运算符翻译成 Haskell 语言

【英文标题】：Translating a fixed-point operator to Haskell language

【发布时间】：2021-10-28 16:55:06

【问题描述】：

我正在尝试将这个 JS 定点运算符翻译成 Haskell。

JS：

const fix = F => 
    const D = X => F(
        t => X(X)(t)
    )
    return D(D)
;

我的尝试是（Haskell）：

fix' f = d d
  where
    d x = f (\t -> x x t)

但是，我收到以下错误：

Couldn't match expected type ‘(t2 -> t3) -> t4’
              with actual type ‘p’
because type variables ‘t2’, ‘t3’, ‘t4’ would escape their scope
These (rigid, skolem) type variables are bound by the inferred type of d :: (t1 -> t2 -> t3) -> t4

有人知道这里发生了什么吗？

【问题讨论】：

一个众所周知的问题是像 Y 这样的定点组合子不能在 Haskell 中很好地键入。具体来说，x x 形式的东西要求x 同时具有两种冲突的类型。在动态语言中，这无关紧要，因为您只是不关心类型是什么，只是您可以以某种方式使用该值。但是 Haskell 编译器确实在乎。但是不需要这样的组合器，因为 Haskell 的解决方案 fix f = let x = f x in x 更优雅，并且没有打字困难（但确实需要惰性求值）。

像x x 这样的自我应用程序在haskell 中失败，因为它不能很好地键入。有一些魔法可以让它的一些变体起作用，但你不需要那个。要定义一个有效的定点运算符，只需使用递归，例如fix f = f (fix f)（有更高效的，但这是最简单的）。

【参考方案1】：

在自我应用程序d d 中，d 既是某个类型为a -> r 的函数，也是它的参数类型为a。因此这两种类型必须是同一种，a ~ (a -> r)。

Haskell 想要完全预先知道它的类型，所以它不断用一个替换另一个，最终得到一个无限类型。

Haskell 中不允许使用无限类型，但允许使用递归类型。

这里我们需要做的就是命名递归类型：

newtype T r = D  app :: T r -> r 

现在T r 既是函数类型又是它的参数，对于某些结果类型r。

这里T是一个类型构造函数，D是它的数据构造函数D :: (T r -> r) -> T r。

上面的记录语法定义了一个新的数据类型（虽然这里使用关键字newtype，而不是data）并将其单个字段命名为app。它还将app 定义为访问函数app :: T r -> (T r -> r)。 _{(这是D的一种倒数，并且经常看到这样的函数以“un”为前缀命名，比如app本来可以命名为unD。但这里app是有道理的，因为我们稍后会看到。）}

对于T r、x :: T r 类型的值x，这意味着x 是/匹配/某个值D g 其中(g = app x) :: T r -> r，即app 只是展开数据构造函数D 获取基础值（函数）g：x = D g ; app x = app (D g) = g。这就是 Haskell 中记录语法的工作原理。

现在我们可以写了

- fix' f = d d
     where
       d x = f (\t -> x x t)   -- applying x to x can't be typed!
-

fix1 :: ((t1 -> t) -> t1 -> t) -> t1 -> t
fix1 f = d (D d)
  where
    d x = f (\t -> app x x t)   -- `app`ing x to x is well-typed!

fix2 :: ((t1 -> t) -> t1 -> t) -> t1 -> t
fix2 f = d (D d)
  where
    d (D y) = f (\t -> y (D y) t)

fix3 :: ((t1 -> t) -> t1 -> t) -> t1 -> t
fix3 f = f (\t -> d (D d) t)
  where
    d (D y) = f (\t -> y (D y) t)

fix4 :: (t -> t) -> t
fix4 f = f (d (D d))
  where
    d (D y) = f (y (D y))

所有工作。最后一个甚至与内置fix的类型相同。

但 Haskell 不仅有递归类型。它本身也有递归。实体被允许在其自己的定义中引用自身。

因此，正如 cmets 所说，我们真的不需要通过自我应用作为参数传递的值来模拟递归。我们可以递归地使用被定义的函数本身：

fix0 :: (t -> t) -> t
fix0 f  =  f (fix0 f)

或者我们可以使用递归定义的值：

y :: (t -> t) -> t
y f  =  x  where   x = f x 

---

关于错误，秒类型错误you get，

prog.hs:3:22: error:
    • Occurs check: cannot construct the infinite type:
        t1 ~ t1 -> t2 -> t3
    • In the first argument of ‘x’, namely ‘x’
      In the expression: x x t
      In the first argument of ‘f’, namely ‘(\ t -> x x t)’
    • Relevant bindings include
        t :: t2 (bound at prog.hs:3:15)
        x :: t1 -> t2 -> t3 (bound at prog.hs:3:7)
        d :: (t1 -> t2 -> t3) -> t4 (bound at prog.hs:3:5)
  |
3 |     d x = f (\t -> x x t)
  |                      ^

似乎比你包含的那个更中肯/有帮助/。

【讨论】：

再次感谢您！你能解释一下“app x x t”这一行吗？

我已经编辑过了。 :) app x x t 与 case x of (D g) -> g (D g) t 相同。 Haskell 的应用是柯里化的，所以a b c 真的是(a b) c。出于同样的原因，a :: b -> c -> r 的类型实际上是 a :: b -> (c -> r)。据说在Haskell中，左边是application associate，右边是type arrows associate。