3

我为 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")也失败并且类型检查器抱怨它不能构造一个无限类型（否定发生检查）。

对于其他组合器，我的统一结果与 Haskell 的一致。

我的统一算法可能是错误的还是fix只能在非严格环境中输入？

[编辑]

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

4

2 回答 2

5

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

诚然，朴素的 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
于 2018-01-25T16:20:51.480 回答
1

So as it turns out, you tried to implement U combinator, which is not a fixed-point combinator.

Whereas the fixed-point Y combinator _Y g = g (_Y g) enables us to write 

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

with _U g = g (g) we'd have to write

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

As you've discovered, this _U has no type in Haskell. On the one hand g is a function, g :: a -> b; on the other it receives itself as its first argument, so it demands a ~ a -> b for any types a and b.

Substituting a -> b for a in a -> b right away leads to infinite recursion (cf. "occurs check"), because (a -> b) -> b still has that a which needs to be replaced with a -> b; ad infinitum.

A solution could be to introduce a recursive type, turning a ~ a -> b into R = R -> b i.e.

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

so we can define 

 _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                -- (**)

which now has a type; and use it as 

 _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

edit: And if you want to implement the Y combinator as a non-recursive definition, then 

 _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))

so

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

does the job:

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

(later update:) Or, point-freer, 

 _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 )

Thus

 _Yn :: (b -> b) -> b
 _Yn = _U . (. join app)                -- and, using (**)
     = join app . U . (. join app)
于 2018-01-26T12:18:10.503 回答