EK9 in Depth

The Payoffs: Liskov and Hoare

The Evidence, at the end of Volume 1, said that "two names sit behind the whole language, and the second volume returns to them": Hoare's null mistake, and the Liskov Substitution Principle. You have now met every mechanism that serves them, one at a time and under other names: a tri-state value and a checked get(), a pure that an override must keep, one sameness per type, a type that is closed unless it says otherwise, a dispatcher where another language writes a cast. This chapter does not teach anything new. It says what the mechanisms were for, shows the compiler refusing each way of breaking the promise, and then says exactly how much of each promise is checked today, which is not the same for the two names.

Both problems are ones every language has, and the usual answer to both is a rule that a reviewer is expected to remember. EK9's answer is to make the betrayal impossible to write where it can, and to say so where it cannot yet.

Substitution, as the compiler checks it

Barbara Liskov's principle (1987, and with Jeannette Wing as a behavioural definition in 1994) says that a subtype must be usable wherever its parent is, without the caller being able to tell. A caller written against Shape may rely on whatever Shape promises, and every subtype must keep those promises, not only the ones the type checker happens to see. The principle has no enforcement in most languages; it is advice. You have probably met its breaches in Java: a List.of(...) whose add throws, an equals that disagrees with hashCode, an instanceof ladder that has to be extended for every new subclass, an override that was meant to replace a method and did not because the signature drifted. This is the working case, a Shape hierarchy whose callers hold the parent type:

#!ek9
defines module book.payoffs.shapes

  defines class

    Shape as abstract
      area() as pure abstract
        <- rtn as Float?

    Square extends Shape
      side <- Float()

      Square()
        -> side as Float
        this.side: side

      override area() as pure
        <- rtn as Float: side * side

      override operator ? as pure
        <- rtn as Boolean: side?

    Rectangle extends Shape
      width <- Float()
      height <- Float()

      Rectangle()
        ->
          width as Float
          height as Float

        this.width: width
        this.height: height

      override area() as pure
        <- rtn as Float: width * height

      override operator ? as pure
        <- rtn as Boolean: width? and height?

  defines function

    describe() as pure
      -> shape as Shape
      <- rtn as String: `area ${shape.area()}`

  defines program

    Substitution()
      stdout <- Stdout()
      shapes <- List() of Shape
      shapes += Square(3.0)
      shapes += Rectangle(2.0, 5.0)
      for shape in shapes
        stdout.println(describe(shape))

area 9.0
area 10.0

describe knows nothing of Square or Rectangle, and area() is declared pure on Shape, so a caller can rely on it being a query. The rest of this section is the list of ways a subtype could betray that, and what the compiler does about each. None of the examples that follow is an experiment in being clever. Each is the natural thing to write, and each is refused.

An override may not change the purity contract. The parent promised area() is a query. A subtype whose version assigns state, or one that adds pure where the parent did not, would make the same call mean different things depending on the object behind it.

Shape as open
  area() as pure
    <- rtn as Float: 0.0

Circle extends Shape
  radius <- Float()

  Circle()
    -> radius as Float
    this.radius: radius

  override area()
    <- rtn as Float: radius * radius

  override operator ? as pure
    <- rtn as Boolean: radius?

EK9     : Error   : E05150: 'area' on line 17 position 15: 'override public Float <- area()' and 'public Float <- area()' on line 7 in 'overrideDropsPure.ek9': 'pure' in super requires 'pure' for this definition
             See: ek9 -h E05150
           forAI: purityRules

The compiler's own explanation of the rule (ek9 -h E05150) is in Liskov's terms: a child that is substituted for its parent must uphold the contract the parent declared, and breaking purity would violate behavioural substitution. It runs the other way too. An override may not add pure to a parent that was not pure (E05160); the contract is the parent's, in both directions.

A subtype that adds state must say what equality means now. An Account is equal to another by id. A NamedAccount adds an owner. If it silently inherits == and $, two accounts that differ only in owner compare equal and print alike, and the parent's comparison has been inherited by a type it cannot see into.

