Checked refinements

Declare a type whose values are proven to pass a check, get values into it three ways, and use what the proof buys.

A checked refinement is a type made of a base type and a predicate, a condition every value of the type is proven to meet. A value is proven when it is written down, when an if or a match has checked it, or when it already has the refined type. The compiler refuses any other value. In return, an operation that had to allow for the bad value no longer does. The library’s NonZeroInteger is Integer where @::isNot(0), and dividing by one returns a Rational, not an Optional. The nearest TypeScript idea is a branded type, but here the compiler derives the type guard from the predicate.

implementation {
	type NonZero = Integer where @::isNot(0)

	function perGuest(_ total: Integer, _ guests: NonZero) -> Rational {
		<- total::divide(by guests)
	}

	function split(_ total: Integer, among guests: Integer) -> Rational {
		if guests::isNot(0) {
			<- perGuest(total, guests)
		}

		<- 0/1
	}

	Terminal.print(perGuest(12, 4)) § 3
	Terminal.print(split(12, among 5)) § 12/5
	Terminal.print(split(12, among 0)) § 0
}

type NonZero = Integer where @::isNot(0) declares a refinement. The type before where is the base. The call after it is the predicate, and @ stands for the value being refined. Read the line as “an Integer for which isNot(0) returns true”.

Inside perGuest, guests is proven not to be zero, so the division cannot fail. divide(by:) returns an Optional<Rational> for an Integer divisor, and a plain Rational for a proven one. The call perGuest(12, 4) compiles because a written 4 is its own proof. split receives an Integer that nobody has checked, and the if proves the predicate inside its branch. You still make the check once, in the if, and the division in perGuest has no Optional to unwrap.

0/1 is the Rational zero. <- 0 would be refused as return-type-mismatch: the function returns a Rational, and 0 is an Integer.

Compared with JavaScript.

type NonZero = number & { readonly __brand: "NonZero" }

function isNonZero(n: number): n is NonZero {
  return n !== 0
}

function perGuest(total: number, guests: NonZero): number {
  return total / guests
}

function split(total: number, guests: number): number {
  if (isNonZero(guests)) {
    return perGuest(total, guests)
  }
  return 0
}

perGuest(12, 4 as NonZero)

A branded type needs a type guard you write yourself, and TypeScript trusts the guard: if isNonZero returned true for 0, nothing would notice. A literal needs a cast. In Essence the where clause is the guard, and a written value is checked while compiling. The refinement erases, so at runtime a NonZero is an ordinary integer. If you validate with Zod, the nearest thing is .refine(…).brand(): your if still runs the check at runtime, and the compiler refuses any value that skipped it. More on Coming from JavaScript › Types.

Declaring a refinement

implementation {
	type Digit = Integer where @::isBetween(0, and 9)
	type Discount = Rational where @::isGreaterThan(0)::and(@::isLessThan(1))
	type Answer = String where @::is("yes")
	type GuestList = List<String> where @::hasItems()

	constant digit: Digit       = 7
	constant discount: Discount = 1/4
	constant answer: Answer     = "yes"
	constant guests: GuestList  = ["Ada", "Grace"]

	Terminal.print(digit) § 7
	Terminal.print(discount) § 1/4
	Terminal.print(answer) § yes
	Terminal.print(guests::firstItem()) § Ada
}

A refinement is a type alias with a where clause: type Name = Base where predicate. Five bases can be refined:

• Integer
• Rational
• String
• an applied List, one with its item type written, such as List<String>, never a bare List
• an applied Dictionary, such as Dictionary<String, Integer>, shown on Dictionaries

The first four appear above. firstItem() on guests prints Ada, not Value("Ada"): GuestList proves the list has items, so there is no Optional to unwrap.

Every other base is refused as invalid-refinement-predicate. That covers a Boolean, a record, an Optional, a bare List, and a refinement of another refinement:

[invalid-refinement-predicate]
Error: A 'where' clause can not refine NonEmptyString
   ╭─┤ initial.es:2:17 │
   │
 2 │     type Initial = NonEmptyString where @::isOneCharacter()
   │                    ───────┬──────  
   │                           ╰──────── this is NonEmptyString
   │ 
   │ Help: Drop the 'where' clause from 'Initial'.
   │ 
   │ Note: A checked refinement is written on an Integer, a Rational, a String, an applied List or an applied Dictionary — 'List<String>', never a bare 'List'.
───╯

Write the predicate on the base instead: String where @::hasCharacters()::and(@::isOneCharacter()) compiles.

A refinement can take a type parameter, as in type NonEmpty<Item> = List<Item> where @::hasItems(). The library’s NonEmptyList is declared this way, and declaring your own is on Generics.

