We decided that we did not want to wire a dependency on type inference into the semantics, and therefor match for type patterns is the zero-level match, which looks at the methods that are present but not at their argument and return types.

did we? I know that's what mg, kernan, moth (& slug) have pretty much always done but I'm not sure that's what the spec says:

https://github.com/gracelang/language/blob/master/languageSpec/spec.md#type-assertions

the problem with this is, it seems to me, that interfaces & types will behave differently from the way that they look: their type annotations are ignored anywhere they matter, so all these types mean the same thing:

type N = interface { 
  m(_ : Number) 
}

type S = interface { 
  m(_ : String) 
}

type U = interface { 
  m(_) // argument & result types treated as Unknown, consistent with everything
}

and this object would match all of them:

object rat = {
  method m( r : Rat ) { } 
}

The catch is, then, that the actual behaviour is... rather nonintuitive, to me at least. If we really don't want to use argument & result types in type tests, we shouldn't allow type annotations in interfaces, rather than allowing them and ignoring them.

The thing is, that for the dynamic semantics, we don't have much choice. We can't, in general, know the parameter and return type of methods — all we can know is their names. Of course, it might be that the method is annotated with parameter and return types, but we can't rely on that, because annotations are optional.

So either we make the semantics depend on type inference — in which case we have to specify exactly what inference — or we make it independent of parameter and result types.

Note that just because N, S and U all match

interface Rat { m(_:Rat) -> Unknown }

does not mean that the static type checker will say that they have type Rat. Dynamic matching is a super-relation of static typing.

We want the semantics of static typing to be in the hands of the writer of the typing dialect — of which there may be several. So the meaning of types as object — the dynamic matching semantics — needs to be

implementable, and
consistent with (i.e., weaker than, or forming a lower bound for) all reasonable static semantics.

Can you suggest another option that is consistent with these requirements?

Can you suggest another option that is consistent with these requirements?

No - but the current semantics aren't necessarily consistent either (e.g. consider a nominal static checker - is that "reasonable")? The "erase all annotations for dynamic checking" semantics isn't that far from Java's erasure though --- if anything taking it one step further (not just "generic" parameter are erased, but all type annotations) and I'm not sure Java's model is something we'd rather emulate.

The "Right Thing" option would be to require "deep" dynamic checks, potentially with some form of blame.

But if we go with the Boyland "erase all annotations for dynamic checking" semantics, the spec should make that clear -- that way, we can claim we do actually meet the current Grace spec in the Moth paper :-)

James

Can you suggest another option that is consistent with these requirements?

No — but the current semantics aren't necessarily consistent either (e.g., consider a nominal static checker - is that "reasonable")?

Nominal semantics are fine, because a sound nominal system can usually be defined as "structural & the programmer said so", which clearly implies structural, which in turn implies zero-level structural.

But the substance of your objection is right. I can think of at least one typing regime that is not a strengthening of zero-level structural: Eiffel's unsound co-variant typing. Presumably there are other unsound typing regimes that we are excluding too. Does that limit what a static type-checker can do? I don't think so: it just limits the usefulness of any "certification" offered by the type checker. An unsound static checker is more like Lint than a guarantee service.

The "Right Thing" option would be to require "deep" dynamic checks, potentially with some form of blame.

Well, it might be "right" if it were implementable. "Deep" has to mean "infinitely deep". The only way one can know the return type of a method is to invoke it, and look a the resulting object. Where is the source for the arguments for that invocation? I suppose that we could do symbolic execution... How do we "tie the knot" and identify when the result of one method is definitively of the same "shape" and hence the same type, as another? If we can't do that, when does the deep dynamic checking terminate?

These are interesting research questions, but I don't think that they are questions that every Grace implementation needs to solve before it can claim to implement the full Grace language.

We could just get rid of type tests altogether, and then this question would not arise! But I find them quite useful. I think the important thing is not to confound the guarantees offered by the run-time checks (zero-level matching, or a user-defined pattern returning true) with the guarantees offered by the static checker.

Or we could give up structural typing in favour of nominal typing...

there is also the problem that the current spec does not say our current semantics are shallow. the section on types, if anything, says the opposite - e.g.

assert (B <: interface {foo(_:C) -> D} ) description "B doesn't have a method foo(_:C)->D"

rather than

