# Understanding weird infinite type loop { b | fn : ∞ -> a }

(0) This post shares a learning experience. It’s a bit long because I use examples and small steps to help provide clarity.

I do this to offer help to others who encounter the same problem. I hope it might result in improved documentation. I welcome any comments that shine further light on this, particularly the new puzzle in (6) below.

An aside. The background is this. There’s something I want to do in Elm, that I think should be possible. But I kept on running into a weird error. And I kept persisting. In the end I understood much better where the problem comes from.

(1) The following comes from an `elm repl` session, with `repl` output as comments.

``````obj = { int = 1, fn = identity }
-- { fn = <function>, int = 1 } : { fn : a -> a, int : number }

fn = obj.fn
-- <function> : a -> a

y = fn obj
-- { fn = <function>, int = 1 } : { fn : a -> a, int : number }

puzzle arg = arg.fn arg
-- INFINITE TYPE
``````

(2) What puzzled me was that the computation of `y` worked fine, but when I refactored it into `puzzle` I got an `INFINITE TYPE` error.

(3) Here’s the help I got from the Elm compiler, rewritten to improve clarity.

I am inferring a weird self-referential type for `arg`. Here is my best effort at writing down the type of `arg`:

``````{ b | fn : ∞ -> a }
``````

I use ∞ for parts of the type of `arg` that are part of an infinite loop.

(3) Step 1 of how I understand the puzzle.

1. The `identity` function satisfies a type constraint. The types of `arg` and `identity arg` are the same.

2. When I did `y = fn obj` the Elm compiler wasn’t aware of this type constraint, or it didn’t matter.

3. When I did `puzzle arg = arg.fn arg` it was aware of this constraint.

(4) Step 2. In

``````puzzle arg = arg.fn arg
``````

the compiler checks that `arg` and `arg.fn arg` have the same type. Let’s see what happens.

1. From `arg.fn` the compiler deduces that arg is a record. This is important.

2. Therefore the value `arg.fn arg` must also be a record, and of the same type.

3. Here’s an example of something that changes the type of a record.

``````{ obj | int = "1" }
-- You can't update `int` to be a `String`, as `int` must be a `number`.
``````
1. For a reason I don’t understand, Elm can’t know or doesn’t trust the type property
``````obj.fn
-- <function> : a -> a
``````

and so insists on checking it.

1. This leads to the infinite loop `{ b | fn : ∞ -> a }`.

2. A new puzzle. I’m allowed to do

``````{ obj | fn = identity }
-- { fn = <function>, int = 1 }
``````

Why does (6) succeed when (4) fails?

1 Like

I believe you confused yourself a bit:

``````puzzle arg = arg.fn arg
``````

