What we need to say about Types

[apblack]

I've moved this from an email thread, so that we can have a hope of finding it again.

Kim Bruce wore (email of 6 June 2017 at 15:00):

I’d appreciate it if everyone could take a look at the document objectLitType.md that I sent several weeks ago. It can also be found in this gitHub repository under languageSpec/objectLitType.grace on the newTypes branch

It is my first shot at specifying types associated with object literals in Grace.

[apblack]

OK, you get marks for trying (yet again).

:-)

Alias has been in the spec, and in the implementation, for a while now. But aliases don't affect the annotated type of an object, because they create confidential methods.

yeah, and it's been in kernan for years.

Kernan supports this though:

class c -> CRETIN { ... method a { 1 } ... }

class d {
... inherit c
... alias b is public =3D a
... } d.b
1

which you'd talked about, I didn't like, I though that had gone in anyway.

then - assuming the resulting object's structure is OK (modulo gradual structuralism rules) - can't we just take the resulting object definition, AFTER exclude & alias & inherit & Use & whatever are done. and then do steps 4-6?

Steps 4-6?

on pages 2 & 3 of kims document. Should probably be 2-6 actually. the rules about how you generate method signatures from declarations within objects. it's possible this could be simplifed too, depending on how e.g. we word the description of def & var: do they in some sense create methods, or do they allow an object to handle one or more requests (but without creating methods)

another peripherialy related but really important point:

(though we would expect the dynamic type checker to catch most such inconsistencies).

we need to say what dynamic type checks do, when they are invoked, how and when the type objects are bound. some of that is implied in section 10 of the spec, most of it isn't.

[apblack]

On 7 Jun 2017, at 19:00 , kjx kjx@ecs.vuw.ac.nz wrote:

OK, you get marks for trying (yet again).

:-)

Alias has been in the spec, and in the implementation, for a while now. But aliases don’t affect the annotated type of an object, because they create confidential methods.

yeah, and it's been in kernan for years.

Kernan supports this though:

class c -> CRETIN {
... method a { 1 }
... }

class d {
... inherit c
... alias b is public = a
... }
d.b
1

We agreed not to do this; we agreed that aliases should always be confidential. If you want to make an alias public, you would have to do something like

alias b'(_,_) = a(_,_)

method b(a, y) { b'(x, y) }

I actually like what kernan does; just as one can annotate a def (or a nickname for an import) as public to create a method to access it, I don’t see why one should not be able to annotate an alias. But it's not a big deal, because alias is not used all that often in the first place.

Note that in one of the current known deviations of minigrace from the spec is that aliases are not confidential; they have whatever visibility the original method had. Fixing this will involve a new way of designating methods as confidential, which I will probably get to during my sabbatical.

which you'd talked about, I didn't like, I though that had gone in anyway.

I don’t belive that it was ever in the spec.

then - assuming the resulting object's structure is OK (modulo gradual structuralism rules) - can't we just take the resulting object definition, AFTER exclude & alias & inherit & Use & whatever are done. and then do steps 4-6?

Steps 4-6?

on pages 2 & 3 of @KimBruce 's document. Should probably be 2-6 actually. the rules about how you generate method signatures from declarations within objects. it's possible this could be simplifed too, depending on how e.g. we word the description of def & var: do they in some sense create methods, or do they allow an object to handle one or more requests (but without creating methods)

Kim and I agreed yesterday that most of what he wrote in his document is already in the spec in other forms. I added (yesterday)to the spec a few sentences that say that omitted type annotations are equivalent to Unknown. The spec already talks about the meaning of omitted visibility annotations. So we needn’t, and shouldn’t repeat that stuff.

Most importantly, the spec also explains what attributes are present in an an object that’s built using an constructor with inherit and use clauses. We shouldn’t repeat that either.

The stuff that we do need to say, for type-checking, is that every (dynamic) object has what we proposed calling its annotated type. This is not it’s “best fitting” or principal type (the one that describes it most precisely), but rather it’s the one that can be deduced from the annotations that the programmer provided (or omitted to provide). For example, if my pedigreePussy object has

def miceEaten:Unknown = 0

then it’s annotated type will contain

miceEaten -> Unknown

even though one might trivially deduce that the result of miceEaten will always be a Number.

another peripherialy related but really important point:

(though we would expect the dynamic type checker to catch most such inconsistencies).

we need to say what dynamic type checks do, when they are invoked, how and when the type objects are bound. some of that is implied in section 10 of the spec, most of it isn't.

Are we perhaps better not saying much of this? For example, suppose that I declare

    method count -> Number

Then I think we should say that the Grace language implementation will guarantee that the result of method count will always have an annotated type that matches Number, but we should carefully not say what mechanism is used to achieve this guarantee. It might be a run-time check, or it might be a compile-time check: can’t we leave unspecified which?

[kjx]

On 9/06/2017, at 11:08AM, Andrew Black notifications@github.com wrote:

The stuff that we do need to say, for type-checking, is that every (dynamic) object has what we proposed calling its annotated type. This is not it’s “best fitting” or principal type (the one that describes it most precisely), but rather it’s the one that can be deduced from the annotations that the programmer provided (or omitted to provide)

I think I like this idea - not sure I like the name though, it sounds like the type itself has been annotated, not the object.

"annotation" type? "declared" type? "explicit" type?

[apblack]

We discussed and discarded "declared type", because it's not declared. Of course, as you point out, it's not annotated either. Neither is it explicit.

I like "annotation type", though: it's derived from the annotations.

[kjx]

Are we perhaps better not saying much of this? For example, suppose that I declare method count -> Number

so: we need to say how "Number" is resolved, and when, and what the constraints on that resolution are. This is far from trivial.

Then I think we should say that the Grace language implementation will guarantee that the result of method count will always have an annotated type that matches Number, but we should carefully not say what mechanism is used to achieve this guarantee. It might be a run-time check, or it might be a compile-time check: can’t we leave unspecified which?

dunno. I don't think so. How important is portability (i.e a consistent semantics)? How important are "Nixonion" semantics. Should there be dynamic options that can always TRUMP explicit declarations.

If we didn't want to be Nixonion, then we can set things up that

• there is an operational semantics which explains when & how types are checked at runtime
• the existing dialect options allow us to layer static checks on top of that. I guess that's how it works in my head.

if we want to always be able to TRUMP the annotations, then the operational semantics needs a "Comey switch" at least :-)