assert (B <: interface {foo(_) -> _} ) description "B doesn't have a method foo(Unknown)-> Unknown"

or, as I put it above:

assert (B <: interface {foo(_:C) -> D} ) description "B doesn't have a method foo(Unknown)-> Unknown"

if we're going shallow for now, there needs to be another para in there. The current spec does have the quibble that types apply insofar as Grace has the required type information.

we could put a line in saying Grace implementations only need to check one level of type information. Or something.

Yes, indeed, we need to update the spec. But before the spec can say what a type-check means (dynamically), we need to agree on this amongst ourselves. @kjx, it seems that you are now arguing for what I proposed in my prior comment. Are we all agreed on that?

If we are, then

assert (B <: interface {foo(_:C) → D} ) 
    description "B doesn't have a method foo(Unknown) → Unknown"

ought to be

assert (B <: interface {foo(_:C) → D} ) 
    description "B doesn't have a method foo(_)"

because the more elaborate message implies that B may have some other foo

A related point is the meaning of the static type system. Are we agreed that this is entirely in the hands of the dialect writer? Do we constrain the dialect writer to specify a refinement of the dynamic zero-level structural types? And how do patterns fit into this?

For reference, here is the paper that we used to discuss this issue at the Grace Workshop at SPLASH 2018.

Static and Dynamic Typing In Grace

Andrew P Black, Kim B. Bruce, and James Noble

Abstract

An obviously desirable goal, when mixing static and dynamic typing, is that the static and dynamic checks should do the same thing. We discuss why we cannot achieve this goal in Grace — and indeed in any language in which type information is optional — and consider various compromises.

Introduction

Even when static typing is the norm, type-checks must sometimes be deferred until runtime, when they are performed dynamically. On the surface, it seems obvious that the static and dynamic type checks should do the same thing. This is most easily ensured by using the same type-checking code in both situations. Here is some sample code:

method handleNetworkMessage(socket) {
    def message = socket.getNextMessage
    match (message) 
      case {p: PostMessage -> 
        doPostMessage(p)
    } case {g: GetMessage -> 
        doGetMessage(p)
    } case {d: DirMessage ->
        doDirMessage(d)
    }
}

In the block that follows the first case, message has passed the dynamic check against PostMessage, and is bound to p. We would like this to mean that p actually has type PostMessage.

For the sake of this example, let’s assume that PostMessage is defined as follows:

type PostMessage = interface {
     flags -> Sequence⟦String⟧
     data -> Sequence⟦Number⟧
     isAppend -> Boolean
     sequenceNumber -> Number
}

Let’s further assume that the socket is defined in another module, and we don’t have access to the code that has constructed message. What we do have access to, at runtime, is the actual message object.

The pre-condition for the case block is that PostMessage.matches(message). This is implemented by the pattern PostMessage introspecting on the object message. Because Grace uses structural (rather than nominal) typing, matching a pattern or conforming to a type involves looking at the available methods, and not at the parentage, of the object in question. So we ask: does the message object have methods flags, data, and isAppend? If not, the object can’t match the pattern PostMessage, and we are done.

But, if it does have those three methods, what next? We would also like to check, for example, that the isAppend method returns a Boolean, and that the sequenceNumber method returns a Number. But how can we do that?

The Problem

If the implementation of the message object is fully-annotated with types, and these annotations are preserved in the object itself, then we can indeed implement the same "infinitely deep" recursive type-check that we would have performed statically. In which case, all is right with the world.

However, one of the original design goals for Grace [Black 2010] was that type annotations should always be optional: they might be required by some instructors (using a suitable dialect), but they are never required by core Grace. So let us suppose that the implementation of message is not annotated with types. What now? There seem to be several alternatives

Perform just a shallow (also known as level-1) type-check, looking at the sets of method in the type and the object, but not at their arguments and results.
Perform a shallow type-check, as in option 1, but restrict the language so that the results don’t change if more (or less) type information becomes available.
Perform a variable-depth type-check. First, we perform a level-1 type check; then for those methods whose arguments and results are annotated, we perform a variable-depth type-check on those arguments and results.
Perform type inference on all code, so that full type information is available, even if the programmer chooses not to provide it. With such information, it should be possible to perform an (infinitely) deep dynamic type check.

Perhaps there are other options that we haven’t thought of? We hope so, because none of these seem to be satisfactory.

