Types

This chapter describes the types a Mica program’s values have: the kinds of type and how each is written, the values each holds, the types an operation takes and the type of its result, the conversions between types, when two types are one type and what an assignment admits, and the types a template declares with parameters. Each construct names its rule in the grammar, says what it means, and quotes what the compiler answers when a source breaks the rule. How a type is declared and named is chapter 3, and the value every variable of a type starts at is chapter 2. The capabilities each type carries, the matrix of what the sequence families admit and the integer family’s promotion and cast tables are the type system, which this chapter links rather than repeats.

Every example is complete, compiled and run by the compiler’s own test suite on AMD64 and AArch64, and the output shown beneath it is the output those runs are held to.

The kinds of type

A type is named by the right side of a type declaration (type-denoter) or, for a variable, a field or a parameter, where its type stands (value-type). The language names these kinds:

What each kind admits, operator by operator, is the capability table.

The ordinal types

An integer, bool, unicode, an enumeration and a subrange are ordinal: their values stand in a discrete order, each with a position. Ord gives a value’s position as an integer, Succ and Pred the value after and before it, and Chr the character of a code point. An ordinal is what a for loop counts through, a case dispatches on and a fixed array is indexed by.

An enumeration’s members are ordered as they are listed and counted from zero, so in Mode = (Off, Heat, Cool) Ord(Heat) is 1 and Heat < Cool holds. A bool is the ordinal False, True, counted 0 and 1. A subrange 5..30 holds the values of its base type from its first bound to its last, and 'A'..'D' holds four characters. A comparison answers a bool, so mode = Heat is a value a bool variable takes.

An enumeration, a subrange, bool and unicode carry no arithmetic: +, - and the other operators of numbers take none of them. A program computes with a subrange of the integers through its base type, (setting as int64) + 2, and converts the result back with as Setting.

A value of a subrange, an enumeration, bool or unicode always belongs to its type, on every tier. The compiler checks each road on which a value enters such a type from outside it: n as Setting stops the program with ordinal_out_of_domain at the conversion when n holds 31, in a debug build as in an O2 build; Chr stops for a number that is no Unicode scalar value; Succ, Pred, Inc and Dec stop past the domain’s edge; and a device register of such a type is checked at every read, as chapter 3 states. Traps names every road.

{
    Thermostat - the ordinal types: an enumeration, a subrange of the integers, a subrange of the characters, 'bool'
    and 'unicode', each value counted by 'Ord' and stepped by 'Succ' and 'Pred'.

    'Mode' is an enumeration, whose members are ordered as they are listed, so 'Heat' comes before 'Cool'. 'Setting'
    is a subrange of the integers, which carries no arithmetic of its own: the body computes through its base type,
    'setting as int64', and converts the result back with 'as Setting', a conversion checked on every tier, so the
    value always belongs to the subrange. 'Zone' is a subrange of the characters, whose successor is the next letter,
    and a 'bool' is the ordinal 'False', 'True', counted 0 and 1. An enumeration's members are the values a 'for' loop
    counts through.
}
program Thermostat;

imp
    WriteLn, Ord, Chr, Succ, Pred : std;

const
    Comfortable = 21;
    Warmer = 2;
    FirstZone = 'B';
    FirstLetter = 'a';
    ModeLine = "mode %lld, the next %lld, the one before %lld";
    OrderLine = "heat comes before cool: %lld";
    SettingLine = "setting %lld";
    ZoneLine = "zone %lc, the next %lc, code point %lld";
    TruthLine = "heating %lld, false %lld, true %lld";
    LetterLine = "the letter after a: %lc";
    CountLine = "mode %lld";

type
    { The modes the thermostat runs in. }
    Mode = (Off, Heat, Cool);

    { A temperature the thermostat may be set to, in whole degrees. }
    Setting = 5..30;

    { The zones of a house, named by letter. }
    Zone = 'A'..'D';

var
    mode : Mode;
    setting : Setting;
    zone : Zone;
    heating : bool;
    letter : unicode;
    reading : int64;

