Types and inference
Name types, write annotations, define generic functions, and inspect the types inferred by the checker.
Types describe the values a program can accept and return. The checker infers types from definitions and their uses, and checks any annotations you write. This page shows how to name types, distinguish structural data from labelled values, write generic functions, and see the checker’s result.
(
i/core
i/stdio
)
increment = (x) { x + 1 }
main = () {
stdio.print(
core.inspect(increment(4)),
)
} 5 No type is written here. The + operator requires integers, so increment accepts an integer and returns an integer. Inference still checks the program; leaving out an annotation does not leave a value unchecked.
Definitions: names and labelled types
(
i/core
i/stdio
)
Point = { (x = Int, y = Int) }
ScreenPoint = (x = Int, y = Int)
Hidden = ()
Position = Point | Hidden
main = () {
raw : Point = (x = 3, y = 4)
labelled = ScreenPoint(x = 3, y = 4)
position : Position = raw
stdio.print(core.inspect((raw, (labelled.x, labelled.y), position, Hidden)))
} ((x = 3, y = 4), (3, 4), (x = 3, y = 4), Hidden) A type definition starts with an uppercase name and =. An alias is another name for an existing type. The written right side determines whether a definition makes an alias or a new labelled type:
Point = { (x = Int, y = Int) }names a record type: the braces group the data type, making a transparent alias.ScreenPoint = (x = Int, y = Int)defines a new labelled type and a constructor namedScreenPoint.Hidden = ()defines a labelled type whose constructor is the valueHidden.Position = Point | Hiddennames a union of the two existing types.
A union alias adds no constructor. A Position is already a record of type Point or the value Hidden; there is no Position(…) wrapper. The same rule applies to T = A | B: it names a union, even when A and B are labelled types.
A record type is structural: its positions, labels, and the types under those keys describe it. raw needs no constructor call to belong to Point. A labelled type has its own identity even when its fields match a record or another labelled type. ScreenPoint constructs that identity; a raw record with the same fields is not a ScreenPoint.
Data types write labels with =, as x = Int. Value annotations use :, as raw : Point. Both raw and labelled data support field access when the checker knows the fields and the constructor is visible. The example reads labelled.x and labelled.y rather than taking it apart.
Inferring the evaluator
The repository’s examples/tour/src/main.i uses the same type forms to describe arithmetic expressions. Here is that file unchanged:
(
i/stdio
std/int
)
Num = (Int)
Add = (Expr, Expr)
Mul = (Expr, Expr)
Expr = Num | Add | Mul
// Inferred: (e: Expr) -> Int
eval = (e) {
e |>
(Num(n)) { n }
| (Add(a, b)) { eval(a) + eval(b) }
| (Mul(a, b)) { eval(a) * eval(b) }
}
main = () {
sum = Add(Num(1), Num(5))
expr = Mul(sum, Num(7))
expr |> eval |> int.to_string |> stdio.print
} 42 Expr names the union of three labelled types. Add and Mul contain other expressions, so these definitions describe a recursive tree. eval takes that tree apart with the constructor patterns introduced on the functions page.
No parameter or result annotation is written on eval. Its branches tell the checker that it accepts Expr and returns Int: Num holds an integer, while Add and Mul combine recursive results with integer operators.
To inspect that inferred type, run:
i check --types | head -n 1 tour/main.eval : (Expr) -> Int Annotations and unions
(
i/core
i/stdio
)
NumberOrText = Int | String
show : (NumberOrText) -> String = (x) {
x |> (n : Int) { core.inspect(n) } | (s : String) { s }
}
choose : (Bool) -> { Int | String } = (flag) {
flag |> (True) { 7 } | (False) { "seven" }
}
main = () {
value : { Int | String } = choose(False)
count : Int = 7
stdio.print(show(value))
stdio.print(show(count))
} seven
7 Write name : Type = value to annotate a binding. Parameter annotations look like (x : Int), and a result annotation follows the parameter group as -> Int. A function type writes parameter types without parameter names: (Int) -> String.
After a : that introduces a type, the annotation ends at an outermost |. Put a union annotation inside braces: value : { Int | String }. A function annotation with a union result needs the same grouping: choose : (Bool) -> { Int | String }. Without the braces, the | would end that annotation.
A named alias also avoids an outermost |: show uses NumberOrText. Type definitions such as NumberOrText = Int | String are not annotations and read the full union directly. Space : like =, with one space on each side; i fmt applies this layout.
Annotations constrain inference rather than converting a value. Writing count : Int = 7 accepts an integer value; writing the same annotation on a string produces a type error. Union annotations let a value belong to any of their members, while a branch type test selects the member used in its body.
Generic functions and type parameters
(
i/core
i/stdio
)
Box(A) = (A)
identity = <A>(x : A) -> A { x }
wrap = <A>(x : A) -> Box(A) { Box(x) }
main = () {
stdio.print(
core.inspect((identity(5), identity("five"))),
)
stdio.print(
core.inspect((wrap(5), wrap("five"))),
)
} (5, "five")
(Box(5), Box("five")) A is a type parameter: a name for a type used within the definition. A generic type declares parameters in its head, as Box(A). A generic function declares them before its parameter group, as <A>(x : A) -> A. That A is in scope throughout the function, including its body.
identity gives back the value it receives, and the calls use it with both an integer and a string. wrap gives a Box containing the argument, so its result is Box(A). These examples use the written parameter to describe the relationship between input and output.
Seeing inferred types
(
i/core
i/stdio
)
identity = (x) { x }
count = 7
word = "seven"
numbers = [1, 2]
add_one = (x) { x + 1 }
main = () {
stdio.print(
core.inspect((identity(count), identity(word))),
)
stdio.print(
core.inspect((numbers, add_one(2))),
)
} (7, "seven")
([1, 2], 3) Run this command in the scratch project, whose package name is tour; it prints the first five lines of the checker’s type listing:
i check --types | head -n 5 tour/main.identity : (A) -> A
tour/main.count : 7
tour/main.word : "seven"
tour/main.numbers : List(1 | 2)
tour/main.add_one : (Int) -> Int Without head, i check --types prints every top-level name, including main. The name before : identifies the package, module, and binding. Inferred type parameters appear in the printed type even when no parameters were written in the source: the unannotated identity works for both calls.
Integers and strings have literal types. count has the type 7, and word has the type "seven", each containing exactly that value. List inference combines its item types, giving List(1 | 2). These values can be used where Int, String, or List(Int) is expected. An integer operator gives the whole type Int, which explains the result of add_one.
Some operations need a known type, including reading fields from a function argument. An annotation can supply that information, as raw : Point did above. Use annotations to state an interface or make the required shape clear, and use --types to inspect what the checker derives.
A type mismatch
main = () {
count : Int = "seven"
count
} i check reports E0501: “"seven" is not a subtype of Int”. The string value does not belong to the annotated type, so the module does not pass checking. Supply an integer or change the annotation to describe the intended value.
Current limits
The standard says the text form of a value of a labelled type keeps its labels, for example User(age = 36, name = "ada") (§11.8). The compiler on this tree prints the parts without their labels, so core.inspect of such a value shows ScreenPoint(3, 4). This is a recorded difference from the standard (known gaps, DOC2), not the intended output.