I write a runtime type checker in and for Javascript and have trouble to type fix:
fix :: (a -> a) -> a
fix f = ...
fix (\rec n -> if n == 0 then 1 else n * rec (n-1)) 5 -- 120
The factorial function passed to fix has the simplified type (Int -> Int) -> Int -> Int.
When I try to reproduce the expression in Javascript, my type checker fails due to the invalid constraint Int ~ Int -> Int.
fix (const "hallo") also fails and the type checker complaints that it cannot construct an infinite type (negative occurs check).
With other combinators my unification results are consistent with Haskell's.
Is my unifiction algorithm probably wrong or can fix only be typed in non-strict environments?
[EDIT]
My implementation of fix in Javascript is const fix = f => f(f).
It's a bug in the type checker.
It is true though that the naive Haskell definition of fix does not terminate in Javascript:
> fix = (f) => f(fix(f))
> factf = (f) => (n) => (n === 0) ? 1 : n * f(n - 1)
> fact = fix(factf) // stack overflow
You'd have to use an eta-expanded definition in order to the prevent looping evaluation of 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