Account as open
  id <- Integer()

  Account()
    -> id as Integer
    this.id: id

  default operator ?
  default operator $
  default operator ==

NamedAccount extends Account
  owner <- String()

  NamedAccount()
    ->
      id as Integer
      owner as String

    super(id)
    this.owner: owner

  default operator ?

EK9     : Error   : E07238: 'NamedAccount' on line 17 position 4: 'NamedAccount' has 1 field(s) of its own but would inherit '$' from 'Account', '==' from 'Account', '#?' from 'Account' - declare 'default operator $', 'default operator ==', which also gives '#?' - or the bare 'default operator' for all of them (or write the operator): a type that adds fields, concrete or abstract, must declare its own '$', '$$' and ':=:', and its own sameness ('<=>' or '==', with '#?'), where it would inherit one: the inherited operator was written for the super's fields and cannot know these - use 'default operator' for each (or the bare 'default operator') or write one
             See: ek9 -h E07238

The message names the operators the subtype would have inherited and the one-line cure for each. The same rule applies to an abstract type that adds fields. That is the point of the one-sameness model in Operators and Pragmatic Purity, in Full: a type has exactly one of <=> and ==, the other comparisons are generated from it, and a hand-written pair that could disagree (Java's equals against compareTo) cannot be written.

An ordering written for a hierarchy is not the subtype's to change. When an abstract base writes <=> by hand, the whole family is ordered one way. A Circle that orders itself differently, even by asking for a generated comparison of its own, breaks transitivity once different kinds of shape are mixed: one circle sorts before a shape, the shape before another circle, and the two circles do not sort that way, so a sort depends on the order of its input. ek9 -h E07182 states the argument and cites Bloch's item on equals in Effective Java.

Shape as abstract
  area() as pure abstract
    <- rtn as Float?

  operator <=> as pure
    -> other as Shape
    <- rtn as Integer: area() <=> other.area()

  operator #? as pure
    <- rtn as Integer: #?area()

Circle extends Shape
  radius <- Float()

  Circle()
    -> radius as Float
    this.radius: radius

  override area() as pure
    <- rtn as Float: PI * radius * radius

  default operator <=>

  default operator ?

EK9     : Error   : E07182: '<=>' on line 30 position 23: 'Circle' inherits '<=>' from 'Shape', whose sameness is hierarchy-wide: sameness ('<=>' or '==') written by hand on an abstract base or a trait is hierarchy-wide sameness; a subtype inherits it and cannot redefine it
             See: ek9 -h E07182

Replacement is explicit in both directions. An override must say override; a member that overrides nothing must not. A subtype method that matches the parent's by name and signature without the keyword, and one marked override with no parent version, are both errors, and the second is how a parent whose signature changed fails loudly in its children and not quietly:

Shape as open
  describe()
    <- rtn as String: "a shape"

Circle extends Shape
  describe()
    <- rtn as String: "a circle"

  override radius()
    <- rtn as Float: 1.0

EK9     : Error   : E05120: 'describe' on line 11 position 6: 'override' required on 'public String <- describe()' in 'Circle' (add it to THIS member only - a member with no parent version must not carry 'override', E05110) as it overrides method of same name/signature in hierarchy
             See: ek9 -h E05120
EK9     : Error   : E05110: 'radius' on line 14 position 15: 'radius' has no parent version - remove 'override' from THIS member only (members that do override a parent, such as 'operator ?', keep it): does not 'override' any method/operator
             See: ek9 -h E05110

You cannot extend what was not opened. A class is closed unless it is declared as open, so substitution is a decision the author of the base type makes, and not something any caller can force by subclassing:

EK9     : Error   : E05030: 'Account' on line 15 position 20: not open to be extended
             See: ek9 -h E05030
           forAI: closedByDefault

There is no cast and no run-time type test. The remaining betrayal is outside the type system altogether: code that asks an object what it really is, and branches. EK9's grammar has neither a type test nor a cast, so the parser refuses both, and behaviour that depends on the run-time type lives in a dispatcher (The Dispatcher), where the compiler checks the whole set of handlers. A type test written as a condition, and a cast written with as:

Syntax  : 'Circle' on line 19 position 18: unexpected 'Circle' expecting 'empty', 'of', '(', '.', '?', ':', 'not', 'in', '::', ':~:', ':=' or '=' 

Syntax  : 'as' on line 19 position 22: mismatched input 'as' expecting ';' or newline 

Both are syntax errors: there is no rule saying "do not cast", because there is no way to say it. A ClassCastException has no spelling. Two rules from earlier chapters belong in the same list and are not repeated here: a query operator such as $ must be pure and a mutating one must not be, so a subtype cannot make + change its operand (E07500 and E07510, in Operators and Pragmatic Purity, in Full), and an immutable collection is not a subtype that throws, because there is no immutable collection (the same chapter's design note).

A design note. I closed types by default because inheritance is a promise the author of the base class has to be able to keep, and an author cannot keep a promise to subclasses that do not exist yet. Java's open ArrayList is the example I would point at: a class that nobody meant to be a base, extended by programs that now depend on its internals. The answer is delegation, and traits with by make it as easy as inheritance. A class declared with trait of View by inner has every method of View forwarded to inner without writing one; it overrides only the methods it means to change, as a subclass would, and what it holds stays the type that was tested. - Steve

Where substitution stops

The compiler checks the shape of the contract, and not its content. It knows an override kept pure, restated its sameness, and said override. It cannot know that area() returns an area: a Rectangle whose area() returns the perimeter compiles, is pure, and breaks every caller. Preconditions and postconditions, the part of Liskov and Wing that is about meaning, are still require, assert and tests (Testing the Compiler Trusts). What the structure does is shrink the set of ways a subtype can betray its parent to the ones that need a human to have written the wrong value, and remove the ones that only needed a human to have forgotten a keyword.

The null mistake

Tony Hoare introduced the null reference in 1965 and called it, in 2009, his billion-dollar mistake. The mistake is not the absence of a value; every program has to model that. It is that absence arrives as a value of the ordinary type, so the type checker says nothing, and the program fails far from where the absence was introduced. EK9's answer has three parts, and each is a chapter you have read.

There is no way to write one. null is not a keyword, and a program that tries is refused:

NullProbe()
  stdout <- Stdout()
  name as String: null
  stdout.println(name)

EK9     : Error   : E01073: 'null' on line 8 position 22: 'null' does not exist in EK9 - use tri-state semantics (unset/set) with '?' operator
             See: ek9 -h E01073
           forAI: excludedFeatures.null

The message names the replacement. A value is absent, present but unset, or present and set, and the program tests the second and third with ?. Integer() and String() are unset: real objects that answer the question and propagate unset through arithmetic. The removed null-coalescing token is refused with its own code, E01096, whose message points at ?: and :=?; it tested for an absence that EK9 is designed not to let a program see.

The tri-state operators do what they say. :=? assigns only when the target is unset, so it never overwrites a real value; ?: supplies a fallback when its left is unset:

AssignIfUnset()
  stdout <- Stdout()
  name <- nameOf(true)
  name :=? FALLBACK_NAME
  stdout.println(`a set name stays [${name}]`)
  missing <- nameOf(false)
  missing :=? FALLBACK_NAME
  stdout.println(`an unset name becomes [${missing}]`)

a set name stays [Ada]
an unset name becomes [anon]

Fallback()
  stdout <- Stdout()
  unknown <- numberOf(false)
  chosen <- unknown ?: OFFSET
  stdout.println(`unset or ${OFFSET} gives ${chosen}, set? ${chosen?}`)
  known <- numberOf(true)
  kept <- known ?: OFFSET
  stdout.println(`set or ${OFFSET} gives ${kept}, set? ${kept?}`)

unset or 5 gives 5, set? true
set or 5 gives 42, set? true

What cannot be set is checked at the read. The one place a value can be missing is a declaration that says so, x as T?, which is a slot with nothing in it yet. The compiler's job is to prove the slot is never read before it is written:

EmptySlot()
  stdout <- Stdout()
  name as String?
  stdout.println(name)

EK9     : Error   : E08020: 'name' on line 9 position 21: 'name as String': might be used before being initialised
             See: ek9 -h E08020

The check is a whitelist, not a search for known bad shapes. A test in the compiler's own suite lists every position in the grammar where a name can be read, and fails the build if any is unclassified or has no checking rule behind it; one shared check, behind E08020, covers the reads of local names. Optional and Result add E08030 on top, for a get() or an ok() outside a block whose check proved it.

The cost of tri-state

You cannot ask an unset value to fail, and it will not. An unset operand makes an arithmetic result unset, quietly, and that is the defined behaviour, not an accident. The price is that it can go unnoticed. Here an unset number takes part in a sum, and the program asks to print it three ways:

UnsetFlows()
  stdout <- Stdout()
  unknown <- numberOf(false)
  total <- unknown + OFFSET
  stdout.println(`total is [${total}]`)
  stdout.println(`total set? ${total?}`)
  stdout.println($total)
  stdout.println("after the unset lines")

total set? false
after the unset lines

Two of the four lines are missing. An interpolated string that holds an unset value is itself unset, and printing an unset String prints nothing, neither a blank line nor []. Only ${total?} shows it. That is the cost of the model: where Java would have thrown an exception at the first use of the missing value, EK9 carries the unset through and says nothing until you ask with ? or a guard. The guard is the cure, because it makes you ask where the value arrives (Guards and Safe Code), but the language does not make you.

What is claimed, and what is not yet proven

For absence, the sentence that can be said today is this: EK9 is designed so that absence is unobservable; the compiler checks every read; the proof is in progress. Each of the three clauses is narrower than it sounds.

Designed so that is a statement about design intent and about a work list that has no known open item: no route to a value-less slot is known to be open, and the document that records the investigation says plainly that the guarantee is not yet a theorem. The compiler checks every read is the whitelist above, and it is built. The proof is in progress means that the layers that would turn "no counterexample found" into a theorem are not built: a check, in the middle of the compiler, that every load in the generated intermediate form is preceded by a store on every path; a check over the runtime library, at build time, that none of its operations can return an absent value; a generator that fuzzes programs specifically to provoke an absent value; and the written proof over all of them. Third-party code, once it can be called from EK9 (it cannot be today), will sit outside the guarantee and its results will be checked at the boundary.

There is also a switch for the cautious. Running a compiled program with the Java property ek9.absent.strict set to true turns an observed absence into a panic that names the place, instead of a quiet wrong answer. It is off by default, and a cached build has to be cleaned before it takes effect.

That is the most the evidence supports, and it is why this book has said designed so that every time. When the remaining layers exist and the corpus runs clean under the strict switch, the sentence changes. Until then, what you can rely on is what the compiler does: a read it cannot prove legal is an error, with a code and a line.

The cost

You cannot reach for the shortcut. There is no null to return when you do not know, no cast to get past a type you could not prove, no override that quietly differs, and no way to loosen a limit on the afternoon it is wrong. Each refusal is a place where another language would have let you finish and left the consequence for a later reader or a later run. In EK9 the consequence arrives as a compile error, sooner and in your hands, which is a real cost when the thing you refused was right.

What it buys is the ability to read a program and know what a call may do. A call through a parent type keeps the parent's purity and the parent's equality. A value is either set or you were made to ask. A name that can be read has been checked. Those are narrower than "the program is correct", and the two problems this chapter names are narrower still: a subtype can still return a wrong value, and the proof about absence is not finished. The preface asked of every rule whether it removes a category of failure or merely discourages it. This volume has shown where the answer is removal, where the compiler checks it, and where the work is still in progress.

For the research behind each rule, and for Hoare's own account, see The Evidence.