[Grace-core] Statically-known and family-polymorphism

[Timothy Jones]

As part of trying to hash out a proposal for extended static reasoning, Michael
and I were trying to precisely define what is meant by 'statically-known'. The
point of statically-known is that we know exactly what the structure of an
object will be, which is particularly for sanity checking inheritance. We came
up with the following definition.

  Start with either:

  1) An object constructor that is not tail-returned by a method
  2) A dialect
  3) An import which can be resolved to an object definition

  Then you may chain together requests on these statically-known objects so long
  as the requested methods tail-return an object constructor.

(1) is important because we need to know the exact outcome of calling a
tail-returning method on an object. If an object constructor is itself
tail-returned, then we can't reason about any of the methods on it, because they
all might be overridden, and we don't have a guarantee that they necessarily
return an object with a compatible structure.

This seems to restrict the ability to do family-polymorphism, in that you can't
inherit from a method defined in the same 'trait', because the trait can be
inherited and the method overridden.

  class my.trait {
    method a {
      object { ... }
    }

    method b {
      object {
        inherits a
      }
    }
  }

This is rejected by the definition above, because the trait object could be
overridden by an implementor, possibly returning a completely different object
when the 'a' method is requested. The same is true for the following:

  class basic.trait {
    method basicImpl {
      object { ... }
    }
  }

  class better.trait {
    inherits basic.trait

    method betterImpl {
      object {
        inherits basicImpl
      }
    }
  }

The only place where it's safe to do this is when you hit a concrete class,
because at that point the method can be statically resolved.

  def best = object {
    inherits better.trait

    method bestImpl {
      object {
        inherits betterImpl
      }
    }
  }

It seems like we need to include a requirement that if you override a method
that tail-returned an object constructor, the new method must tail-return an
object constructor that inherits from the super method, thereby ensuring that
the structure of an object (and potentially statically-known methods inside) is
preserved by inheritance, and allowing (1) to generalise to any object
constructor. Do we have the syntax to achieve this, though?

  class yours.trait {
    inherits my.trait

    method a is override {
      object {
        inherits outer.super.a
        ...
      }
    }
  }

-- 
Tim