Values: numbers, ids, text, money, time
Every field, parameter and carried value has a type, and the types are few. Each one says what the value is for, and the checker refuses the operations that would mix one purpose with another. This chapter goes through them with one program, a small club.
enum Tier { basic, silver, gold }
row Member { id: id, name: string(16), tier: Tier, joined: instant, paid: money(2), sponsor: option<id> }
unit Club {
state members: Member[8];
state open: bool = true;
state prices: map<Tier, money(2)> = map(Tier.basic => 1000, Tier.silver => 2500, Tier.gold => 5000);
contract join(member: id, name: string(16), now: instant, sponsor: option<id>) {
case !open => fail Closed;
else => Joined: members += [Member { id: member, name: to_upper(trim(name)), tier: Tier.basic, joined: now, paid: 0, sponsor: sponsor }];
examples {
{} (7, " ada ", 1000, none) => Joined { members: [Member { id: 7, name: "ADA", tier: Tier.basic, joined: 1000, paid: 0, sponsor: none }] };
{ open: false } (7, "ada", 1000, some(3)) => Closed;
}
}
contract promote(member: id, tier: Tier) {
case tier <= members[member].tier => fail NotHigher;
else => Promoted: members[member].tier := tier;
}
contract pay(member: id, months: int(1, 12)) -> money(2) {
else => Charged(get_or(prices, members[member].tier, 0) * months): members[member].paid += get_or(prices, members[member].tier, 0) * months;
}
contract renews(member: id) -> instant => Renews(members[member].joined + days(365));
contract card(member: id) -> string(32) => Card(concat(members[member].name, concat(" #", int_to_string(as_int(member)))));
contract sponsored(member: id) -> bool => Sponsored(match members[member].sponsor { some s => s != member, none => false });
contract shut() => Shut: open := false;
}
scenario a_member {
Club.join(7, " ada ", 1000, some(3)) => Joined;
Club.promote(7, Tier.basic) => NotHigher;
Club.promote(7, Tier.silver) => Promoted;
Club.pay(7, 3) => Charged(7500);
Club.renews(7) => Renews(31536001000);
Club.card(7) => Card("ADA #7");
Club.sponsored(7) => Sponsored(true);
Club.shut() => Shut;
Club.join(8, "bo", 2000, none) => Closed;
}
scenario a_member
Club.join(7, " ada ", 1000, Some(3)) => Joined
Club.promote(7, basic) => NotHigher
Club.promote(7, silver) => Promoted
Club.pay(7, 3) => Charged(7500)
Club.renews(7) => Renews(31536001000)
Club.card(7) => Card("ADA #7")
Club.sponsored(7) => Sponsored(true)
Club.shut() => Shut
Club.join(8, "bo", 2000, None) => Closed
Club = Club { members: [Member { id: 7, name: "ADA", tier: silver, joined: 1000, paid: 7500, sponsor: Some(3) }], open: false, prices: {basic: 1000, silver: 2500, gold: 5000} }
9 step(s), all as expected
bool and int
open: bool is true or false, read with !, && and ||. int is a whole number with no fixed range.
int(1, 12) is an int with a bound: pay accepts one to twelve months and nothing else. The chapter on contracts named the three places a bound holds: the checker refuses an example or a scenario step outside it, the verifier samples only inside it, and a served program refuses a request outside it. Here is the first of the three (book/refusals/values-bound.vish):
book/refusals/values-bound.vish:6:17: error: example argument for `guests` is outside its type
{} (6) => Visited { visits: 6 };
^
A bound is the cheapest rule in the language: one line in a header, and a whole class of arguments is gone from every tool at once. Fields take bounds too, like copies: int(0, 9) in the last chapter’s books. When a limit on a field is one that every call must keep, say it in the unit’s invariant as well, because the invariant is what the verifier checks after each call.
id
id is a key: the name of a row. You may write an int literal where an id is expected, join(7, …), but an id is not a number. It has no arithmetic that gives an id back, so the classic “next id is the last plus one” does not type (book/refusals/values-id.vish):
book/refusals/values-id.vish:5:73: error: field `id` expects id, got int
contract join(name: string(16)) => Joined: members += [Member { id: last + 1, name: name }], last := last + 1;
^^^^^^^^
last + 1 is an int, and an int is not an id. When you do need the number, as_int(member) gives it, as card does to print the member’s number, and as_id(n) turns an int back into an id. Where new ids come from, without arithmetic, is the last chapter of this part.
Text
string(16) is text of at most sixteen bytes, written in double quotes with the escapes \", \n, \t and \\. The builtins cover what a contract needs to normalise and assemble text: trim and to_upper in join, concat and int_to_string in card, and len, to_lower, starts_with, ends_with, contains, find, substr, split, join, replace and string_to_int besides.
Money
money(2) is an amount in minor units with two decimals: the gold price 5000 is fifty units. A money literal is a plain int of minor units, so there is no 50.00 to write. Money adds and subtracts money of the same scale and multiplies and divides by an int, which is how pay charges a price times a number of months. It never mixes with a plain number (book/refusals/values-money.vish):
book/refusals/values-money.vish:3:60: error: delta on `takings` expects money(2), got int(1,10)
contract sell(tickets: int(1, 10)) => Sold: takings += tickets;
^^^^^^^
Selling ten tickets does not add ten to the takings; ten tickets at a price does. The refusal is the checker asking which price.
Time
instant is a moment and duration a length of time, both in milliseconds. An instant plus a duration is an instant, which is how renews answers a year after joining: joined + days(365), and seconds, minutes and hours build the others. One instant minus another is a duration. Two instants cannot be added (book/refusals/values-instant.vish):
book/refusals/values-instant.vish:4:68: error: two instants can only be subtracted (giving a duration) or compared; instant + instant has no meaning
contract renews(member: id, now: instant) -> instant => Renews(now + members[member].joined);
^^^^^^^^^^^^^^^^^^^^^^^^^^^^
A contract does not read a clock. join takes now: instant as a parameter, like any other value; the last chapter of this part shows where the time comes from.
Enums
enum Tier { basic, silver, gold } is a type with three values, written Tier.gold. The variants are ordered as declared, so promote compares them: tier <= members[member].tier refuses a promotion to the same tier or a lower one, which the scenario’s second step shows. match reads one variant at a time, which the chapter on reading the state covers.
Options
option<id> is either none or some(x). sponsor is an optional member: most members join without one. You cannot use an option as the value inside it; you match it, one arm for each case: match members[member].sponsor { some s => s != member, none => false }. The name after some is the value inside, bound for that arm only.
Maps
map<Tier, money(2)> is an ordered map from tiers to prices, written map(Tier.basic => 1000, …). get_or(prices, tier, 0) reads with a default, get reads an option, put and remove_key build a new map, and has_key, keys, values and len inspect one. A map’s keys are ints, ids, strings or enums.
What the checker bought
verify: 2 examples, 9 scenario steps and 14000 sampled checks passed
The program has no rules, and it passed fourteen thousand sampled calls. The value of the types is in what did not get written: no money added to a count, no id computed from a number, no two moments summed. Each would have been a quiet wrong answer in a language that let it through; here each is a line number.
Try
Change paid: money(2) in the row to paid: money(3), as if the club had started keeping tenths of a cent. The checker refuses pay: the cell paid expects money(3) and the charge is money(2). Nothing converts between scales silently; the change has to be made where the price is.