Static vs Dynamic Types

[apblack]

This issue is a placeholder for the issue that the spec itself admits. Let me quote the section on Type Annotations, which concludes with "This treatment is types not entirely satisfactory, and is subject to review and change." I believe that this makes it an issue.

Type Annotations

When parameters, fields, and method results are annotated with types,
the programmer can be confident that objects bound to those parameters and
fields,
and returned from those methods, do indeed have the specified types, insofar
as Grace has the required type information. The checks necessary to implement
this guarantee may be performed statically or dynamically.

Static Type Checking

When implementing the static type check, types specified as Unknown will always
conform. So, if a variable is annotated with type

    interface {
        add(Number) → Collection⟦Number⟧
        removeLast → Number
    }

an object with type

    interface {
        add(Unknown) → Collection⟦Unknown⟧
        removeLast → Unknown
        size → Number
    }

will pass the type test. Of course, the presence of Unknown in the type
of the object means that a subsequent type error may still occur.
For example, the code of the add(_) method
might actually depend on being given a String argument,
or the collection returned from add(_) might contain Booleans.

Static type checking is implemented by dialects; various static typing dialects
may impose varied restrictions on Grace.

Dynamic Type Checking

Currently, the dynamic interpretation of types is shallow, that is,
it considers only the methods present in an interface,
and not the types of the arguments or the results of those methods.
This is because, in the absence of type annotations, Grace has no information
about the argument types or the return type of a method.
This means that if programmers annotate a declaration

var x:Number

they can be sure that any object assigned to x has a method +(_), but are not
assured that this +(_) method will expect an argument that is also a Number,
nor that the result will be a Number, even though these details are part of
the Number interface.
Similarly, when the operators <:, :> and == between types are evaluated
dynamically, argument and result types are ignored, even if they are present in the
type definitions.

This treatment is types not entirely satisfactory, and is subject to review and change.

Examples

assert (B <: A) description "B does not conform to A"
assert (B <: interface { foo(_) } ) description "B has no foo(_) method"
assert (B <: interface {foo(_:C) → D} ) description "B has no foo(_) method"
assert (B == (A | C)) description "B is neither an A or a C"

[KimBruce]

At some point I believe it would be useful to do a post-mortem on the language and highlight issues like this that we were not able to resolve to our satisfaction. Hopefully the description will be helpful to others if they stumble into similar issues (or they will suggest a simple consistent solution if known).

…

On Sun, Nov 27, 2022 at 2:00 PM Andrew Black ***@***.***> wrote: This issue is a placeholder for the issue that the spec itself admits. Let me quote the section on Type Annotations <http://web.cecs.pdx.edu/~grace/doc/lang-spec/#type-annotations>, which concludes with "This treatment is types not entirely satisfactory, and is subject to review and change." I believe that this makes it an issue. Type Annotations When parameters, fields, and method results are annotated with types, the programmer can be confident that objects bound to those parameters and fields, and returned from those methods, do indeed have the specified types, *insofar as Grace has the required type information*. The checks necessary to implement this guarantee may be performed statically or dynamically. Static Type Checking When implementing the static type check, types specified as Unknown will always conform. So, if a variable is annotated with type interface { add(Number) → Collection⟦Number⟧ removeLast → Number } an object with type interface { add(Unknown) → Collection⟦Unknown⟧ removeLast → Unknown size → Number } will pass the type test. Of course, the presence of Unknown in the type of the object means that a subsequent type error may still occur. For example, the code of the add(_) method might actually depend on being given a String argument, or the collection returned from add(_) might contain Booleans. Static type checking is implemented by dialects; various static typing dialects may impose varied restrictions on Grace. Dynamic Type Checking Currently, the dynamic interpretation of types is *shallow*, that is, it considers only the methods present in an interface, and not the types of the arguments or the results of those methods. This is because, in the absence of type annotations, Grace has no information about the argument types or the return type of a method. This means that if programmers annotate a declaration var x:Number they can be sure that any object assigned to x has a method +(_), but are *not* assured that this +(_) method will expect an argument that is also a Number, nor that the result will be a Number, even though these details are part of the Number interface. Similarly, when the operators <:, :> and == between types are evaluated dynamically, argument and result types are ignored, even if they are present in the type definitions. This treatment is types not entirely satisfactory, and is subject to review and change. *Examples* assert (B <: A) description "B does not conform to A" assert (B <: interface { foo(_) } ) description "B has no foo(_) method" assert (B <: interface {foo(_:C) → D} ) description "B has no foo(_) method" assert (B == (A | C)) description "B is neither an A or a C" — Reply to this email directly, view it on GitHub <#197>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/AAN2D6WRXUUKOMUMGOLO343WKPKWDANCNFSM6AAAAAASMXDUTU> . You are receiving this because you are subscribed to this thread.Message ID: ***@***.***>