Is this problem specific to Grace? We don’t think so. It appears to be caused by the confluence of structural (interface) typing, and optional typing. With class types, every object’s type is always fully known, so dynamic type checks can always be precise.

Option 1: Dynamic Type-checks are Shallow

Strictly, Grace does not have dynamic type checks — it has dynamic pattern matching. In one of the more obscure parts of the language, type objects have a dual role. Statically, they are indeed types, and PostMessage, defined above, is an object that contains all of the information in the type declaration. But when used to match an object, a type plays the role of a pattern — essentially a predicate — and the conditions under which that predicate holds may be different from the conditions under which the object conforms to the type. Currently, in minigrace, the Pattern-matching predicate performs a level-1 type check, not a full type check, for the reasons discussed above.

The consequence of this is that, in the case block, the argument must match the type annotation on the parameter, but may not have the type corresponding to that annotation. To be concrete about it, let’s suppose that

type GetMessage = interface {
     flags -> Sequence⟦String⟧
     data -> String
     isAppend -> Boolean
     sequenceNumber -> Number
}

So GetMessage is similar to PostMessage, except that the return type of the data request is String. Suppose that message actually has type GetMessage. Then GetMessage will match it, but so will the pattern PostMessage, and the first branch of the case statement will be executed (because the branches are attempted in sequential order). If doPostMessage (in the first case statement) makes the request p.data, the result might be a String or a Sequence⟦Number⟧.

Perhaps more insidiously, the second branch of the case statement can never be executed, because the patterns in the first and second branches are equivalent, and they are tested in order.

This situation is not very satisfactory. Specifically, it fails the Obviousness test: the above program does not mean what it obviously should mean.

One way to restore at least some measure of the obviousness property is to explicitly distinguish patterns from types. For example, in a pattern-matching block, we could require the programmer to write, instead of

p: PostMessage ->

something like

p: Shallow(PostMessage) ->

where Shallow takes a type as argument and returns a pattern that implements the shallow type-match predicate. But this fails the Gracefulness test..

Option 2: Restricted Shallow Type-Checks

As we have seen, the way that the difference between static dynamic type-checks manifests itself in practice is that the case selected by a match()case()... statement might not be the one that the programmer expects. We might ask: is it possible to restrict match()case()... in some way to prevent this from happening?

As we saw in the initial motivating example, the outcome of a match()case()... might be unexpected if the types used as patterns in two separate branches are similar. For simplicity, suppose that there are two cases, guarded by patterns p1 and p2. In general, there will be objects that conform to p1 & p2, and will thus will be matched by both patterns, but that’s OK; such objects will always match p1, because p1 is tested before p2, and that is the expected behaviour, and it would not change if the static and dynamic checks were identical.

The situation that we would like to avoid is when considering more (that is, deeper) type information changes the match: this is the situation in which the outcome of a deep static check and a shallow dynamic check might differ. We can detect such a situation (assuming that all the patterns are types): what we need to look for is a situation where p1 is a subtype of (or equal to) p2 at level 1, but not a subtype when doing a level 2 (or deeper) type comparison. This is the case where considering more type information could change the outcome, and thus confuse programmers reading the code naively.

Unfortunately, this is quite a strong restriction. It rules out not just our motivating example, in which PostMessage and GetMessage are equivalent at level 1, but also any program with a final case pattern that matches any object, because such a pattern is effectively a supertype of any other type.

Option 3: Dynamic Type-checks are Variable-depth

We can attempt to repair this situation by providing type annotations on the implementation of socket.getNextMessage, carefully distinguishing the situations in which it returns a PostMessage from those in which it returns a GetMessage. Given this extra information, the pattern-matches implemented by the case blocks can go deeper, and distinguish the situations in which message has type PostMessage from those in which it has type GetMessage.

This sounds satisfactory at first glance, but in fact this solution violates Siek and colleagues’ gradual guarantee [2015], which states that removing type annotations does not change the behaviour of a correct programs. While it is OK for type annotations to stop a type-incorrect program from running, and it is also OK for them to stop a type-correct program from running, it is not OK for the annotations to change the run-time behaviour of a program. With this "solution", adding or removing a type annotation in another module would change the behaviour of our program at runtime — it would select a different case branch.

