Handling "The resulting type would be infinite when unifying"

Question

let rec bind x f = f x |> bind bind "Hello World" (fun x -> x.toUpper()) printf "%s"

The code snippet above results in this error "The resulting type would be infinite when unifying".

The compiler's suggestion: "Lookup on object of indeterminate type based on information prior to this program point. A type annotation may be needed prior to this program point to constrain the type of the object. This may allow the lookup to be resolved."

As the compiler said adding a type annotation would resolve this problem. How would you write a type annotation which satisfies the compiler?

This might be helpful. Since Javascript is more forgiving and it doesn't complain, you can look at a working example of the same piece of code translated into JS.

const bind = x => f => bind(f(x))

bind("Hello World")
(x => x.toUpperCase())
(console.log)

Answer 1

The problem is that the bind function you are trying to define does not have a type that you can express in standard F#. You want a function that has a type looking something like this:

'A -> ('A -> 'B) -> ('B -> 'C) -> ('C -> 'D) -> ('D -> 'E) -> ....

In other word, the bind function should take input and a sequence of functions that it applies to them, but you're not restricting how long the sequence is. The standard F# type system does not have a way of expressing this and so people usually use other patterns. In your case, it would be the |> operator. In contrast to your bind, you have to write |> repeatedly, but that's typically fine:

"Hello World" 
|> (fun x -> x.ToUpper()) 
|> printf "%s"

That said, I think your example is not well chosen, and I'd just write:

printf "%s" ("Hello world".ToUpper())

Finally, it might be actually possible to define something like your bind function using overloading that's possible thanks to F# static member constraints. Something along those lines, but |> is an idiomatic and clean solution for doing the thing that your example illustrates.

Answer 2

Summary: you can't do this, but that function isn't useful in F#; just use the |> operator instead.

Longer version: there is no way to annotate the bind function that you've described in a way that will satisfy the F# compiler. When I paste let rec bind x f = f x |> bind into F# Interactive, it gives me the following error:

error FS0001: Type mismatch. Expecting a
    ''a -> 'b'    
but given a
    ''a -> ('a -> 'a) -> 'b'    
The types ''b' and '('a -> 'a) -> 'b' cannot be unified.

If we rearrange the definition a little to look like let rec bind x f = bind (f x) instead, we get a slightly simplified type error:

error FS0001: Type mismatch. Expecting a
    ''a'    
but given a
    ''b -> 'a'    
The types ''a' and ''b -> 'a' cannot be unified.

With a bit of type hinting (let bind (x : 'x) (f : 'f) = ...), we get the error that the types 'a and 'f -> 'a cannot be unified, so it becomes clear what's going on. 'a is the return type of bind (in the absence of any names for generic types, F# assigns them starting with 'a). Now let's look at why this type error is happening.

It looks like tou already know about partial application: any two-argument function, when given a single argument, returns a function that waits for its second argument before evaluating the function body. In other words, let f a b = ... in F# is equivalent to the Javascript const f = a => b => .... Here, the bind function, when given a single argument x, returns a function that waits for an f before evaluating the body of bind. That means that when bind is passed a single parameter, its return type is 'f -> 'a (where 'a is, as we said, the name that the F# compiler has arbitrarily assigned to the result of bind).

However, here's where the type conflict comes in: the value bind (f x), which has the value of 'f -> 'a as we've already said, is also the result of your bind function. That means that it should have the type 'a. So the F# compiler would need to compile that function in such a way that the type 'a is the same type as 'f -> 'a. If that were possible, then in type algebra 'a = 'f -> 'a, and you could then expand the 'a in the right-hand side of that equation to be 'f -> 'a, so that the equation becomes 'a = 'f -> ('f -> 'a). You could now expand the 'a again, getting 'a = 'f -> ('f -> ('f -> 'a)). And so on infinitely. The F# compiler does not allow infinitely-expanding types, so this is not allowed.

But as I already pointed out (and Tomas Petricek explained), you don't actually need this bind function in F#. All it is is a way to hook functions into a pipeline, where the output of one function will be passed into the input of the next one (as your Javascript example demonstrates). And in F#, the idiomatic way to do this is with the "pipeline" operator. Instead of bind "input value" f1 f2 f3 (where f1, f2 and f3 are three functions of appropriate type), in F# you'd simply write:

"input value"
|> f1
|> f2
|> f3

This is normal, idiomatic F# and will be understood by pretty much anyone, even those who aren't particularly familiar with functional programming. So there's no need for this bind function in F#.

Answer 3

That definition of bind is a functional paradox. It is self contradictory.

let rec bind a f = f a |> bind
//  val bind: (a:'a) -> (f:'a->'a) -> 'b

The best way to see it is by adding some type annotations, lets replace 'a with int to make it more concrete:

let rec bind (a:int) (f:int->int) = f a |> bind
//  val bind:(a:int) -> (f:int->int)-> 'a

bind receives a number and a function that takes the number and returns another, but what does bind return? The system does not know because it never really returns anything, it only goes deeper and deeper into another level of currying. That in itself is not a problem, F# can handle routines that never exit, for instance:

let rec loop() = printfn "Hello" ; loop()
//  val loop : unit -> 'a

In fact you can annotate loop with any type and F# would be OK with that:

let rec loop() : float = printfn "Hello" ; loop()
//  val loop : unit -> float

But if we do the same with bind the contradiction becomes apparent:

let rec bind (a:int) (f:int->int) : string = f a |> bind
//  val bind:(a:int) -> (f:int->int)-> string

The error message says:

Expecting a 'int -> string' but given a 'int -> (int -> int) -> string'

Why is it expecting int -> string? Because it is what the type says. We know f a returns an int and we pass it to bind and we should get a string, because that is the final result of the function. But bind does not return a string when only one parameter is passed, instead it returns a function of type (f:int->int)-> string, there in lies the contradiction. The left side (of the =) says bind returns a string when receiving 2 parameters but the right side says it returns a 'string' when receiving 1 parameter. It is a paradox, like the statement 'I always lie'.

If we go back to the initial definition without type annotations we can see that the inferred result type of bind is 'b which means any type, but it has to be one specific type not many types or a type that changes on every call. In particular 'b cannot be equal to ('a->'a) -> 'b because it involves 'b and thus is a circular definition (or maybe elliptical), hence the infinite loop.

For Javascript it is not a problem because it does not care about what types are passed to or returned from functions. That is they key feature that makes F# so much better to work with than Javascript.