[Grace-core] [A Graceful Blog] Comment: "From Lancaster to Portland"

[John Tang Boyland]

] Hi John
] 
] > I'll try to come up with an example.
] 
] that would be great -   
] (I'm cc:ing grace-core as the others will be interested too - hope you don't mind)
] 
] > It would help if you'd tell me whether the type that every object carries with it
] > is a nominal type or a structural type.
] 
] let's say structural for now
]  - although with "branding" most objects will at least carry *both* 

Thanks. The branding Andrew Black mentions fits into this
model just fine.  (BTW: Number types will HAVE to be branded,
because otherwise, they will be unimplementable.)

Just to remind people: My main worry is about pattern matching
with gradual typing.  But some of my worries occur even without
gradual typing.

OK, here with syntactic errors are a few examples.

(1) UNION TYPES

In James' example on the blog, he defines some types:

	class Some[T] { v : T ->
	  method extract -> [T] {[T]}
	}

	def None = object { } 

	type Option[T] = Some[T] | None

(Personally, I don't understand the syntax of the extract
method.  I would expect:
	method extract -> T { v }
but I assume we can all muddle our way through syntax.)

The first thing that comes to me is that, since James assures me
that there is no tagging of union types, other than the
fact that ALL objects are tagged, that the type Option[T]
is essentially equal to None: The None type permits any object
(it is the empty structural object type).  Thus anything can be
passed to something of type Option[T].

This is what I originally asked of the blog and Kim Bruce assured
me that these union types were NOT set-style union types.
(And thus Option[T] was NOT identical to None.)  But that
led me to assume that there is some "inleft" "inright" explicit
coercion needed to create something of a (tagged) union type
a la ML.  But James says that's not necessary because everything
knows its type.

I hear a contradiction here.  If I have something of type Number,
then can it be passed to something wanting Option[T] ?
Some might say that the static type system of Grace will require
me to put in an explicit cast.  But if that cast has no run-time
significance (i.e. no tagging), then the gradually typed Grace
will have set-style union types: the kind that generally
are thought to be a Bad Idea.  

And why would a cast be necessary?
What indeed is the subtyping rule for Union types?
If I recall correctly, Igarashi's design lets A | B be a supertype of A.
Hence Option[T] > None > Number, and we have the Bad Idea in typed Grace
too.


(2) ORDER MATTERS

Since None includes all object types, it makes a difference
if we have:

	x match {
	   case x: Option[T} => ...
	   case y: None => ...
        }

or have the reverse.  When dealing with option types,
people often may want to put the None case first to get
it out of the way.  Here that would cause the None branch
to be chosen always, since None is the same as "object {}".

At the very least, we would want a compiler that checked that
a later case wasn't rendered redundant.


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

A set-style union type "match" is doing type-checks
at runtime: is this object of this (structural) type?
If so, do this.  The checks will be VERY expensive.
And that's even when all the types are declared.

With gradual typing, it gets MUCH worse.  Methods may use
conditions to decide what to return, and so the type of
an object is actually undecidable at runtime.

In the "Blame" papers, Felleisen and others show how when
going between untyped and typed worlds, you want to avoid
solving unsolvable problems when traversing the type barrier
and instead permit a cast provisionally but leave information 
around that permits a cast error to be pinned (blamed)
to the right place.

This only works if a cast error is fatal.  But if a cast error
means "OK, not this branch, try the next one", then a cast
error found late will be impossible to recover from: we chose the
WRONG branch and have done who-knows-what side-effecting damage
since the wrong decision.

(3) EXAMPLE: Draw

Supposed we have:
    class Shape {
      method draw(c : Canvas) -> Unit { ... }
    }

and we have code that has:
   type MaybeDrawable = Shape | None

and code that does:
  c : Canvas ->
  show(x : MaybeDrawable) -> Unit {
    x match {
      s:Shape => s.draw(c)
      _:None => println("Something")
    }
  }

If we now have some untyped code that declares:
    class Cowboy {
      method draw(g) -> { g.shoot(3) }
    }

and pass a "cowboy" as a MaybeDrawable to "show", then should it
be considered a Shape or not?  If g were typed as "g : Gun"
then no, but how can the runtime system know that g is a gun?
The body of Cowboy#draw might embed the use of g deep in
lambdas where it cannot be found (concealed carry?) and 
defeat any tractable attempt to determine the actual type of g.

In conclusion: pattern matching should be on types
with a implicit tagging BEYOND that provided by the objects
themselves.

And then Some[T] | None is different from None | Some[T],
because we will have explicit inl/inr objects and need to
know which one we have.

But once we have inl/inr, shouldn't we permit in(Nat)
and then name the positions (rather than use numbering)
and end up with something like:
	SOME of T | NONE
:-)

Best regards,
John