A potential escape route lies in admitting that match(_)case(_)... is part of the reflection interface. While we assert that adding type information to a normal program should not change the program’s dynamic behaviour, this clearly can’t be true for a program that introspects on its implementation, examines the type annotations, and conditionally does one of two different things depending on the value of (or the presence of) that annotation. This same loophole exists for what would otherwise be behaviour-preserving transformations. For example, we expect that changing the name of a local variable will not change a program's behaviour, but if the program introspects on the names of its variables and prints them out, then of course we expect that the change in variable name will change the output.

While forcing programmers to write mirror.match(_) may give us a fig-leaf of respectability to hide behind, this escape route hardly seems satisfactory. The above program would still fail the obviousness test, and in an even more insidious way: the behaviour of the match(_)case(_) would now depend on implementation details that we cannot even see.

Nevertheless, we must recognize that type annotations in the pattern-matching blocks are qualitatively different from annotations on variable declarations or method parameters. While the gradual guarantee might well be expected to hold for the latter — removing a correct type annotation from a declaration should not change a program’s behaviour — it can not be expected to hold for a type in a pattern-matching block, whose semantics is defined by that annotations.

We can perhaps rescue the situation by combining this option with Option 2: restricting the types used as patterns so that they do not overlap at level 1. Adding or removing type information would then have the effect of causing a non-exhaustive match error, but not of changing the case branch executed in a match(_)case(_) statement. This helps only so long as the non-exhaustive match error is a hard error that terminates the program, and not an exception that can be caught.

Option 4: Dynamic Type-checks depend on Type Inference

The fourth option is for the meaning of a pattern match to rely not on programmer-supplied annotations, but on type-inference. Inference might be performed on the compiled code in the object message, or on the source code that builds message; in either case, it is independent of whether the programmer added type annotations to the source code, and this means that we have not violated the gradual guarantee: our program will behave in the same way regardless of whether the programmer adds type annotations or not.

The downside of this option is that the language semantics would now depend on the type inference algorithm. The type-inference algorithm would thus become part of the Grace language specification, and all Grace implementations would have to follow this specification, performing neither more nor less inference than the specification requires.

It’s not clear whether this solution would pass the obviousness test. Type inference algorithms are tricky; it seems unlikely that we could come up with an inference algorithm that would make the choice of branch in the above match()case()... "obvious". Indeed, the inference algorithm that is most easily specified—the inferred type is always Dynamic—reduces Option 4 to Option 1, which we have already seen fails the obviousness test.

Discussion

What we can conclude from this analysis is that Grace has a problem, and one that that requires a clever solution. We hope the language-design community can help us to find it!

We note in passing that the exact semantics of optional typing are largely irrelevant to this problem. Indeed, the above analysis has not discussed the exact meaning of type annotations at all, or whether objects are wrapped at the typed-untyped interface, or what those wrappers do. The problem arises as soon as we make types optional; it seems to be fundamental to optional object typing. Some interpretations of gradual typing do limit our options, though. For example, Chung’s "Optional" semantics [2018] says that all annotations are thrown away before runtime, so would reduce option 3 (variable-depth checks) to option 1 (1-level checks), since there would never be any additional information.

Another take on this problem it is that it is intrinsic to using types to control run-time behaviour. So long as all a type system does is stop a program from being run at all, everything is well. This remains true if the way that the program is stopped is by failing a runtime type check. However, if it is possible to trap that failure (e.g., with an exception handler) and continue execution, or, equivalently, ask whether a runtime-check would fail and branch accordingly, then type annotations are clearly influencing runtime behaviour, and we have violated the gradual guarantee.

Boyland [2014] has previously commented on the issue with Grace’s match statement. Essentially, the match statement requires that we make a true or false decision on a question (type conformance) on which we have incomplete information. If the answer is "maybe", we cannot make the right decision — at least, we cannot do so in the absence of a non-deterministic implementation that takes both branches and abandons the one that later leads to a type error. Jones & Homer [2014] have argued that Gradual Typing is morally incorrect, because of the difficulty of giving a precise meaning to a type annotation. This same objection can perhaps be extended to any kind of optional type annotation.

References

A. Black, K. B. Bruce, and J. Noble. 2010, October. Designing the next educational programming language. In Proceedings ACM international conference on Object oriented programming systems languages and applications companion, SPLASH ’10, pages 201–204, New York, NY, USA..

