[Grace-core] Gradual typing with Dynamic return type

[Michael Homer]

This was originally to be a response to the other thread, but I found
a broader issue in the process: does return type Dynamic conform to a
static return type? It looks like there's a problem with either way
around (worked through below).
On Sun, Sep 25, 2011 at 9:46 AM, John Tang Boyland
<boyland at pabst.cs.uwm.edu> wrote:
> ] Hi John
> ]
> ] > I'll try to come up with an example.
> (3) TESTING Structural Types at run-time
>
> Structural types are NOT easy to compare.
> Consider:
>
> class A {
>    methods foo -> B { ... }
> }
>
> class B {
>    method foo -> A { ... }
> }
>
> class C {
>    method foo -> C { ... }
> }
>
> The types A, B and C are all structurally the same.
>
> Determining this without getting stuck in infinite loops
> requires complicated caching etc.  (And I hope you realize
> that it's easy to multiply ever worse examples, where A
> has a method "bar" as well that takes a B and returns a C,
> and B and C have similar methods! etc.)
>
> This is bad enough to happen statically at compile time,
> but is MUCH worse to happen at runtime.  You can imagine
> a large binary search tree where ONE of the leaves
> does NOT have the required contract to make it legal
> as a binary search tree leaf, and thus the entire tree is
> not a binary search tree.  So one small piece of state
> deeply inside of some structure can change the type of the
> whole thing, and there may be cyclic pointers all over the
> place that we must traverse carefully with caching to avoid
> getting into cycles.
Running the structural typing algorithm at runtime is definitely an
issue (and I think unavoidable because of generics), but it isn't
quite as bad as this. Types only describe the methods on an object, so
a piece of state anywhere can't affect the type. In the binary search
tree case, if we assume:
  type BST = {
    left -> BST | None
    right -> BST | None
    value -> String
  }
then this should be type-valid, even with the gradual check at runtime:
  var b := object {
    var value := "A"
    var left := None
    var right := object {
      var value := 1
    }
  }
  var bst : BST := b
b itself has type Dynamic, and all its methods have return type
Dynamic as well. Checking whether b is assignable to type BST just
involves checking whether all the methods of BST are present with
conforming signatures, and "right -> Dynamic" does conform to "right
-> BST". There will be a further runtime check when bst.right is
invoked, and this should fail:
  var bst' : BST | None := bst.right
For the types to work over the actual dynamic state of the object
would require invoking the methods and testing the return value, which
can't work because they could be real methods with side effects. That
does mean that statically-typed code has no real type-safety
guarantees at runtime if it's mixed with Dynamic. Code like
"bst.right.left" looks like it should be safe (ignoring the | None for
the moment), but can fail dynamically with a no-such-method error.

Having been through all that I think I've talked myself into thinking
that Dynamic must not be a conforming return type for anything but
itself. There's no way for the code from above to raise an error
unless every assignment or invocation is accompanied by a runtime
check. This:
  var bst : BST
  ...
  var bst' : BST | None := bst.right
should be able to rely on static type information for correctness, but
it can't if there's any possibility that the value of bst may contain
a method returning Dynamic. There could be correctness problems too,
and pattern matches can't be guaranteed exhaustive. Banning that seems
to make the Dynamic type fairly useless, though, and especially
hinders gradually adding return types to code. There doesn't seem to
be any way to check whether an object like that actually conforms to
all of the type or not, other than running the code.

There is a trade-off to be made there: either Dynamic is a conforming
return type, turning statically-typed code into potentially-dynamic
code, or it isn't, and you can't add return type annotations to the
type without adding them to all the otherwise-dynamic objects you want
to use with those as well.
-Michael