Logo Questions Linux Laravel Mysql Ubuntu Git Menu
 

Compiler error about class graph being not finitary due to a expansively recursive type parameter

With this piece of code:

trait B[T]
trait C[T]
class A[T] extends B[A[C[T]]]

I get the following error:

error: class graph is not finitary because type parameter T is expansively recursive
       class A[T] extends B[A[C[T]]]
               ^

Can someone explain what the error message is about, why T is infinitely recursive and why the following code works?

class A[T] extends B[A[T]]
like image 201
soc Avatar asked Sep 24 '11 17:09

soc


1 Answers

From the Scala 2.9 specification (note that this is in the Change Log as a change that was introduced in 2.4, so it's not a "new restriction" in 2.9):

The implementation of subtyping has been changed to prevent infinite recursions. Termination of subtyping is now ensured by a new restriction of class graphs to be finitary.

Kennedy and Pierce explain why infinitary class graphs are a problem:

Even disregarding subtyping, infinite closure presents a problem for language implementers, as they must take care not to create type representations for supertypes in an eager fashion, else non- termination is the result. For example, the .NET Common Language Runtime supports generic instantiation and generic inheritance in its intermediate language targeted by C. The class loader maintains a hash table of types currently loaded, and when loading a new type it will attempt to load its supertypes, add these to the table, and in turn load the type arguments involved in the supertype.

Fortunately, as Kennedy and Pierce point out, there's a convenient way to check whether a class graph is infinitary. I'm using their definitions throughout this answer.

First I'll make your type variables distinct for clarity:

trait B[X]
trait C[Y]
class A[Z] extends B[A[C[Z]]]

Next we construct the type parameter dependency graph using Kennedy and Pierce's definition. The only declaration that's going to add edges to the graph is the last one, for A. They give the following rules for building the graph:

For each declaration C <X̄> <:: T and each subterm D<T̄> of T, if T_j = X_i add a non-expansive edge C#i → D#j; if X_i is a proper subterm of T_j add an expansive edgeC#i → D#j

So first we look at Z and C[Z], which gives us a non-expansive edge from Z to Y. Next Z and A[C[Z]] gives us an expansive edge from Z to Z, and Z and B[A[C[Z]]] gives us an expansive edge from Z to X:

Graph for the bad version

I've indicated non-expansive edges with dashed arrows and expansive edges with solid ones. We have a cycle with an expansive edge, which is a problem:

Infinitary class tables are characterized precisely by those graphs that contain a cycle with at least one expansive edge.

This doesn't happen for class A[Z] extends B[A[Z]], which has the following graph:

Graph for the good version

See the paper for a proof that a class table is infinitary iff it's expansive.


like image 54
Travis Brown Avatar answered Oct 16 '22 07:10

Travis Brown