[Grace-core] On Gradual Typing

[James Noble]

Hi Michael 

a few replies - I'm actually about to go offline for a few days,
both this & next weekend... 

> So far, the conception of how gradual typing works in Grace
> ...
> I've mentioned before that I don't think all of this actually fits
> together, but interest has been low.

It's good to have this email then! 

> Let us consider the following completely statically-typed program:
> 1    object {
> 2        method x -> Done {
> 3            self.y
> 4        }
> 5    }
> Line 3 is clearly a static type error because there is no such method
> "y" on self.

sure. 

> Now let us consider the following completely dynamically-typed program:
> 1    object {
> 2        method x {
> 3            self.y
> 4        }
> 5    }
> Line 3 is clearly a static type error because there is no such method
> "y" on self.

It's not "clearly" a static type error. It's not an error in most dynamically
typed languages.   We may want to treat it as such, but that's a different
question.   

It's not an error if we can show x is never requested on this object,
or if only requested from another inheriting / delegating object
that itself implements y. 

> We have a problem here.

Well yes - but Andrew's Nixon/Bush/Atlee distinction 
(sorry I've forgotten precisely who) did address this directly.
Even in the case of statically typed code, it could be pedagogically
useful to allow student to run to code to see the error for themselves
in the context of an actual execution.

> A key goal has been that control structures are actually methods
> inside. Let's look at a plausible definition of the for-do method:

yep.

> In order to be able to write dynamically-typed code, omitted generic
> parameters must be populated with "Dynamic" (at runtime - we don't
> necessarily know statically what the type of the method is, so this,
> rather than static inference, must be the semantics of the language).

not necessarily. It's one choice, there are others. 

> In statically-typed code, though, what does that mean? If I write
> 1    for (someList) do { v : X -> print(v) }
> then that must (because we have gradual typing) mean the same thing as
> the dynamically-typed case, regardless of whether we know the type of
> the method.

for suitable definitions of "mean the same things as".

> That rules out inference of the parameter.

Not necessarily. Dart, C# and Scala (and Racket I guess) all have some
form of Gradual typing or type Dynamic and Generics and Type inference. 

> So in your
> statically-typed code, this loop is actually
> 1    def someList : List<Number> = generateNumberList(5)
> 2    for<Number> (someList) do { v : Number -> print(v) }

I take it you mean - "all types in the loop must be written out explicitly" - ?

> This seems unwieldy,

indeed!

> but perhaps it is acceptable to the people who are concerned with that.

probably only a few...

> Internal iterators do not have this problem, although the general issue still stands.

I'm not sure about that - because of blocks, as you say next:

> There seems to be no common "Block" type
> possible. Instead, there needs to be many "Block0", "Block1" types
> defined, or possibly variadic generics.

probably variadic generics - I think the Racket guys again have a paper,
and C# & Scala have them in practice - are the right ways to go.... 

> In either case, these will all  be totally different types.

given we already have variadic methods,  surely they could all be 
related to some type like:

type Block = { 
  apply(args : *Dynamic) -> Dynamic 
} 

now that's not a terribly useful type, but it is a type,
and you'd get a certain amount of checking with it.

> Firstly, is this type-correct? It seems that it cannot be, when there
> is no overarching Block type.

there is a question whether blocks can ignore some or all of their arguments.
the real problem is with the no-overriding rule.

Self gets away with this by setting things up so that blocks basically ignore extra arguments.

> Secondly - ignoring types - is it even
> semantically valid at runtime? Can I provide a block with excess
> arguments? People have been habitually writing code with both forms
> (it was even put in the specification), but it doesn't seem like they
> can both be well-typed.

well you can in Self, Smalltalk, and Newspeak, at least. 
their only use of keyword syntax gets around overloading.
The big thing you may be pointing out here is that variadic generics
(in particular) might let overloading back in the back door.
Or not.   The "generalized message" idea might get around this
(but at a potentially awful cost).

> Type inference of the return type of the block seems to have many of
> the same conceptual issues as other inference, but I don't think it
> affects runtime behaviour that isn't either already doing type
> matching or a gradual check.

I'd hope so - so that means it's not so bad. 

> There doesn't seem to be any way tospecify the type explicitly.
 
we could add syntax to specify both block argument & return types.

{  <X> x : X -> : X;  x  }   // horrible but possible?

> Tim has been talking about implementing the
> typechecker as a dialect for research purposes; I think that this is
> in fact the only way forward, in which the typechecker is an
> additional layer that may be bolted on for programs desiring static
> typing.

yes, I think that's mostly how things need to go. 
It may have to be a bit special, compared to other dialects, though.
The nice thing about this is it means we could have multiple different type checkers)
(pause for realising how horrible that would be in practice :-)

> Secondly, that given all of this, anywhere that type inference is required is a significant problem.

this is why the type checker would need to be special (at least),
or, rather, although it may be implemented as a (special) dialect,
the type checker would have a distinguished status in the system

>  Variants of the rule where inference only
> occurs for statically-typed code cause spooky action at a distance,
> where a new type annotation in one part of the program causes a
> behavioural change somewhere far away, and so aren't satisfactory either.

I'd say aren't *ideal* rather than aren't satisfactory. 
We don't have enough experience to know what's satisfactory -
but we do know of some designs - Dart, C#, Scala - that have
managed to combine features in similarly to the way we're hoping to in Grace.

> any inference that is utterly essential must be very narrowly circumscribed.

I'd buy this: or at least - must be capable of being explained by one of our 
average 2nd year students. Which may mean the same thing! 

> Thirdly, that the run-time checks implied by gradual typing end up in
> an interesting place in this world. They presumably end up
> implementing a specific view of the types, but how that conforms to
> the view taken by the static checker is unclear.

if semantics are actually defined by the _dynamic_ types 
then the static typechecker should be sound wrt the dynamic types.
You're right, though, the trick is how to do type inference. 

it may be possible to think about dynamic semantics for type inference
so that e.g.  method foo<T>( a : T) -> T { ... }
the type of T is picked up from the *dynamic* type of the argument
but that makes my head hurt.

> There seems to be a mode where there are no static checks, but fully-typed code will be
> checked dynamically at every step.

yes - and that may be possible even if the code fails the type checker. 

> No type inference is possible here.

again, not so sure about that. 
It's possible we have to consider two or more things 
- in the same way minigrace currently has an "identifier resolution phase"
between parsing & typechecking:

we could have a "type resolution / inference" phase which looks at 
static declarations and somehow fills in types automatically
(perhaps annotating 'em to say they were inferred)

then the actual type *checker* is a dialect that runs over those annotations
and raises the errors (or warnings) but the code is runable without that. 

> Finally, that exactly how blocks work needs some urgent consideration.
> They are pervasive but underspecified.

mostly yes.

overall, this is a good discussion to have, 
particularly good to hear Tim is thinking about working on the type checker 

we should think more on such things.

James