[Grace-core] Declarations for static reasoning

[Kim Bruce]

As you know, I prefer to be conservative about making changes to the language at this point.  You seem to suggest that there might be other places where having compile time determinable values are useful.  How important are those?

My initial reaction is to be conservative.  One of the wonderful things about Grace is that we have keywords that actually tell you what kind of thing you have: var, method, def, type, etc.  As a result, I am loathe to give up the keyword type as it tells you exactly what you have and how you can use it.  (I am especially sensitive to this now that I am teaching Java to my Grace programmers and am very much noticing the lack there.)

I'm more inclined to treat the brands as a special kind of object and allow a statically determinable brand be something that could be mixed in to a type statically to form a new type.

As I think about this and similar issues we have been discussing, I realize that we are talking about two related, but different notions.  At one end we have static types that are used for static type-checking.  At the other end we have patterns that are designed to be used for dynamic checks of objects.  All types can be used as patterns, hence the close ties between them.  As I recall, patterns were invented to be used in match statements.  Static types can be used as patterns (though I find it convenient to think of the associated patterns as objects that are created when the static type is created).  As well as in match statements, types as patterns are used when we are doing dynamic type-checking (presumable these would/could be disabled in the dialect with purely static typing).

Now patterns are just ordinary objects and can be passed as parameters, for example.  On the other hand, type parameters of the sort we have previously discussed (used in context with <T> or [T]) have much more restrictive usage.  They can be used for static type checking, but only in restrictive ways that correspond to our knowing only some information about them statically (e.g., they may satisfy a type constraint).  Of course they are also patterns, and presumably could be used in match statements or with more exotic operations, but static type checking depends on our using them in only restrictive ways.  Once we lose track of them as static types, they may no longer be usable for static typing.

So what about brands?  In Modula-3 they seem to have very limited use. Brands are created only as part of a type, and the constructors of objects of that type seem to only be definable in the module in which the type is defined -- i.e., the brands cannot escape into the world, and operations that create objects with these branded types seem to have to be part of the same module.  It seems to be the intention (I find the report a bit fuzzy on this) that branded types are "partially revealed" so that outside the module in which the type is defined, no one else can create object or functions that create objects with that branded type.  Instead objects with that brand are constructed only via operations defined in that module.

That seems quite reasonable to me as a general framework (though I'll interested to hear if we have broader ambitions).  Thus it seems reasonable that a brand can be used to create objects with that brand and to design classes creating objects with that brand, but only within the scope of definition of the brand.  However, the brand cannot be exported.  Thus if we define the Fraction type with an associated brand, then classes generating object of type Fraction (e.g. fractionPair.n()d() ) can only be defined in that same scope.  Of course the classes themselves can be exported.  I am guessing that we would also be fine with subclassing fractionPair outside of the scope of the definition of Fraction and its brand, but I can also imagine a desire (or at least an option) to treat such classes as final.  As Tim points out, the compiler needs to process the brands at the same time we process types as they impact type definitions.

Of course the subclasses might generate objects of some type ExtendedFraction extending type Fraction and that have their own new brand.  Classes generating these likely would need to have been defined as subclasses of the original fractionPair in order to generate the right branded type Fraction.

Of course our branded types need to be able to be used as patterns, but that seems doable given everything else (objects could hold their brand(s) along with their run-time type).

As it is, it seems like we can have brands that have no operations on their own (they are not patterns), but instead can be mixed in to types to form new static types (and hence new patterns).  Of course we do need to be able to statically determine brands and make sure that all brands introduced are unique.  Modula-3 does this by making them all be created from string literals (explicitly or implicitly), thus making it easy to check if there are repeats at link time.

Is my understanding of how Modula-3 uses brands and our intentions correct?  Please let me know if I've missed something important.  (I've left out the reasons as to why we want them at all, but hopefully that is already known to readers.)

I know this is incomplete -- for example I haven't thought through branding type functions (can we brand the function Stack<T> as opposed to branding the type Stack<String>?) and I'm sure there are other issues remaining, but I'm hoping this will serve as something concrete we can refer to when looking at proposals.

 
Kim



On Nov 23, 2014, at 8:27 PM, Timothy Jones <tim at ecs.vuw.ac.nz> wrote:

> 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
> _______________________________________________
> Grace-core mailing list
> Grace-core at cecs.pdx.edu
> https://mailhost.cecs.pdx.edu/mailman/listinfo/grace-core