[Grace-core] Minutes of Teleconference 2013-07-24

Mon Jul 29 14:22:44 PDT 2013

I've been looking over the gradual typing papers and generally been worrying about how gradual typing will work with Grace.

1.  I ran into Gilad Bracha's paper on optional types in Dart at
	http://www.dartlang.org/articles/optional-types/
They are using the same defaults that we have just agreed to.  If a type parameter is omitted, say for List<T>, then it is treated as though there were an explicit type parameter of type Dynamic.  I.e. List means List<Dynamic>.  Obviously if you do something that explicitly depends on that type (reflection, match statements, etc.), then you will be using Dynamic there.

2.  Unfortunately the Siek and Waha paper on gradual typing on objects (in the repository as gradual-objSiek) misuses the Abadi-Cardelli notation for objects.  Where AC would write m = s(x:T) b for a method m with body b and x the name of self (what I wrote as "s" they write as a Greek symbol), Siek-Waha write m = U s(x:T) b for a method m with body b and parameter x with type T, returning a value of type U.

Aside from confusing me for a while, this also obscured the fact that in their type system in Figure 1 of that paper, they always type check an object by first computing the implicit type of self from its method declarations and then type check the method bodies using that type (see rule GObj).  This isn't surprising, as it is the standard way of type checking objects.  However, it means that their system does not include calculi where the type of self is implicitly dynamic, which is one of the options we discussed.

Unfortunately, I haven't run into any papers that discuss gradual typing and abstract classes/objects.  It seems that things should work pretty reasonably if we indicate what methods are missing and at least what their arity is (and possibly their types -- which they would be taken as dynamic if not annotated).  It's a bit less clear how to handle an incomplete class/object definition.  I suspect that the simplest way to deal with this would be to do no static type checking at all inside such an expression.  

If we tried to do some type checking, we would have to invent partial object types of the form {m:T,...,n:U,?) where ? means any compatible method types might be added (compatible means we don't break our rules on overloading).  That would allow us to pick up some type errors, but at the cost of adding a great deal of complexity to the type system.  People have looked at such systems (Mitchell among others), but they have not generally been adopted because of the complexity of often having to specify negative information as well as positive.

We should obviously continue this conversation.

Kim

On Jul 24, 2013, at 6:22 PM, Andrew P. Black <black at cs.pdx.edu> wrote:

> Minutes of Teleconference 2013-07-24, started at 15:00 PDT, ended around 16:30
> 
> Present:  Michael, Tim, Jameson, Kim, Andrew
> 
> Jameson demonstrated a number of Kim's objectDraw programs running in Javascript and doing html5 graphics.  He has achieved this by writing a Javascript version of the gtk libraries used by objectDraw.  Not everything works perfectly, but many examples do now run.
> Ongoing programming has revealed some bugs in minigrace, but on the whole the minigrace compiler is quiet serviceable.
> Visibility annotations don't seem to work in the Javascript backend.    Inherited variables annotated readable are not readable from a sub-object.
> Minigrace does not give errors or warnings when a variable is re-declared in an inner scope, contrary to what the Spec says in §6.
> Minigrace allows outer not just as a request target, but also as a request.   That is, it permits o.outer, which breaches confidentiality.  A sequence of outer.s should be allowed only as the left-most part of a request. 
> The meaning of outer is confusing.  Does it mean "the object enclosing self" or "the scope outside the current scope"?   If minigrace warned about re-declarations, then  "the object enclosing self", which is what is currently implemented, would be the right thing.  In this scenario, outer is the name of an object, and can be used only in a method request.
> We discussed once again the ambiguity of resolving method requests on implicit receivers that can be satisfies either on the super-chain or on the lexical chain.   Kim once again stated that if there is an ambiguity, then it must be resolved explicitly, by making the receiver explicit (either  self or outer, or outer.outer, or ...).  Once minigrace is issuing re-declaration warnings for lexical variables, we can see is this is practical.
> Tim discussed his their plan, which involves building a "model" for the runtime semantics of Grace and for gradual types, generic types, type inference, etc, all in a uniform setting.  By "model" he means an operational semantics.  Andrew said that making such a semantics executable would be a powerful tool, and suggested that Tim look at existing systems for executing operational semantics.
> We discussed Michael's problems with gradual typing, first aired in his email of 17 July.  The assumption is that we can get either static of dynamic behaviour without a global switch, and that all variables not explicitly given types will be typed Dynamic 
> The first problem is that Kim doesn't want self to be typed Dynamic by default, but instead wants the type of self to be inferred, so that he can get satic "missing method" errors.  Andrew wants the opposite.  These two views are representative of different communities, and we need to support them both.  Andrew suggested that annotating an object "is complete" (or, "is requiring(y, z), etc") would turn on type inference for the self representing that object.  A dialect could perhaps reverse this setting.
> It's currently legal to use generic type parameters in a computation.  For example
>         method go<E>(x : Iterable<E>) { print(E) } 
> What should this do when requested from a dynamic context in which the argument corresponding to E is omitted?   Tim said that for consistency, E should be Dynamic at runtime, even though the compiler might do some inference at compile time to produce better error messages.  Andrew thought that mixing annotations with runtime values was suspect; a program should remain meaningful when all annotations are removed.
> Blocks: we agreed that applications of blocks need to supply the same number of arguments as the block has parameters.  This is to enable the most helpful error messages.  In case of exceptional need, an "apply taking only as many arguments as you need" operation can be coded using reflection.  (This is what Smalltalk does.)  At this point, we did not see a need for having a common supertype for all blocks — instead there are separate supertypes Block0, Block1, Block2, … with zero, one, two, … arguments.
> The Spec is out of date with current decisions.  As a result, we forget what we have decided.  It's time to go through the Spec and update it, and open issues for discussion where necessary.  Kim suggested that Andrew allocate each of the three Graces with a part of the Spec to read, fix, and highlight problems found with annotations.  Accordingly:
> James should look at sections 1–7
> Andrew should look at sections  8–10
> Kim should look at sections 11–Appendix A
> These pieces are approximately equal numbers of pages.  Andrew made some minor changes recently (at home) that he forgot to commit.  He also just updated the spec so that it uses subversion's revision numbering and has pdf hyperlinks to the various sections.  Once we all have out annotations in place, we will need to schedule some discussion sessions.
> Next meeting: Tuesday 30th July at 15:00 PDT (Wednesday 31st July at 10:00 NZT).
> _______________________________________________
> Grace-core mailing list
> Grace-core at cecs.pdx.edu
> https://mailhost.cecs.pdx.edu/mailman/listinfo/grace-core

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mailhost.cecs.pdx.edu/pipermail/grace-core/attachments/20130729/40036afa/attachment.html>