[Grace-core] Statically-known and family-polymorphism

[James Noble]

Hi Tim & all

a few comments on this (tho' I think we should stick with the square bracket stuff first...)

> As part of trying to hash out a proposal for extended static reasoning, Michael
> and I were trying to precisely define what is meant by 'statically-known'.

so this is good, and something we really need to do. 

> The point of statically-known is that we know exactly what the structure of an
> object will be, which is particularly for sanity checking inheritance. We came
> up with the following definition.
> 
>  Start with either:
> 
>  1) An object constructor that is not tail-returned by a method
>  2) A dialect
>  3) An import which can be resolved to an object definition
> 
>  Then you may chain together requests on these statically-known objects so long
>  as the requested methods tail-return an object constructor.

> This seems to restrict the ability to do family-polymorphism, 

Well right. So the question we need to ask is "why"?
I think there are two reasons:
 - a) to ensure we can type check code statically
 - b) to ensure we can implement straightforwardly

Of this, a) is quite important: we want to check statically. Type systems without
family polymorphism are simpler that those that support it.   

b) is also quite important, but it depends on assumptions about the implementation.
If we want one Grace (generic) class to correspond to one JVM class, for example,
then family poly will need either a rather complex encoding, or dynamic class generation --
or it's easier not to support it.   On the other hand, on JS, or PyPy, or possible Truffle,
we won't have such problems. 



            ~             ~             ~             ~ 

(a rather longer discussion)


More generally, there seem( to be several different kinds of statically-known or constant timescales and scopes here:

* context-independent static constant  - Tim's proposal: a name / expression evaluates an object that can be determined before execution begins, irrespective of the wider context.  Obviously this expression always evaluates to the *same* object. 

* context-dependent static constant - a name / expression evaluates an object that can be determined before execution begins, but that may depend on static contexts (e.g. inheritance) that can be determined at compile time.  The expression always evaluates to the *same* object in any context, but the same expression may evaluate to different objects in different contexts.  Think C++ templates, where you can e.g. create new instances of template parameters because the templates are fully expanded at compile time, or I guess family polymorphism - although, again, thinks like Jet or J& - class-in-class nesting, could in theory expand out all the class families at compile time.

* context-dependent dynamic constant - a name / expression always evaluates to the *same* object, although which object may depend on context that may only be determined as part of execution.  I think this is basically a "pure" request.
Grace's defs - especially "per instance defs" that depend on constructor parameters - are in this class.

* variable: a name / expression that evaluates to different objects at different times.  Grace's vars.

(and yes, the names are horrible).

We use "var"s to declare variables, and "def"s to declare all types of constant --- although really all we can be sure about are that the result of defs are at least "context dependent constants".   We currently don't distinguish between different types of constants --- that is to say we have no syntax for annotations or for ensuring a value is a "more constant constant" :-) 
While we distinguish these timescales on declarations, we don't through method requests --- a type {  foo -> T }
says that requesting "foo" yields a T; but there's no way to say that the "foo" request should be constant (i.e. that a foo request to the same object must always return the same object), or that it should be static (i.e determinable at compile time).
We mostly want both types and superobjects in inheritance to be static, but we differ about context-dependence. 

Grace explicitly supports the bottom two levels for variables - or rather, the var vs def distinction is the bottom level vs all the rest.  I take Tim's message to mean - at least - we need to decide to which of the top two levels types and superobjects should belong.

It would be possible to have a language that recognised more than two of these levels explicitly.
It would also be possible to have a language that made this distinction for code as well as data - 
methods as well as fields - although you may then get in to e.g. timeframe polymorphic methods.
I bet Rust does some of this, as did the older Jan Vitek / Tian Zhao ownership systems for real time programs
that made distinctions between memory spaces for ROMable constants, the stack, and the heap.

Perhaps ML is another extreme data point where one functional language - the module language - handles static computation, while the core language (without vars) gives pure computation.  The catch there is that many similar features (defining names, defining functions, invocations) are implemented by completely different constructs in each language.

In Grace so far, for modules if not for types, we're trying to follow Newspeak amongst others by using the same constructs at different levels (e.g. both objects, that are dynamic, and modules that quite static)

J