If we do this: method passNumber(x) -> Number {x} print(passNumber("x"))

under what circumstances is it permissable for this program to complete and print "x" (assuming Number binds to what we normally thing of as Number, "x" isn't a Number, and "x" can be printed)

frankly I think we should tie this down more...

J

[KimBruce]

I'm happy with "annotation type"

[apblack]

Why is resolving Number "far from trivial"?

Defining what Number should be is far from trivial, but resolving it isn't; it's just outer.Number or self.Number in the usual way.

One example of where defining Number is tricky, which Kim & I discussed yesterday, is the signature of +(_). It's something like

    + (other: R) → R
        where R = Number | W
        where W matches Addable

type Addable = interface {
    reversePlusNumber(n: Number) -> Self
}

This is trying to say that the result type of +(_) is the same as the type of the argument, and that the argument must either be of type Number or of a type that matches Addable. For example, Point matches Addable, because it has a method

    reversePlusNumber(n: Number) -> Point

and if you do 1 + (3@4) you get as result the point (4@5)

As for the "Nixonian" stuff, I don't understand what you are saying. And I certainly don't want TRUMP in our language.

[kjx]

As for the "Nixoniam" stuff, I don't understand what you are saying. And I certainly don't want TRUMP in our language.

sorry - I lost track of with which dodgy president you were comparing: should be GWB

Wilson (hard static checking) Murrow (static warnings, dynamic checking) GWBush (no static checks, dynamic checks only)

the question still remains - do we distinguish between dynamic checks resulting from type annotations, vs dynamic checks required without which programs cannot progress (e.g. method requests, basically). I thought this was your GWBush semantics, but it seems worse.

so, yeah, Nixon... (or TRUMP) ignore checks written in to code and crash only when you really cannot force things to continue

[kjx]

Why is resolving Number "far from trivial"?

initialisation order I think. Michael would know better. but say:

object { def x : Number = 3 type Number = interface { ... } }

is rewritten to

object { def x : Number = 3 def Number = interface { ... } }

then there are obvious problems. at least, types should probably be manifest, and the Object Combination and Initialisation section should talk about when types are initialised.

One example of where defining Number is tricky, which Kim & I discussed yesterday, is the signature of +(_). It's something like

why can't we have

type Number = interface { +(_ : Number) -> Number }

and

type Point = interface { +(_ : Point) -> Point }

This is trying to say that the result type of +(_) is the same as the type of the argument, and that the argument must either be of type Number or of a type that matches Addable

why isn't Number <: Addable ?

and if you do 1 + (3@4) you get as result the point (4@5)

a) only if you support that, rather than requiring (1 @ 1) + (3 @ 4) when the simpler types will work fine.

or

b) you're doing type inference. You could have

type Number = interface { +[T](_ : T) -> T where T <: Number }

but then you'd have to write:

1 +_[Point] (3 @ 4)

and if you write 1 + (3 @ 4)

you'd get return type Unknown

otherwise, well, you've got two unbound type variables in your signature

James

OK there's another option: allow "top level type disjunctions" aka type overloading (but not method overloading) rather than something like

type Number = { +(_ : Number | Point) -> (Number | Point) }

you'd want