begin
    mode := Heat;
    WriteLn(ModeLine, Ord(mode), Ord(Succ(mode)), Ord(Pred(mode)));
    WriteLn(OrderLine, Ord(Heat < Cool));

    { a subrange computes through its base type and converts back with a checked 'as' }
    setting := Comfortable;
    reading := (setting as int64) + Warmer;
    setting := reading as Setting;
    WriteLn(SettingLine, setting as int64);

    zone := FirstZone;
    letter := Succ(zone);
    WriteLn(ZoneLine, zone, letter, Ord(zone));

    heating := mode = Heat;
    WriteLn(TruthLine, Ord(heating), Ord(False), Ord(True));
    WriteLn(LetterLine, Chr(Ord(FirstLetter) + 1));

    for mode := Off to Cool do
        WriteLn(CountLine, Ord(mode));
end.

It prints:

mode 1, the next 2, the one before 0
heat comes before cool: 1
setting 23
zone B, the next C, code point 66
heating 1, false 0, true 1
the letter after a: b
mode 0
mode 1
mode 2

The real types

float16, bfloat16, float32 and float64 hold real numbers in binary floating point, bfloat16 with float32’s range and eight bits of precision. A real is a number, ordered and computed with, but not an ordinal: it has no successor, so it counts no loop, indexes no array and selects no case arm. Its operators are +, -, * and /, and the remainder mod belongs to the integers: ratio mod 2.0 is refused with 5113, data type 'float64' cannot be used in arithmetic operation 'modulo' (requires integral). A real constant without a type computes in float64, and beside a real operand it takes that operand’s type, so single * 0.1 over a float32 is a float32 product.

The structured types

A record holds its fields, each of its own type, and a value of the record holds a value of every field (record-type, field-group). A fixed array holds one element for each index of its dimensions, and an index is an ordinal: a range 1..4, or the name of an ordinal type, so array[Shelf] of Jar holds one jar for each member of Shelf (array-type, dimension). A dynamic array, a span and the read view of a parameter hold runs of elements whose length the value carries, and the sequence families state what each admits. A set holds members of an ordinal type, asked with in (set-type). A string holds text, and Length counts its characters.

A structured value is a value: assigning a record or an array copies it, every element and field, so the copy changes while the original keeps its own. A sum type holds one of its cases with that case’s fields, and a case may hold a dynamic array of the sum type itself, Item = (ItemText(text : string), ItemList(items : array of Item)), so a value holds values of its own kind; a copy of it copies every value it holds, at every depth. A pointer T holds the address of a place of type T (type-reference), and a field read or written through it is the field of that place.

{
    Pantry - the structured types: a record, arrays indexed by an enumeration, a typed constant table, a set and a
    pointer.

    'Jar' is a record of a string and an integer, and 'Stock' an array of jars with one element for each member of
    'Shelf', which also indexes the table of the shelves' names. 'Shelves' is a set of shelves, asked with 'in'.
    Assigning a record copies it, so the spare jar changes while the top jar keeps its weight, and a pointer to an
    element writes through to the element itself.
}
program Pantry;

imp
    WriteLn, Length, Ord : std;

const
    Honey = "honey";
    HoneyGrams = 340;
    Rice = "rice";
    RiceGrams = 1000;
    Scoop = 250;
    ShelfLine = "%ls shelf: '%ls', %lld letters, %lld grams, used %lld";
    SpareLine = "the spare jar holds %lld grams, the top jar %lld";

type
    { The shelves of the pantry, from the top down. }
    Shelf = (Top, Middle, Bottom);

    { The shelves that hold something. }
    Shelves = set of Shelf;

    { A name for each shelf. }
    ShelfNames = array[Shelf] of string;

    { One jar: what it holds and how much. }
    Jar = record
        contents : string;
        grams : int64;
    end;

    { A pointer to a jar. }
    JarLink = pointer Jar;

    { One jar on each shelf. }
    Stock = array[Shelf] of Jar;

const
    Names : ShelfNames = ("top", "middle", "bottom");

var
    stock : Stock;
    used : Shelves;
    spare : Jar;
    link : JarLink;
    shelf : Shelf;

begin
    stock[Top].contents := Honey;
    stock[Top].grams := HoneyGrams;
    stock[Bottom].contents := Rice;
    stock[Bottom].grams := RiceGrams;
    used := [Top, Bottom];

    { a record assignment copies, a pointer writes through }
    spare := stock[Top];
    spare.grams := 0;
    link := address stock[Bottom];
    link.grams := link.grams - Scoop;

    for shelf := Top to Bottom do
        WriteLn(ShelfLine, Names[shelf], stock[shelf].contents, Length(stock[shelf].contents), stock[shelf].grams,
            Ord(shelf in used));
    WriteLn(SpareLine, spare.grams, stock[Top].grams);