What the predicate may say

The predicate is one method call on @, and its arguments are written values: an Integer, a Rational, a String or a Boolean. Several calls join with ::and(…), as Discount does above. A name in argument position is refused, even the name of a constant:

[invalid-refinement-predicate]
Error: This is not a predicate a refinement can be checked by
   ╭─┤ party.es:4:56 │
   │
 4 │     type PartySize = Integer where @::isLessThanOrEqualTo(largestTable)
   │                                                           ──────┬─────  
   │                                                                 ╰─────── this is not a literal value
   │ 
   │ Help: Pass a written Integer, Rational, String or Boolean.
   │ 
   │ Note: A predicate is one Method call on '@' with literal Arguments, or several of them joined with '::and(…)'.
───╯

Written arguments are what let the compiler tell when two refinements prove the same thing.

The receiver of a call is the value before ::. Three more shapes get the same error, labelled this is not '@'. They are a receiver other than @ (5::isOdd()), a chained receiver (@::trim()::hasCharacters()), and ::or(…) in place of ::and(…). A predicate that returns something other than a Boolean, such as @::absolute(), is predicate-not-boolean.

A predicate can also call a method your program declares, such as @::isAtLeast(18). Namespaces and methods covers declaring one, and which method bodies let a written value pass.

The ten refinements in the library

Every program can use these ten without an import.

What counts as one character is on Strings. Which list methods keep the NonEmptyList proof, and which lose it, is on Lists.

Refinements are compared by what they prove

implementation {
	type NonZero = Integer where @::isNot(0)
	type SmallOdd = Integer where @::isOdd()::and(@::isLessThan(10))
	type OddAndSmall = Integer where @::isLessThan(10)::and(@::isOdd())
	type Odd = Integer where @::isOdd()

	function tripled(_ n: SmallOdd) -> Integer {
		<- n::multiply(with 3)
	}

	constant four: NonZero = 4
	constant fromLibrary: NonZeroInteger = four

	constant seven: OddAndSmall = 7
	constant odd: Odd           = seven

	Terminal.print(12::quotient(dividingBy four)) § 3
	Terminal.print(fromLibrary) § 4
	Terminal.print(tripled(seven)) § 21
	Terminal.print(odd) § 7
}

Two refinements are one type when they prove the same thing of the same base. NonZero is NonZeroInteger under another name. four is accepted as a NonZeroInteger, and quotient(dividingBy:) returns a plain Integer for it.

The order of the calls in an ::and(…) chain does not matter: SmallOdd and OddAndSmall are one type. A chain proves each call in it, so seven, proven odd and less than 10, is accepted as an Odd, which requires only one of them.

The library’s refinements also imply each other. A PositiveInteger is accepted wherever a NonZeroInteger or a NonNegativeInteger is wanted, and a PositiveRational works the same way for the two rational refinements. A refined value has every method its base has, and it is accepted wherever its base is:

implementation {
	function perGuest(_ total: Integer, _ guests: NonZeroInteger) -> Rational {
		<- total::divide(by guests)
	}

	function seatsLeft(_ seats: NonNegativeInteger) -> String {
		<- "{seats} seats left"
	}

	function doubled(_ count: Integer) -> Integer {
		<- count::multiply(with 2)
	}

	constant tableSize: PositiveInteger = 6

	Terminal.print(perGuest(60, tableSize)) § 10
	Terminal.print(seatsLeft(tableSize)) § 6 seats left
	Terminal.print(doubled(tableSize)) § 12
	Terminal.print(tableSize::isEven()) § true
}

tableSize goes into all three functions. isEven() is an Integer method, and a PositiveInteger has it too.

Getting a value in

Leave the if out of split from the top of the page, and the call to perGuest no longer compiles. The error is argument-type-mismatch:

[argument-type-mismatch]
Error: This Argument does not fit Parameter 2
   ╭─┤ split.es:9:22 │
   │
 9 │        <- perGuest(total, guests)
   │                           ───┬──  
   │                              ╰──── this is an Integer
   │ 
   │ Help: Check '@::isNot(0)' on the value in an 'if' or a 'match', or pass a value that already has Type 'NonZero'.
   │ 
   │ Note 1: Parameter 2 is NonZero.
   │ Note 2: Every value of 'NonZero' has been proven to answer '@::isNot(0)'.
───╯

The Help names both ways in: check the predicate on the value in an if or a match, or pass a value that already has the type. A written value already has it.

A value of another type entirely gets no such Help, since no check would make it fit. 0 passed where a Rational where @::isLessThan(1/2) is expected is an Integer, and the Note says the refinement takes a Rational before the predicate is asked.

