[Grace-core] Type Parameters and parametric type

[Michael Homer]

On Wed, Oct 23, 2013 at 11:48 AM, James Noble <kjx at ecs.vuw.ac.nz> wrote:
> Hi Lex
>
> a few quick thoughts - not intending to dismiss the things to which I haven't responded...
>
>> 5. If-then-else is easy if you take the right perspective.
>> 6. Target typing helps the above problem.
>
> the difficult here is the interaction of type dynamic / gradual typing / local type inference   and generics.
>> 9. It sounds unpleasant to use parametric types without inference; it
>> would be problematic if id() and if()then()else() only ever had an
>> inferred type of the dynamic type or the gradual type.
>
> right. and this is the hard issue we're facing...
It's probably worth noting at this point that *nobody has ever
suggested that be the case*. A static dialect can do whatever
inference it wants for its own benefit; in the case of an absent
parameter, something has to be bound to the name at runtime, which is
most sensibly something irrefutable (whether it is actually Dynamic or
not isn't really important). That's all. The principle has always been
that static types do not affect runtime behaviour, and so they
continue not to do so.

It's also worth noting that for code that is entirely
statically-typed, this can never make any discernible difference
because anything that would make it do so will already have been a
static error. The additional annotation Andrew proposed might help the
dialect to do that, although I don't think it solves much on its own.

If you do pattern-matching on types you're explicitly waiving the
principle that static types don't affect runtime behaviour and you
should be similarly explicit about what you're going to give to it. A
static dialect can inspect or use annotations to enforce that if it
wants.

There are other solutions available if Andrew is willing to give up on
the possibility of writing fully dynamically-typed code, or if you
give up on gradual interaction of static and dynamic code. Assuming
that the former is out of the question and the latter creates a new
and worse set of problems, I think this is the best we can get.

This has been previously discussed in July in a thread starting from
here: <http://mailhost.cecs.pdx.edu/pipermail/grace-core/2013-July/001163.html>.
In this, and the contemporary meetings, it was decided that the base
language was necessarily dynamically-typed and typechecking was
performed by a static dialect layered on top. That was required to
address the type-of-self problem and some other issues.

A useful message from that thread is this one:
<http://mailhost.cecs.pdx.edu/pipermail/grace-core/2013-July/001204.html>
(and the one it immediately responds to), wherein Kim supports absent
generic parameters being populated with Dynamic. The static-dialect
solution to the broader problem is my scenario (3), which I think is
what was settled on. That static dialect (or dialects) can report
whatever static errors it likes based on whatever rules, inference, or
out-of-band information it likes, just like any dialect. Other than by
the methods it defines, it doesn't affect the runtime behaviour of the
program.

Run-time gradual checks remain an interesting problem with some
overlap here. I lean towards saying there should be a hook for a
dialect to say how these checks work in its code, rather than baking
in anything particular at the language level.
>> 10. At the same time, I would be pleasantly surprised at a design
>> where type parameters are *always* inferred. Maybe I am not
>> imaginative enough, but the sweet spot seems to be that most of them
>> are inferred, but you can write one down explicitly if you need to.
> always for some suitable meaning of always?
The kind where there is no dynamically-typed code. Or, alternatively,
the kind where to write dynamically-typed code you have to write
static types and to write statically-typed code you don't, which is at
least a fun option.
-Michael