type Number = { +(_) : ( ( Number -> Number ) | ( Point -> Point ) )

which comes down to

type Number = { +( : Number) -> Number +( : Point) -> Point }

[apblack]

Yes, I agree that we need to define the semantics of type declarations. I have tried to talk about this before. Clearly, they can't be anything like defs because they are mostly recursive. Hence, we need a rule that allows, and gives a meaning to

type X = interface { 
    wombat(_:X) -> X
}

but disallows

type X = X

The reason that Number does not conform to addable is that Number does not implement reversePlusNumber.

The reason that we need matching in general is that, while Point does conform to Addable, that's true only because in this little fragment there are no arguments of type Self.

If we have a type like

type M = interface { 
    wombat(_:M) -> M
    kanga(_:M) -> M
}

then M does not conform to X, but it does match X.

We do need a way of saying "the type of the result of this method is the same as th type of the argument". Type parameters don't let us do that.

Your discussion of multiple generations of bad US presidents has me all at sea. We probably need to have a meeting to talk about that, at least in so far as they affect Grace, and I'm sure that my views have changed over time. But, briefly, I think that If I take the trouble to annotate a variable or a method with a type, then that annotation should have the semantics of an assertion: I should be guaranteed that any object bound to the variable, or returned from the method, does indeed have an annotation type that matches the annotation.

Why should it be the purview of the language spec to say what mechanism is used to achieve this guarantee?

[kjx]

We do need a way of saying "the type of the result of this method is the same as th type of the argument". Type parameters don't let us do that.

sure they do - or rather, they let everyone else do that. Even Java. The catch is that they do type inference to get there. Michael's proposal to decouple the "static" and "dynamic" type systems: this is why

I think that If I take the trouble to annotate a variable or a method with a type, then that annotation should have the semantics of an assertion:

I'm not unhappy with that.

Why should it be the purview of the language spec to say what mechanism is used to achieve this guarantee?

portability. consistency. I bet there are corner cases - more than corner cases - where this is observable

James

[apblack]

sure they do - or rather, they let everyone else do that.

I would have said not, because what I want to do here is make the type of a method depend on the type of a value argument,. In contrast, what type parameters do is make the type of the method depend on the value of a type argument. But yes: using inference of omitted type parameters lets some languages shoe-horn these two different things into the same box.

I think that having separate mechanisms (Emerald used types introduced by forall T, as well as type parameters) for these two different use cases makes sense in the abstract. We also have the problem that we have said that omitted parameters are not inferred.

I bet there are corner cases - more than corner cases - where this is observable Of course it's observable! If it were not, why would we be interested in static type checking at all?

I've just realized that we are making stuff more complicated that necessary by allowing

type X = interface { 
    wombat(_:X) -> X
}

We don't allow the equivalent object definition; instead we require that self references in an object be written self. SImilarly, we could require that self-references to a type be written Self.

When one is defining two mutually recursive types, this can get awkward, though. I think that one has to be inside the other, and refer to the outer one using outer.

[KimBruce]

The type:

type X = interface { wombat(_:X) -> X } will eventually (once we get Self type in place) be different from:

type Y = interface { wombat(_:Self) -> Self } The first is a closed recursion, while the second is open. If you let type U = X & {m: Number -> Number} and u: U then u.wombat will still accept any parameter of type X. However, if you let type V = Y & {m: Number -> Number} and v:V then v.wombat will still require a parameter of type V (i.e., it must have an m method).

It is reasonable to include both of these in the language.

Of course, we don’t have Self in there at all at the moment, and our first pass will likely restrict Self to only positive occurrences (no parameters), but that is the long-term hope.

Kim

[kjx]

On 13/06/2017, at 10:11AM, Andrew Black notifications@github.com wrote:

I would have said not, because what I want to do here is make the type of a method depend on the type of a value argument, and what type parameters do is make the type of the method depend on the value of a type argument.

so the parallelism is cute, but...

But yes: using inference of omitted type parameters lets some languages shoehorn these two different things into the same box.

it's the same box. I mean, the point of Damas/Hindley/Milner is to set up just those dependencies (and the other dependency, on the return type context, which I hate...)

you could equally see the "type of a value argument" as an extra implicit type parameter (I'd guess that's the way Kim sees it)

We also have the problem that we have said that omitted parameters are not inferred.

yes. that's the big problem. having two mechanisms or two kinds of type parameters, one inferred and one not, doesn't seem ideal either.

I don't know a good design here - but I think nobody does: this is why Gilad is now anti generics ;-)

I bet there are corner cases - more than corner cases - where this is observable Of course it's observable! If it were not, why would we be interested in static type checking at all?

OK so I didn't express myself very well there. Where I'm reluctantly getting to is

• at some level, static and dynamic systems are incommensurable
  (how that works for the generic contracts with blame stuff I don't know..)
  • or we have to bring in type inference, and that type inference must cross over from static types to dynamic types (which may be what the dynamic contracts stuff does)

[kjx]

So, I now think we may be able to get away with type and annotations being nothing more than requests #135.