end.

It prints:

top shelf: 'honey', 5 letters, 340 grams, used 1
middle shelf: '', 0 letters, 0 grams, used 0
bottom shelf: 'rice', 4 letters, 750 grams, used 1
the spare jar holds 0 grams, the top jar 340

A whole record or array has no single value to compare, so = and # over two of them are refused, and a program compares the fields or elements that decide its answer. spare = stock[Top] over two Jar records is refused with 5487: 'equal' compares two values of 'Jar', and a whole record has no single value to compare: equality over a block of elements is a walk, not an operator, so compare the elements or fields that decide the answer — for a sequence, walk it once and stop at the first difference, and for a record, compare the fields that identify it.

The types of operations

An operator takes operands of the types whose capability grants it, and its result has the operands’ type:

• +, -, * and / take integers and reals. Over two integers / divides and drops the fraction toward zero, so 7 / 2 is 3 and -7 / 2 is -3; mod gives the remainder of two integers.
• = and # take two values of one type that carries equality, <, <=, > and >= two of an ordered type, and every comparison answers a bool.
• and, or and not take two bool values and answer a bool, and over two integers they combine bits.
• in takes a member and a set of its type and answers a bool.

Two operands of different types meet in the type one of them promotes to, and the operation computes there: an int32 beside an int64 computes in int64, an int32 beside a float64 in float64. A constant without a type takes the type of the operand beside it where that type holds it, so level + 1 over a uint8 is a uint8 sum; where it does not, the constant keeps the first of int32, int64 and uint64 that holds it, as the type system states. Operands that meet in no type are refused with 5112, as the ordinal types’ table shows.

A result’s type is what WriteLn reads its conversion against, so the float32 product prints with %f, and %lld for the uint8 sum level + 1 is refused with 5184, format string validation error: format specifier '%lld' at position 1 incompatible with type: uint8. The example widens the sum with as int64 to print it.

Conversions

A value converts to another type implicitly where every value of its type is a value of the other: an int32 promotes to int64 and to float64, a uint8 to int16, and a float32 to float64. That is promotion, and its tables list every pair. A conversion that may change the value is written with as (casts): a narrower integer, an int64 to a float64, which rounds once where it is written, and a real to an integer, which drops the fraction toward zero, so 2.7 as int64 is 2 and -2.7 as int64 is -2. as binds more loosely than the operators, so a cast that is an operand stands in parentheses, (large as float64) / 2.0.

An enumeration, bool, unicode and a subrange of them convert to an integer only with Ord, and an integer becomes a character only with Chr. A subrange of the integers converts to and from its base type with as, checked as the ordinal types state.

{
    Scales - the conversions between types: promotion, which the compiler performs where every value survives, and
    'as', which the program writes where a value may change.

    An 'int32' promotes to 'int64' and to 'float64' without a word, and 'Grams', a second name for 'float64', takes a
    'float64' as it is. Integer division drops the fraction toward zero, and 'mod' answers the remainder. An 'int64'
    becomes a 'float64' only through 'as', and a real becomes an integer through 'as' by dropping its fraction. A
    constant takes the type of the operand beside it where that type holds it, so a 'uint8' sum stays a 'uint8' and a
    'float32' product a 'float32', and an 'int64' sum holds a constant no 'int32' holds. 'Ord' and 'Chr' convert
    between a character and its code point.
}
program Scales;

imp
    WriteLn, Ord, Chr : std;

const
    Seven = 7;
    Two = 2;
    Halving = 2.0;
    Fraction = 2.7;
    NearlyFull = 250;
    Billions = 3000000000;
    Tenth = 0.1;
    Letter = 'A';
    CodePoint = 66;
    PromotedLine = "%lld %lf";
    DivisionLine = "%lld %lld %lld";
    CastLine = "%lf %lf %lld %lld";
    ConstantLine = "%lld %lld";
    HalfLine = "%f";
    CodeLine = "%lld %lc";

type
    { A weight in grams, a second name for 'float64'. }
    Grams = float64;

var
    small : int32;
    large : int64;
    ratio : float64;
    weight : Grams;
    level : uint8;
    single : float32;

