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 foralls.

-- 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 foralls 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 foralls 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.