John Tang Boyland. 2014, October. The problem of structural type tests in a gradual-typed language. In Foundations of Object-Oriented Languages, FOOL..

B. Chung, P. Li, F. Z. Nardelli, and J. Vitek. 2018, July. Kafka: Gradual typing for objects. In T. D. Millstein, editor, 32nd European Conference on Object-Oriented Programming, ECOOP 2018, Amsterdam. Vol 109 of Leibniz International Proceedings in Informatics (LIPIcs), pages 12:1–12:24. Schloss Dagstuhl— Leibniz-Zentrum für Informatik.

Timothy Jones and Michael Homer. 2015, October. Gradual typing is morally incorrect; we’re all monsters now. The 0th Workshop on New Object-Oriented Languages (NOOL-15).

J. G. Siek, M. M. Vitousek, M. Cimini, and J. T. Boyland. 2015, May. Refined Criteria for Gradual Typing. In T. Ball, R. Bodik, S. Krishnamurthi, B. S. Lerner, and G. Morrisett, editors, 1st Summit on Advances in Programming Languages (SNAPL 2015). Vol 32 of Leibniz International Proceedings in Informatics (LIPIcs), pages 274–293, Dagstuhl, Germany,. Schloss Dagstuhl — Leibniz-Zentrum für Informatik.

At the workshop, Tim Jones suggested the following resolution:

The patterns generated by type should continue to do a shallow match
The match(_)...case(_) statement should evaluate all of the guards, and complain if more than one could be true.
We re-introduce an else(_) branch into match(_)...case(_), with the semantics of "the negation of all of the above". This would replace the use of the always-matches pattern Unknown in match(_)...case(_)

I like this suggestion, and propose that we adopt it. I've never liked the "fist match wins" semantics for match, indeed, with that semantics, there is no point in having match, because it is essentially the same as if(_)then(_)elseif(_)...

We would still need to make clear that the meaning of matches(_) on a type is not "has that type", but "looks like it might have that type, at the top level".

Changing the semantics of match(_)case(_)... should be quite easy.