begin
    { promotion: every value of 'int32' is a value of 'int64' and of 'float64' }
    small := Seven;
    large := small;
    ratio := small;
    WriteLn(PromotedLine, large, ratio);
    WriteLn(DivisionLine, large / Two, large mod Two, -large / Two);

    { 'as': the program asks for the conversion that may round or drop a fraction }
    ratio := (large as float64) / Halving;
    weight := ratio;
    WriteLn(CastLine, ratio, weight, Fraction as int64, -Fraction as int64);

    level := NearlyFull;
    WriteLn(ConstantLine, (level + 1) as int64, large + Billions);
    single := Tenth;
    WriteLn(HalfLine, single * Tenth);
    WriteLn(CodeLine, Ord(Letter), Chr(CodePoint));
end.

It prints:

7 7.000000
3 1 -3
3.500000 3.500000 2 -2
251 3000000007
0.010000
65 B

Identity, compatibility and assignment

Two names are one type when one declaration names the other: Grams = float64; makes Grams a second name for float64, so a value of either is a value of both. A declaration that writes a type out, a record, an enumeration, a subrange, makes a new type, so two records with the same fields are two types, as chapter 3 shows with its refusal.

An assignment takes a value of the variable’s type, or of a type that promotes to it. Any other value is refused with 5143, which names the two types; the program writes the conversion it means, with as, Ord or Chr.

Types with parameters

A type declared with parameters behind of is a template (type-declaration, type-parameters), and the unit’s gen section declares its parameters (generic-section, generic-parameter). A type parameter stands for a type and carries a constraint, T is numeric, which says what a template’s body may do with its values. A value parameter stands for a number and has the type its gen section declares, N : int64.

A use names the template with its arguments (type-arguments), and each list of arguments makes a type of its own: Pair of int64 and Pair of float64 are two records, and Row of (int64, 4) is an array of four integers. A generic routine that takes a template binds its parameters from the argument’s type, and inside it a value parameter reads as a number of its declared type, so N prints with %lld and bounds a loop as any int64 does.

{
    Ledger - types with parameters: a record template over a type parameter and an array template over a type and a
    value parameter.

    The gen section declares the parameters: 'T', a type that carries the arithmetic, and 'N', an 'int64'. 'Pair of
    T' is specialized twice, once for 'int64' and once for 'float64', and each specialization is a type of its own.
    'Row of (int64, 4)' is an array of four integers, and the generic function 'Total' binds 'T' and 'N' from its
    argument's type, so inside it 'N' is the 'int64' its gen section declares: it prints with '%lld' and bounds the
    loop.
}
program Ledger;

gen
    T is numeric;
    N : int64;

imp
    WriteLn : std;

const
    RowLength = 4;
    Step = 10;
    LowSize = 2;
    HighSize = 9;
    LowWeight = 0.5;
    HighWeight = 1.5;
    PairLine = "%lld %lld %lf %lf";
    LengthLine = "a row of %lld values";
    TotalLine = "total %lld";

type
    { Two values of one type, the lower and the higher. }
    Pair of T = record
        low : T;
        high : T;
    end;

    { A row of 'N' values of type 'T', counted from one. }
    Row of (T, N) = array[1..N] of T;

var
    sizes : Pair of int64;
    weights : Pair of float64;
    counts : Row of (int64, RowLength);
    index : int64;

{ The sum of a row's values, whose length the function reads from its value parameter. }
function Total(r : Row of (T, N)) : T;
var
    at : int64;
begin
    WriteLn(LengthLine, N);
    for at := 1 to N do
        Total := Total + r[at];
end;

begin
    sizes.low := LowSize;
    sizes.high := HighSize;
    weights.low := LowWeight;
    weights.high := HighWeight;
    WriteLn(PairLine, sizes.low, sizes.high, weights.low, weights.high);

    for index := 1 to RowLength do
        counts[index] := index * Step;
    WriteLn(TotalLine, Total(counts));
end.

It prints:

2 9 0.500000 1.500000
a row of 4 values
total 100

A template declares at least one type parameter: Row of N = array[1..N] of int64; is refused with 5430, the template 'Row' declares only value parameters, and a template needs at least one type parameter beside them — 'Vec of (T, N)' rather than 'Vec of N' — so the abstract template stays clear of the backend until it is instantiated. Generics teaches templates and generic routines, and where a generic constraint is enforced states the rule a constraint is held to.