Types are *not* manifest

[apblack]

When we were editing the spec, I said that we should delete all of the text about manifest because it wasn't necessary. Specifically, I said that a type declaration like

    type Wombat = A & B & type {   ...  }

cannot be overridden, and so named types are always manifest, and we are done.

Unfortunately, I was wrong. Although this works for types in modules (because module nicknames can't be overridden), its does not work for types that come from other objects. So if a class generates a new type,

    def newObject = myClass(arg)
    type nOT = newObject.T

the value of type nOT is not manifest, as we would like, because newObject is subject to overriding.

[KimBruce]

Of course we have this problem in spades if newObject is a variable, as we only know (at most) the type of newObject. If we are going to be exporting a type from an object (e.g., have it be public), then the object (and its type definition) must be manifest. For example, this will always be the case for types defined in modules (assuming you don't allow dynamic generation of types -- non-manifest definitions of types -- a very BAD idea if you want to type check). If the type is used within its scope of definition (inside the object defining it, then it shouldn't be a problem as we do not allow overriding a type definition in a subobject/class.

Another option is making any public type in an object be part of the type of the object. However, I then worry about the untyped/partially typed case.

I like the first better and think we need to bring manifest back.

[kjx]

Can fix this with a bit of tweaking. Types and annotations must also be manifest - there was something else there as well I think but the text's been deleted...

[apblack]

I wrote the following in an email of 5 April 2016. It seems to be relevant here:

I think that the reason that we can’t get manifest right, is because you want two different properties.

Types and annotations must have values that are fully-determinable at compile time — manifest Parent expressions must evaluate to objects whose SHAPE is determined at compile time, but whose value need not be — shaped. I would call this “statically-typed”, but whenever I do that, Kim reminds me that his idea of type excludes confidential and required methods, and shape must include them.

Thus, a Number is shaped (because we know that it’s a Number), but it’s not manifest (because we don’t know whether it’s 17 or 42). We want the parents in inherits and use clauses to be shaped, but don’t require them to be manifest. So we can inherit listNode(data), provided that listNode(data) is shaped, even though the value of data might depend on the input.

In the current text, [Numbers], [Lineups], [Strings], and [Objects] are said to be manifest expressions, but that’s not true. Numbers, Strings and Objects are shaped, but can depend on their context. Numerals are manifest, and so are String Literals, but String constructors are not (because the interpolations may not be manifest). In contrast, String Constructors are shaped.

This reminds me of something that confused us for a long time when we were working on Emerald. We had methods that took a type T as a parameter: their signature depended on the value of T.

operation firstKind[T:Type] -> [r:w] where w = ... some type defined in terms of T ...

We also had methods that took an object obj as a parameter: their signature might depend on the type of obj.

operation secondKind[obj:T] -> [res:T] forall T

This distinction seems clear enough once you have realized it — it's a simple level distinction. But until we realized that we needed the distinction, we tried to cram both ideas into the same syntax, and throughly confused ourselves. (Eventually, we wrote typing rules that depended on the values as well as the types of arguments — but took care that the only values that affected typing were type values.)

I think that we are doing something similar with manifest in Grace.

[apblack]

At our teleconference on 31st January 2017, @KimBruce proposed that whenever a type is overridden, its value must not change. This include "indirect" overriding. For example

class first {
    def o = object {
        type T = ...
        ...
    }
    method wombat -> o.T { ... }
}

class second {
    inherit first
    def o = object {
        type T = ...
        ...
    }
}

Even though the two inner objects have no inheritance relationship to each other, the defs of o, to which they are bound, do: one overrides the other. Because we don't want the meaning of o.T in first to change, the definition of T in second.o better be the same as that in first.o.

Can we phrase this rule formally? Is it sufficient to get us out of trouble?

[kjx]

I seem to remember the phrase "Grace has virtual classes, not virtual types" from somewhere.

attempt at some text: "The values of all types manifesty reachable within an inheriting object must be structurally equivalent to the values of those manifest expressions in any ancestor if those expressions are valid". or something.

[kjx]

the classic example:

class graph[[Node, Link]] {
  class node { links : Sequence[[Link]] }
  class link { to : Node, from : Node } 
}

You can extend classes by overriding, but types you have to use parameters:

class myGraph {
   inherits graph[[MyNode, MyLink]]
      alias superNode = node

  class node is override {
     inherits superNode[[MyNode, MyLink]]
     def weight : Number is public = ...
  }
}

In Family-Poly style:

class graph {
  type Node = type { ... } 
  type Link = type { ... } 
  class node { links : Sequence[[Link]] }
  class link { to : Node, from : Node } 
}

class myGraph {
   inherits graph
      alias superNode = node
      alias SuperNode = Node

  class node is override {
     inherits superNode
     type Node = SuperNode & type { weight : Number } 
     def weight : Number is public = ...
  }
}

[apblack]

So the resolution is that whenever a name refers to a type, such as first.o.T then any "overriding" of that name, such as second.o.T not change the value of T. What's an "overriding" of a name? When that name is inherited or used somewhere else., such as inherit first or inherit first.T.

Still not very precise.

The basic idea behind manifest seems to be:

• if a type is manifest, then it's value is known at compile time.
• if an object (other than a type) is manifest, then we know its shape.