Looping Typechecker

[crusso]

This example cause the type-checker to diverge (observed while implementing a library for join patterns).

// NB: a non-regular type (accepted)
type foo<A> = { next: <B>() -> foo<(A,B)> };

// bad causes the type-checker to loop
func bad<A>():foo<A> {
  new {
     next<B>():foo<(A,B)> { next<B>(); }
  };
};

[crusso]

@andreas, I'll investigate but if you expect this to diverge, let me know why....

[matthewhammer]

I didn't expect this to be legal AS: To what function is the invocation next<B>(); referring?

[matthewhammer]

(Is it a recursive call to the next function being defined on that line?)

[nomeata]

(Is it a recursive call to the next function being defined on that line?)

Sure, why not?

[rossberg]

Yes, this is currently expected, because we don't check uniform type recursion yet.

Closing this as a duplicate of #76.

[rossberg]

(That is to say, the type definition in your program is gonna be illegal. Non-uniform structural type recursion is undecidable.)

[crusso]

Well, I'd actually love this to work for my join patterns example (i.e. it would be nice if this were legal)

It turns out I can fix the bug in this instance by make Type.rel_typ a little less eager in unfolding definition, but I don't know if it's correct (apart from passing all the tests):

| Con (con1, ts1), Con (con2, ts2) ->
   (con1 = con2 && rel_list eq_typ env rel eq ts1 ts2) || (* crusso: check me first, before unfolding *)
   (match Con.Env.find con1 env, Con.Env.find con2 env with
   | Def (tbs, t), _ -> (* TBR this may fail to terminate *)
     rel_typ env rel eq (open_ ts1 t) t2
   | _, Def (tbs, t) -> (* TBR this may fail to terminate *)
     rel_typ env rel eq t1 (open_ ts2 t)
(*
   | _ when con1 = con2 ->
     rel_list eq_typ env rel eq ts1 ts2
*)
   | Abs (tbs, t), _ when rel != eq ->
     rel_typ env rel eq (open_ ts1 t) t2
   | _ ->
     false
   )

[rossberg]

Well, a hack like that would break basic properties of the relation (like transitivity). So that doesn't seem viable.

[crusso]

But isn't this just checking reflexivity? Indeed, I'm just doing the third (original, now commented) check early (before doing the unfoldings) although I guess I should also check con1 (con2) are in the environment.

[crusso]

Or am I missing something about the way the relations are (statefully) grown?

[rossberg]

A type name is supposed to be equivalent to its definition. Consequently, when you have X = T, then X <: X must imply T[U/A] <: T[V/A], otherwise transitivity would not hold. When you can only derive the former but not the latter then it's toast.

That change also doesn't answer the question how to prevent non-termination in the other cases. The standard solution is banning irregular types altogether. It would be awesome if we could find something more permissive, but my attempt of a literature search came up empty.

[rossberg]

[Redoing it with parens, since GitHub eats the angle brackets.]

A type name is supposed to be equivalent to its definition. Consequently, when you have X(A) = T, then X(U) <: X(V) must imply T[U/A] <: T[V/A], otherwise transitivity would not hold. When you can only derive the former but not the latter then it's toast.

[crusso]

Ok, that make sense, but here, I'm only concluding X(U) =/<: X(V) when U=V, in which case, shouldn't T[U/A]=/<:T[V/A] hold ?

[rossberg]

It's probably still breaking other properties, like covariance. If A only appears positively, like in foo, and U <: V, then foo(U) <: foo(V) should hold.

But even if you forget about subtyping entirely, you already get into trouble. Consider this example:

type T<A> = {x : <B> () -> U<(A, B)>};
type U<A> = {x : <B> () -> T<(A, B)>};

Clearly, T and U have identical structure, but how would you successfully check T<Nat> = U<Nat>?

[crusso]

I think in either case the algorithm would be behave as previously, since the modification still does the unfolding if necessary (supporting co-variance in the first case) and diverging (as before) in the second.

Or is there something else wrong?

[rossberg]

Sure, but how do you envision ruling out non-termination while making these cases work? Because if they were rejected although your case is allowed, you'd have an inconsistent type system.

[crusso]

For the case above, I imagine we could actually add a set of equated type constructors and add to the set before unfolding both sides. But I expect this still won't guarantee termination when they are only equal after n-unfoldings, for some n.

[nomeata]

Now at https://dfinity.atlassian.net/browse/AST-19