[Grace-core] Declarations for static reasoning

[Timothy Jones]

I've been stirring a bit of a discussion about 'statically-known' and what
constructs in the language that dialects should be reasoning about, partly
because I think it's important for the language, but mostly because I'm trying
to rewrite the Brands paper and there are some outstanding issues with how the
proposed branding mechanism interacts with the rest of the language.

Here's a (modified) snippet from the old paper:

  def myBrand = brand.new
  type MyBrand = myBrand.Pattern & type { ... }

  def myObject : MyBrand = object is myBrand { ... }

This code doesn't work in Hopper. Type declarations are 'hoisted' to the top of
the scope they are declared in, partly due to the handling of mutually-recursive
type definitions. The right side of the type declaration refers to 'myBrand',
which is not yet defined because of the hoisting behaviour. Also, the type
declaration is declaring a value that is not a 'type' in the (structural) sense
that the rest of the language uses, but it is something that the branding
dialect will reason about statically.

What I need is to have an expanded definition of 'static declarations'. I have
several different ideas about how this could be achieved, but for now I would
like to discuss the simplest idea: rename type declarations to 'let' (or some
other word, it's not really important at the moment) declarations, where the
expression on the right side of these declarations must be statically-known. The
snippet above would then be:

  let myBrand = brand.new
  let MyBrand = myBrand.Pattern & type { ... }

  def myObject : MyBrand = object is myBrand { ... }

These new declarations would be hoisted, but otherwise run in order, and allow
for mutually-recursive definitions and generics. They could not be overridden by
inheritance. I'm going to hand-wave on mutual recursion, generic parameters, and
the definition of statically-known for now, to keep this short, but the short
answers are placeholders, memoisation, and values whose structure can reliably
be determined before running the program. Note that statically-known does not
rule out side-effects.

The other outcome of this change would be that classes could translate into let
declarations rather than defs, which would make them declarative and also allow
them to have generic parameters. The definition of statically-known would not
include object constructors stored in defs, but would include the same for lets.

I have a partially complete proposal that enumerates more of the specifics in
detail if there's interest. The primary point at the moment is that there needs
to be a change in the way that these declarations are handled to support the
behaviour in the paper (and presumably future dialects as well), where values
other than structural types need to be reasoned about statically.

-- 
Tim