-- Prof. Kim Bruce Computer Science Pomona College

[kjx]

This treatment is types not entirely satisfactory, and is subject to review and change.

I'm very much tempted by going to a symmetrical, deep type conformance semantics and letting the chips then fall where they may. Ignoring types on interaces just seems, well, wrong (see example below). Alternatively (perhaps even better) - stealing Michael Ernst's "Ductile" idea and just always run all the types all the time at runtime. So we're not (and don't claim to be) any kind of gradually typed language: removing type annotations will change how things behave (so there's no gradual guarantee, because ultimately that's stupid, for just this sort of reason) We'd just say writing method m (x) { x } meant the same as method m(x : Unknown) -> Unknown { x } (or if andrew prefers. something closer to) method m[T](x : T) -> T { x } aka method m(x) -> staticTypeOf(x) { x } http://mernst.github.io/ductilej/ def o = object { method m (n : Number) { } } type MString = interface { m(s : String) } match (o) case { x : MString → print "got object with string parameter to method m" print "so I then expect the following should work" print "but it doesn't" o.m("Sorry") print "never get here" } else { print "who knows what I got" } print "done" got object with string parameter to method m so I then expect the following should work but it doesn't TypeError: argument to request of `m(_)` does not have type Number. It is string "Sorry" (defined in module built-in library), which is missing methods %(_), +(_), -(_), ..(_), /(_), @(_), ^(_), abs, acos, asStringDecimals(_), asin, atan, ceiling, cos, downTo(_), exp, floor, inBase(_), isEven, isInteger, isNaN, isOdd, lg, ln, log10, prefix-, prefix<, prefix>, prefix≤, prefix≥, rounded, sgn, sin, sqrt, tan, truncated, and ÷(_). raised from o.m(_) at line 3 of Welcome requested from module initialization in native code

[apblack]

I wasn't aware of DuctileJ. It's approach to programming seems a lot like what we originally aimed for with Grace: provide type-security when the programmer wants it, but don't force it down their throat when they don't want it.

Yes, @kjx is quite right: not looking at arguments and result types of methods when doing type tests "is not entirely satisfactory", i.e., wrong. Therefor it is worth remembering why we do this.

In a program with static type declarations on every method, it would be unnecessary. But if we have an object o with a method m whose argument is Unknown (equivalent to being unspecified), what are we to do? If we say that o conforms to MString, we might be wrong. If we say that it does not conform to String, we might be wrong. I would like to say "we don't know", but the semantics of match(_)case(_)... doesn't allow that. (Isn't that the reason that Jerremy decided that Grace wasn't gradually typed?)

I was hoping that type inference might help. I have no wish to infer the types of variables, in fact, I don't think that it's possible (in general), but I was hoping to infer the types of method arguments and results. A little thought, though, says that so long as we can't infer the types of variables, we won't be able to infer the types of methods (in general). Yes, we can do so in some special cases.

What else can we do? We could decide, dynamically, that if an Unknown is ever presented as an argument for a Pattern match against a non-unknown type — at any depth of a type comparison — then an exception InsufficientTypeInformation is raised. Getting a good error message might be challenging (i.e., might need a better implementor than @apblack), but ought to be doable.

@kjx says: "I'm very much tempted by going to a symmetrical, deep type conformance semantics and letting the chips then fall where they may." I don't know what that means. We know that deep type conformance is the right thing to do; the question in front of us is what do we do when we can't do the right thing?