has nothing to do with `obj`. So the compiler does not know that `arg.fn` should be the identity. All it knows is that is should be a function of type `?1 -> ?2`.
I denote `?1` for a type that the compiler has yet to figure out.
Note that it does NOT know that `?1 = ?2`, because `?1` could be a more general type than `?2`. (For example `?1` could of type `a` and `?2` of type `{record | fn : a}`. At this point the compiler does not know.

Now from there it can deduce that `arg` is of type `{ record | fn : ?1 -> ?2 }`.

Next it sees that the first argument of `arg.fn` is `arg` therefore `?1 = { record | fn : ?1 -> ?2 }`. But that’s a self-refering type:

``````?1 = { record | fn : ?1 -> ?2 }
= { record | fn : { record | fn : ?1 -> ?2 } -> ?2 }
= { record | fn : { record | fn : { record | fn : { record | fn : ?1 -> ?2 } -> ?2 } -> ?2 } -> ?2 }
= ...
``````

You can fix this by telling the compiler that `arg.fn` does not change the type:

``````puzzle : {record | fn : a -> a} -> b
puzzle arg = arg.fn arg
``````

Edit:
This fix does NOT work!

4 Likes

(0) Thank you @Lucas_Payr. You’ve made a very good point, that `obj` is not part of the definition of `puzzle`. Perhaps you’re right, that a type annotation can fix the problem. But I’m sorry not the one you provided.

(7) Here’s what I got.

``````puzzle : {record | fn : a -> a} -> b
puzzle arg = arg.fn arg

-- TYPE MISMATCH
-- The 1st argument to this function is not what I expect:
--     puzzle arg = arg.fn arg
-- This `arg` value has type
--     { record | fn : a -> a }
--  But this function needs the 1st argument have type `a`.
``````

(8) Of course adding type annotation can produce a type error. That’s the whole point. But I’m not aware of any examples where removing a type annotation removes a type error.

I half suspect that trying to fix your annotation will send you into the infinite type loop. I hope I’m wrong, as I really want this feature.

Yeah, you are right. It does not solve the problem. Interesting. In that case I’ll just clame: There is no way to fix this.

I would assume that one could get a similar result for

``````puzzle fn = fn fn
``````

I believe the underlying problem is that we usually think of `a->a` as “for any type, return the same type”. Whereas the compiler will read it as “for SOME type, return the same type”. This means it tries to find this SOME type. But the only valid type for this is a self-referencing one - and that’s not allowed.

This evidently should go back to Russell’s paradox and the invention of type theory. But I do not feel I’m capable enough to go down this rabbit hole

# Is this a Elm related problem?

No. That’s more a “Type Theory” problem, so any programming language will fail at solving this.

# How can this be avoided?

This problem should go away if you ensure that functions that can call them self do not live in the model (= a record).

Going back to your original problem:

``````fn = identity

puzzle arg = fn arg
``````
1 Like

The most succinct way of describing the problem is that you are asking for a higher-rank type whereas Elm only supports rank-1 types.

Let’s unpack that terminology a bit by looking at another example that isolates the problem.

``````myPair : (Int, String)
myPair = (identity 0, identity "")
``````

We reuse `identity` for two different inputs of different types. Easy peasy. `identity` is polymorphic after all.

Let’s say we want to do a common refactor and pull out `identity` as a parameter to `myPair` instead.

``````myPairF f = (f 0, f "")
``````

Uh oh, Elm has an error.

``````The 1st argument to `f` is not what I expect:

1| myPairF f = (f 0, f "")
^^
This argument is a string of type:

String

But `f` needs the 1st argument to be:

number

Hint: Try using String.toInt to convert it to an integer?
``````

But what if we really try to tell Elm that `f` is meant to be polymorphic just like `identity` by adding a type annotation?

``````myPairF : (a -> a) -> (Int, String)
myPairF f = (f 0, f "")
``````

Still no luck.

``````The 1st argument to `f` is not what I expect:

2| myPairF f = (f 0, f "")
^
This argument is a number of type:

number

But `f` needs the 1st argument to be:

a
``````

What’s going on? Elm elides a certain feature of our type annotations that is often called `forall`.

``````-- The "real" type of identity, note forall isn't valid Elm syntax
identity : forall a. a -> a
``````

When you call `identity 0`, the `Int` associated with the `0` is substituted for the variable that appears in the left-most `forall`.

Importantly, because our `forall` is on the “outside,” how `a` gets substituted is determined by the caller of `identity`. E.g. `identity 0` turns `a` into an `Int` because `0` is an `Int`, `identity ""` turns a into a `String` because `""` is a `String`, etc.

So in `myPair` everything is fine, `identity` has its `a` substituted twice in different ways (by an `Int` and `String` respectively) and we’re fine.

What about `myPairF`?

``````-- Again the "real" type signature of myPairF
myPairF : forall a. (a -> a) -> (Int, String)
``````

Again, because `forall` is on the left-most side of this type signature, the caller gets to decide how `a` is substituted.

So whoever calls `myPairF` gets to arbitrarily set `a` to `Int`, `String`, `Float`, or whatever!

This means the following type signatures are all valid specializations of `myPairF`:

``````myPairF : (String -> String) -> (Int, String)
myPairF : (Int -> Int) -> (Int, String)
-- etc.
``````

So for example `myPairF String.toUpper` turns `a` into a `String`. That’s bad! `myPairF String.toUpper` which makes `f = String.toUpper` is impossible to square with `f 0`. This is why when Elm’s typechecker goes to typecheck the definition of `myPairF`, within `myPairF` `a` is an opaque type that is incompatible with `Int` and `String`.

So what you need is some way to tell Elm to “delay” the resolution of `a`.

``````-- Hypothetical Elm syntax
myPairF0 : (forall a. a -> a) -> (Int, String)
myPairF0 f = (f 0, f "")
``````

Notice now that `forall a` has been “moved in” one level; it is no longer on the left-most side. In particular that means arguments to `myPairF0` cannot cause concrete type substitutions for `a`. In other words, your caller isn’t allowed now to willy-nilly say “I want `a` to be an `Int`.” You can only decide to set `a` to a concrete value after “unwrapping” it once (in this case by using it in the body of `myPairF0`.

In particular `myPairF0 String.toUpper` is a type error because `String -> String` is not the same type as `forall a. a -> a`. However, `myPairF0 identity` works just fine, and yields the original `myPair` result.

Now `myPairF0` is an example of a type signature with a rank-2 type, where a rank-n type is how “deep” a `forall` is in the type signature (in this case it is one additional level deep because it’s inside a set of parentheses, rather than at the outermost layer of the type signature). Elm only supports rank-1 types. That means that `forall` must always appear on the left-most side of the type signature and cannot be inside any parentheses. That also means that you cannot write the `myPairF0` function in Elm!

Okay now that we’ve isolated the particular problem, how does this apply to your original puzzle? Let’s write out everything with explicit `forall`s.

``````-- Notice that forall is on the left-most side!
obj : forall a. { int : Int, fn : a -> a }
obj = { int = 0, fn = identity }

-- This is not the "same" fn as obj.fn
-- You're effectively "re-specializing" obj.fn
-- Read on for what I mean
fn : forall a. a -> a
fn = obj.fn

-- For example this is perfectly valid as well
fn0 : Int -> Int
fn0 = obj.fn

-- Just to drive the point home, notice that this is valid!
-- (which is probably not what you want)
-- Elm is allowing an "in-place" update of `identity` to `\x -> x + 1`!
thisIsValid : { int : Int, fn : Int -> Int }
thisIsValid = { obj | fn = (\x -> x + 1) }

y : forall a. { int : Int, fn : a -> a }
y = fn obj

puzzle : forall a. { int : Int, fn : a -> a } -> ???
puzzle arg = arg.fn arg
-- Notice that because forall is on the left-most side
-- puzzle thisIsValid
-- must be a valid Elm value. But what could it be?
-- `fn` in `thisIsValid` is `Int -> Int` after all.
``````

Notice that because `forall` is on the left-most side of `puzzle`, it must decided once upfront by the caller, so something like `puzzle thisIsValid` could completely spoil `puzzle`!

What you really want is for the `forall` to be nested inside your record.

``````fixedObj : { int : Int, fn : forall a. a -> a }
fixedObj = { int = 1, fn = identity }

puzzle : { int : Int, fn : forall a. a -> a } -> { int : Int, fn : forall a. a -> a }
puzzle arg = arg.fn arg
-- We're fine here because `arg.fn` exposes its `forall a` _inside__ puzzle.
-- This allows `arg`'s type signature to be substituted for `a`
-- Notice that thisIsValid wouldn't work here:
-- (\x -> x + 1) does not have the type signature forall a. a -> a

puzzle fixedObj -- Works great!
puzzle thisIsValid -- Type error
``````

But you can’t write this in Elm and it is unlikely Elm would ever get the ability to move `forall`s in and out of parentheses. This is because this affects type inference. Notice that `obj` and `fixedObj` have identical definitions, but have incompatible type signatures (unlike `Int -> Int` and `a -> a` one cannot be substituted for the other). This would mean that certain expressions in Elm would require* type annotations (whereas right now type annotations are always optional).

* I’m telling a small fib here. It turns out you can preserve global type inference for rank-2 types, but not for any even higher-rank types, e.g. if you had even further levels of nesting of `forall`. However, the rank-2 type inference algorithm is significantly more complicated than Elm’s current type inference algorithm.

EDIT: I made a small error in one of my code samples (see the edit history of this post for details)

EDIT 2: Also just for accuracy’s sake, what I’ve actually illustrated in the revised type signature of `puzzle` is something known as impredicative types, but the difference is subtle and somewhat moot for Elm because Elm’s not getting either one unless something drastically changes in its philosophy.

The pure rank-2 type would be

``````puzzle : forall b. (forall a . { int : Int, fn : a -> a }) -> { int : Int, fn : b -> b }
``````

but it’s a bit overwhelming to parse the repeated nested `forall`s and I’d need to explain why `forall b` is allowed to appear at the beginning of the type signature rather than also being nested with the output (I can if people are interested, but it’d make this reply even longer). So I cheated a little by using impredicative types. However, the fundamental idea is the same: judicious application of `forall` gets you what you want, but Elm is not capable of expressing it.

9 Likes

(0) I thank @Lucas_Payr and @yosteden very much for their contributions. Together they’ve given me the encouragement I needed to go deeper into this problem. I’ve now proof-of-concept implemented the feature I wanted.

(9) Here’s an example of the feature I wanted.

``````aaa = update int_object 100
bbb = update aaa 1
ccc = update str_object " is"
ddd = update ccc " prime."
``````

(10) The underlying idea is that each object should be a record with a `state` field and a `methods` field. Motivation comes for classes and methods in Python and other languages. And also the data fork and resources fork in Apple’s macOS.

(11) The problem I asked for help with was the weird infinite type error that comes from

``````bad_update obj msg = obj.update obj msg
``````

and my improved understanding of this type error allowed me to avoid it.

(12) The key idea in the solution is to write

``````update obj msg =
let
x_update = obj.methods.update
-- State in and Delta out to avoid type error.
state_delta =  x_update obj.state msg
new_state = state_delta obj.state
in
{ obj | state = new_state }
``````

(13) There’s an implementation at https://ellie-app.com/cFWnpF7kLW6a1. Unusually I think for Ellie, that the code compiles successfully is the main point. I now look forward to exploring whether this solution might help when writing apps. In any case, I’m now less frightened of weird type errors.

This topic was automatically closed 10 days after the last reply. New replies are no longer allowed.