修复只能用非严格评估语言键入吗?

Question

我在Javascript中编写了一个运行时类型检查器，但无法键入fix：

fix :: (a -> a) -> a
fix f = ...
fix (rec n -> if n == 0 then 1 else n * rec (n-1)) 5 -- 120

传递给fix的阶乘函数具有简化的类型(Int -> Int) -> Int -> Int。

当我尝试在 Javascript 中重现表达式时，由于约束无效Int ~ Int -> Int，我的类型检查器失败了。

fix (const "hallo")也会失败，类型检查器抱怨它无法构造无限类型(负发生检查)。

对于其他组合子，我的统一结果与哈斯克尔的结果一致。

我的单构算法可能是错误的，还是只能在非严格环境中键入fix？

[编辑]

我在Javascript中实现fix是const fix = f => f(f)。

Answer 1

这是类型检查器中的一个错误。

的确，Haskell对fix的天真定义在Javascript中并没有终止：

> fix = (f) => f(fix(f))
> factf = (f) => (n) => (n === 0) ? 1 : n * f(n - 1)
> fact = fix(factf) // stack overflow

您必须使用eta扩展定义以防止fix(f)的循环评估：

> fix = (f) => (a) => f(fix(f), a)
> factf = (f, a) => (a == 0) ? 1 : a * f(a - 1)
> fact = fix(factf)
> fact(10) // prints 3628800

Answer 2

事实证明，您尝试实现U组合器，它不是一个定点组合器。

而定点Y 组合子_Yg = g (_Y g)使我们能够编写

_Y (r x -> if x==0 then 1 else x * r (x-1)) 5     -- _Y g => r = _Y g
-- 120

有了_Ug = g (g)我们必须写

_U (f x -> if x==0 then 1 else x * f f (x-1)) 5   
-- _U g => f = g, f f == _U g

正如你所发现的，这个_U在 Haskell 中没有类型。一方面g是一个函数，g :: a -> b;另一方面，它将自己作为第一个参数接收，因此它要求对任何类型的a和ba ~ a -> b。

立即用a -> b代替a -> b中的a会导致无限递归(参见"发生检查")，因为(a -> b) -> b仍然有需要用a -> b替换的a; ad infinitum。

一个解决方案可能是引入递归类型，将a ~ a -> b转换为R = R -> b即

newtype U b = U {app :: U b -> b}      -- app :: U b -> U b -> b

所以我们可以定义

_U :: (U b -> b) -> b
_U g = g (U g)                         -- g :: U b -> b 
-- = app (U g) (U g)
-- = join app (U g)
-- = (join app . U) g                -- (**)

现在有一个类型;并将其用作

_U (f x -> if x==0 then 1 else x * app f f (x-1)) 5
-- _U g  =>  f = U g, 
-- 120                                 -- app f f = g (U g) == _U g

---

编辑：如果你想将Y组合器实现为非递归定义，那么

_U (f x -> if x==0 then 1 else x * (app f f) (x-1))
=                                    -------.-               -- abstraction
_U (f -> (r x -> if x==0 then 1 else x * r (x-1)) (app f f))
=          -------.---------------------------------         -- abstraction
(g -> _U (f -> g (app f f))) (r x -> if x==0 then 1 else x * r (x-1))
=                                                            --  r = app f f 
_Yn                            (r x -> if x==0 then 1 else x * r (x-1))

所以

_Yn :: (b -> b) -> b
_Yn g = _U (f -> g (app f f))         -- Y, non-recursively

完成工作：

_Yn (r x -> if x==0 then 1 else x * r (x-1)) 5
-- 120

---

(后来更新：) 或者，点更自由，

_Yn g = _U (f -> g (app f f))
= _U (f -> g (join app f))
= _U (f -> (g . join app) f)
= _U (g . join app)
= _U ( (. join app) g )

因此

_Yn :: (b -> b) -> b
_Yn = _U . (. join app)                -- and, using (**)
= join app . U . (. join app)