Dijkstra would be pleased! (actiually he'd be most please without the else) But it makes things harder to program.

but really the two (three?) issues are orthogonal:

1. match/case semantics
type/match semantics
- 1. shallow ("transient") vs "deep" (behavioural) vs "concrete"
- 1. the meaning of matches(_) on a type is not "has that type", but "looks like it might have that type, at the top level".

I think I agree with 3. not sure about the other two.

Re: 2 Tim also pointed out that going back to the DLS monadic match design, that question could be left to libraries

actually re 1, that pretty much can be as well.

James, who should be desperately hacking slides inan attempt to avoid embarassment in three hours time. and yes, I KNOW I've had months to do this...

On 6/11/2018, at 6:00AM, Andrew Black notifications@github.com wrote:

At the workshop, Tim Jones suggested the following resolution:

• The patterns generated by type should continue to do a shallow match • The match()...case() statement should evaluate all of the guards, and complain if more than one could be true. • We re-introduce an else() branch into match()...case(), with the semantics of "the negation of all of the above". This would replace the use of the always-matches pattern Unknown in match()...case() I like this suggestion, and propose that we adopt it. I've never liked the "fist match wins" semantics for match, indeed, with that semantics, there is no point in having match, because it is essentially the same as if()then()elseif()...

We would still need to make clear that the meaning of matches(_) on a type is not "has that type", but "looks like it might have that type, at the top level".

Changing the semantics of match()case()... should be quite easy.

— You are receiving this because you were mentioned. Reply to this email directly, view it on GitHub, or mute the thread.

One form of match(_)case_(_) that won't work under this proposed semantics is one that says:

match (anObject) 
  case { b:B ->  // action when anObject is a B
} case { a:A -> // action when anObject is an A
} ...

when B <: A. In this case we would expect both B and A to match anObject, but want the "most precise" match, i.e., B.

I don't see this as a big problem, because one can write

match (anObject) 
  case { a:A -> 
     if (B.matches(a)) then {   
        // action when anObject is a B
     } else {                          
        // action when anObject is an A
     }
} ...

As I said, I don't see this as a big problem, but I hardly use match(_)case(_). Presumably we could also define not on Patterns, and write

match (anObject) 
  case { b:B ->  // action when anObject is a B
} case { a:(A & B.not) -> // action when anObject is an A
} ...

One form of match()case(_) that won't work under this proposed semantics is one that says: ...

match (anObject) case { b:B -> // action when anObject is a B } case { a:A & (B.not) -> // action when anObject is an A } ...

will this is what Dijkstra would prefer, but I can also see good reasons for not doing it this way.

but it should all be library stuff, right?

James

but it should all be library stuff, right?

The meaning of match(_)...case(_) is just library stuff. The meaning of the object created by the interface syntax is part of the core language.

Hmm I recall Tijs? at Boston saying that we "virtualised" control structures and should also virtualise objects - and if we could do that, we could do types too. Object and Interface would somehow loop back through the library I presume. Hmm: would we have to do that to blocks too?

This is an interesting idea. I've been amused in the past when pretty smart Haskell-type people couldn't get their heads around the idea that an OO language doesn't need any "primitive" objects: we can define Boolean and Pair out of whole cloth, and thus can (in principle) define numbers as sequences of Booleans.

That said, I can't get my head around the idea of virtualising objects themselves ...

Ah, someone should follow up with Tijs I guess. I seem to recall this was based on my bad (BETA-like??) idea that object would be some kind of meta-operator that took a block and turned it into an object...

Ah, someone should follow up with Tijs I guess.

Yes, but not as part of this issue!

I think that where we are now is that

the meaning of a Dynamic Interface is a set of method names, with argument and result types as written, and
such an interface matches an object with a superset of the method names.

What is still open is whether or not the declared types of the method in the object must also match.

The "obviousness" rules says that they should matter, but the obviousness rule also says that we should do inference in this case. For example, if we have

type i = interface { size -> Number }

and

def o = object {
    method size { "small" }
}

then it is "obvious" that i.matches(o) is false, because the size method in o obviously answers a String, not a Number.

I think that we have reached a reasonable compromise on the semantics of match(_)case(_)…: that it should check all of the case guards at one time, and complain if more than one holds. It should also complain if none holds, unless there is an else(_) branch, which we should reinstate.

I don't know what the "obviousness" rule is. A rule based on declared types would work be fine, is explicable, although it might be rather confusing when types aren't declared. (I can't even remember if the spec says types are inferred for 'defs' these days).

I thought we were doing some type inference through blocks at least...

I’d prefer for declared types to matter, but ignore inference. In my way of thinking, type inference is a tool for suggesting declarations that the programmer can accept or reject — i.e., it is a preprocessing step that the programmer can accept or reject. If they accept it, the annotation is explicitly inserted into the code.

Kim

On Dec 12, 2018, at 7:17 AM, Andrew Black notifications@github.com wrote:

Ah, someone should follow up with Tijs I guess.

Yes, but not as part of this issue!

I think that where we are now is that

the meaning of a Dynamic Interface is a set of method names, with argument and result types as written, and such an interface matches an object with a superset of the method names. What is still open is whether or not the declared types of the method in the object must also match.

The "obviousness" rules says that they should matter, but the obviousness rule also says that we should do inference in this case. For example, if we have

type i = interface { size -> Number } and

def o = object { method size { "small" } } then it is "obvious" that i.matches(o) is false, because the size method in o obviously answers a String, not a Number.

I think that we have reached a reasonable compromise on the semantics of match()case()…: that it should check all of the case guards at one time, and complain if more than one holds. It should also complain if none holds, unless there is an else(_) branch, which we should reinstate.

— You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub https://github.com/gracelang/language/issues/168#issuecomment-446623861, or mute the thread https://github.com/notifications/unsubscribe-auth/ABuh-udkn3vNMBqa0UjVZgMeI7hLDV4nks5u4R4EgaJpZM4U43iz.

I don't know what the "obviousness" rule is.

It was one of our rules of language design: a construct should means what it obviously appears to mean. Or, may it was that every construct should have an obvious meaning. The problems focus, is that what is obvious is in the eye of the beholder.

In Kim's example, with the code

def o = object {
    method size { "small" }
}

the inference tool would suggest inserting method size -> String, and the programmer would say "OK", since this is obviously what the code does. As a result, i would no longer match o.

The spec (in commit c8fd59edf34) says that exactly one case must match, unless there is an else, in which case none may match.

gracelang / language

Semantics of (Dynamic) Types #168