[Grace-core] RFC: Compile-time constants

[Timothy Jones]

We've been talking about the syntax for types and constants, and I've been
particularly vocal about changing our current approach. Here's a quick summary
of things so far, so we're all on the same page about why things are as they are
at the moment.

Because types are runtime objects, there is no clear separation between the type
and value language, as indicated by the shared namespace. While anything that
appears inside of a type must also be a type, a type is a valid value and may
appear anywhere that any other expression is allowed. This produced an ambiguity
between certain types and blocks: '{}', '{ a }', '{ a -> b }'.

So we moved to prefixing type literals with the 'type' keyword, which was
already in use as prefix of a type declaration. We discussed (mostly on the
wiki) whether to just make type declarations normal 'def' definitions instead.
This produces several problems:

- Mutual recursion: if two named types use one another, they defy the normal
  imperative behaviour of defs, which are only available as variables *after*
  their declaration site (or have undefined values that explode if touched when
  they're also fields).

- Generics: the value of a def is set once evaluated. The underlying object can
  be modified, but two consecutive references to a def should produce the same
  object. Type names need to be able to take generic arguments, and as types
  exist at runtime this would turn defs into functions that take optional
  parameter arguments.

- Overriding: defs can be overridden in a sub-object. Overriding types doesn't
  make sense, as they need to be invariant outside of 'where' clauses.

So we've opted to keep the 'type' keyword, and have sugar for the case where the
type value is directly a literal to avoid unnecessary double-ups. This is where
we are at the moment. I'm not a huge fan of this syntax, but it's a reasonable
compromise in the context of types being only structural type literals and
combinations of those types.

But types aren't only structural type literals and their combinations. In the
presence of dialects -- which are capable of checking *any* property that can
feasibly be checked statically -- anything can be a type. In the interest of
sanity (and because we've had this confusion before), I'm going to talk about
the *structural* types as 'types' and anything else that a dialect wants to
reason about as 'statically known'.

In the branding system, 'brands' are just objects that are created with a
'brand' keyword. They have a method 'pattern' that will dynamically match any
object that has been branded with that brand. The accompanying dialect does its
best to statically follow the identity of a brand in the program, and match an
object's statically known brands with the statically known associated patterns.
Thinking of a brand's pattern as a type, I'm tempted to write this:

  def aThing = brand

  type Thing = aThing.pattern

  def myThing : Thing = object is aThing {}

But this doesn't work, as the pattern isn't a type, it's just an object that
I've arbitrarily decided to statically track. And it doesn't make sense to base
the value of a static type on a runtime object: I shouldn't be able to reference
a variable created by a def on the right hand side of a type declaration,
because that object doesn't exist at compile-time. So, at the moment I write
this:

  def aThing = brand

  def Thing = aThing.pattern

  def myThing : Thing = object is aThing {}

This is fine. Even though Thing isn't declared as a type, I've written a dialect
that can (conservatively) check it statically in the same way as a type. The
runtime semantics are exactly what I need as well.

But what if these two statically separate realms start converging? A brand needs
to be combined with a structural type in order to produce the full functionality
of a nominal system.

  def aThing = brand

  def Thing = aThing.pattern & type { name -> String }

  def myThing : Thing = object is aThing { def name is public = "My Thing" }

Now we're into murky territory. I can ensure that my dialect checks both brands
and structural types, but what if I need generics in the structural type? Or
mutual recursion between types that involve brands? What if someone overrides my
pattern?

So type declarations aren't right, and neither are defs. What we need is some
sort of declaration that means, "this value is statically known". We also need
different semantics for evaluating these declarations, to handle evaluating them
in a way that supports both hoisting and mutual recursion (that is, the
declarations are considered to all appear simultaneously at the top of whatever
scope they appear in). The semantics are important, and are also the hard part.

First, syntax. Both 'const' and I think 'manifest' have been suggested as the
opening keyword. I'm not sure if anyone suggested 'static'. Both 'const' and
'static' have different meanings across different languages, and I'd rather the
keyword be shorter than 'manifest'. I quite like using 'let', so I'm going to
use that for now, and we can have the bikeshedding argument later.

  let MyType<T> = type { thing -> T }

  let aThing = brand

  let Thing = aThing.pattern & type { another -> MyType<Thing> }

  def myThing : Thing = object is aThing {
    def another is public = object { def thing is public = outer }
  }

The static behaviour of this example should be clear, but all of the
declarations contain real objects which must be created at runtime. So, the
right-hand side of a declaration must be 'statically known': either a type
literal, a generic parameter, the dialect, or a request for a let declaration or
a method that is annotated as static (either in scope or on another statically
known value).

So branding would be declared in the dialect as (again, delaying bikeshedding on
the annotation name):

  class brand is static {
    let pattern is public = brandPattern
  }

  class brandPattern is static {
    inherits basicPattern

    method match(obj) { ... }
  }

The basic pattern contains the & and | combinators, which are also marked as
static, and can handle combining static definitions which haven't been created
yet (through some 'becomes' magic, assumedly). At runtime, the declarations are
hoisted to the top of the enclosing scope and then executed in whatever order.
They appear as methods on the surrounding object, but cannot be overridden.

There is more to discuss here, but I don't want to go on too long, and I would
like some feedback. Andrew mentioned that he would like statically known
declarations for traits, so I would like to know more about that use case.

-- 
Tim