A written value is its own proof

implementation {
	constant share: Rational    = 12::divide(by 4)
	constant initial: Character = "essence"::firstCharacter()
	constant first: String      = ["a", "b"]::firstItem()

	Terminal.print(share) § 3
	Terminal.print(initial) § e
	Terminal.print(first) § a
	Terminal.print(9::squareRoot()) § 3
}

A written value, or literal, is checked while compiling. It counts as proof wherever it stands: as a constant’s value, as an argument, as a returned value, and as the receiver of a method call. 4 is not zero, so 12::divide(by 4) returns a Rational. "essence" has characters, so firstCharacter() returns a Character. ["a", "b"] has items, so firstItem() returns a String. 9 is not negative, so squareRoot() prints 3, not Value(3). Each annotation above would be refused if its call returned an Optional.

The proof belongs to the written value, not to a name. A constant bound to a literal without a type annotation holds the base type, and the proof is lost:

implementation {
	constant nine   = 9
	constant scores = [1, 2]
	constant proven: NonEmptyList<Integer> = [1, 2]

	Terminal.print(nine::squareRoot()) § Value(3)
	Terminal.print(scores::firstItem()) § Value(1)
	Terminal.print(proven::firstItem()) § 1
}

nine is an Integer and scores is a List<Integer>, so both calls return an Optional. Annotate the constant with the refinement, as proven does, and the literal proves it once, at the annotation. A constant bound to a call keeps the type the call returns: constant share = 12::divide(by 4) is a NonZeroRational, so share::reciprocal() prints 1/3.

Compared with JavaScript.

const nine = 9                               // type: 9
const scores = [1, 2]                        // type: number[]
const proven: [number, ...number[]] = [1, 2]

scores[0]                                    // number | undefined, under noUncheckedIndexedAccess
proven[0]                                    // number

TypeScript keeps the literal type of const nine = 9, but widens [1, 2] to number[] unless you write a non-empty tuple type. Essence widens both: an unannotated constant holds the base type. More on Coming from JavaScript › Types.

An if or a define proves its condition

implementation {
	function exclaimed(_ text: NonEmptyString) -> String {
		<- text::append("!")
	}

	function shout(_ text: String) -> String {
		if text::isEmpty() {
			<- "…"
		} else {
			<- exclaimed(text)
		}
	}

	function shareOf(_ total: Integer, over count: Integer) -> Rational {
		<- define {
			as total::divide(by count) if count::isNot(0)
			as 0/1 otherwise
		}
	}

	function shared(_ total: Integer, over count: Integer) -> Rational {
		<- define {
			as 0/1 if count::isZero()
			as total::divide(by count) otherwise
		}
	}

	Terminal.print(shout("essence")) § essence!
	Terminal.print(shout("")) § …
	Terminal.print(shareOf(12, over 4)) § 3
	Terminal.print(shared(12, over 5)) § 12/5
	Terminal.print(shared(12, over 0)) § 0
}

An if whose condition checks a refinement’s predicate narrows the constant or parameter it checks: inside the branch, the name has the refined type. split at the top of the page works this way.

The else branch narrows by the complement, the predicate that holds when the condition is false. isEmpty() returning false means hasCharacters() is true, so in the else of shout, text is a NonEmptyString. An else if chain narrows the same way, one condition at a time.

A define arm, one as … line, reads the same way. Its own condition holds for its value, and the complement of every condition above it holds too. In shareOf, count is a NonZeroInteger in the arm that checks count::isNot(0). In shared, the otherwise arm is reached only when count::isZero() returned false. So count is a NonZeroInteger there, and divide(by:) returns a Rational.

A constant bound to the narrowed name inside the branch keeps the proof: inside if count::isNot(0), constant proven = count is a NonZeroInteger. The proof ends with the branch. An early return does not narrow the lines after it. Write a function share that returns 0/1 early when guests::isZero(), then returns total::divide(by guests). The division still returns an Optional, so that return is refused:

[return-type-mismatch]
Error: This value does not fit the declared return Type
   ╭─┤ share.es:7:6 │
   │
 7 │        <- total::divide(by guests)
   │           ────────────┬───────────  
   │                       ╰───────────── this is an Optional<Rational>
   │ 
   │ Note: The Function returns Rational.
───╯

Move the work into the branch, or write a define like shared.

Compared with JavaScript.

function share(total: number, guests: number): number {
  if (!isNonZero(guests)) {
    return 0
  }
  return perGuest(total, guests)
}

TypeScript narrows guests after the early return, and it narrows a let the same way. Essence narrows a constant or a parameter inside the branch that checked it, and nowhere else. More on Coming from JavaScript › Types.

A variable is never narrowed. if guests::isNot(0) compiles, and passing guests to perGuest inside it is the same argument-type-mismatch as above. Its Help suggests the if you already wrote. Bind the variable to a constant, and check the constant:

implementation {
	function perGuest(_ total: Integer, _ guests: NonZeroInteger) -> Rational {
		<- total::divide(by guests)
	}

	variable guests = 3

	guests = guests::add(1)

	constant current = guests

	if current::isNot(0) {
		Terminal.print(perGuest(12, current)) § 3
	}
}

An if on a union does not narrow either. After if value::isEmpty() on a String | List<String>, the else branch still holds a String | List<String>, and a case String there gets a plain String, not a NonEmptyString.

A match proves its cases

implementation {
	function inverse(_ n: Integer) -> Rational {
		<- match n -> Rational {
			case 0 { <- 0/1 }
			case _ { <- 1::divide(by @) }
		}
	}

	function perHead(_ total: Integer, _ size: Optional<Integer>) -> Rational {
		<- match size -> Rational {
			case #Value(count) where count::isNot(0) {
				<- total::divide(by count)
			}
			case _ { <- total::toRational() }
		}
	}

	Terminal.print(inverse(4)) § 1/4
	Terminal.print(inverse(0)) § 0
	Terminal.print(perHead(12, #Value(4))) § 3
	Terminal.print(perHead(12, #Value(0))) § 12
	Terminal.print(perHead(12, #Empty)) § 12
}

Inside a match case, @ is the matched value. A match on an Integer tries its cases in order, and its cases are proof. case 0 proves @::is(0). The case _ below it is reached only by a value that is not 0, so there @ is a NonZeroInteger, and 1::divide(by @) returns a Rational. A guard, a where condition written after a case, proves its condition for its own case: in perHead, count is a NonZeroInteger inside the first case.

The same shape on a String proves less. Below case "", case _ does not prove NonEmptyString, and @::firstCharacter() there still returns an Optional. Check isEmpty() in an if, as shout does.

A refinement cannot be a matcher, the type or value written after case. case NonZeroInteger is refinement-as-matcher, because the predicate erases before the program runs:

[refinement-as-matcher]
Error: A Matcher can not test for 'NonZeroInteger'
   ╭─┤ described.es:4:9 │
   │
 4 │          case NonZeroInteger { <- "a party" }
   │               ───────┬──────  
   │                      ╰──────── this is a checked refinement
   │ 
   │ Help: Match on 'Integer' and prove the predicate inside the arm, the way every 'NonZeroInteger' is proven: an 'if' condition, a Case naming a written value, or a written value.
   │ 
   │ Note: A refinement's predicate erases before the Program runs, so the emitted check could only ask about 'Integer' — and the arm would run for values the predicate refuses.
───╯

What a proof changes

implementation {
	constant guests: NonZeroInteger = 4
	constant seats: NonZeroInteger  = guests::multiply(with 3)

	Terminal.print(seats) § 12
}

multiply(with:) of two NonZeroIntegers returns a NonZeroInteger, because a product of two non-zero integers is never zero. add(_:) of two returns a plain Integer, because 1::add(-1) is 0. Returning that sum as a NonZeroInteger is a return-type-mismatch.

Each library page lists, under Refinements, the methods a proof changes. The NonZeroInteger entry says:

A division by one of these answers a Rational rather than an Optional, and negate and absolute stay within the proof.

The NonEmptyString entry says:

The proof is what lets length answer above zero, and firstCharacter and lastCharacter answer a character rather than an Optional.

Division that can fail, and the rest of the arithmetic, is on Numbers.

When a proof makes a fallback unreachable, the compiler warns. divide(by:defaultingTo:) exists for a divisor that might be zero. Given a proven divisor, the fallback can never be used, and the warning is fallback-never-used:

[fallback-never-used]
Warning: This 'defaultingTo' Argument can never be read
   ╭─┤ bill.es:4:39 │
   │
 4 │     Terminal.print(12::divide(by guests, defaultingTo 0/1))
   │                                          ────────┬───────  
   │                                                  ╰───────── this fallback can never be read
   │ 
   │ Help: Drop the 'defaultingTo' Argument; the call already answers a NonZeroRational.
   │ 
   │ Note: Without it the call answers a NonZeroRational, which is never empty.
───╯

The program still compiles and runs. Drop the defaultingTo argument, as the Help says.

The compiler checks proofs in Essence code only. Do not count on a refinement to check a value that a JavaScript caller passes in: check it in JavaScript before the call. Calling Essence from JavaScript covers the boundary.