Types
Types are an extremely important concept in the Lane programming language. The organization, underlying representation, and behavioral abstraction of data all rely on types.
Builtin Types
Lane provides several important builtin types:
Int
Double
String
Unit
Bool
Void
Their definitions are not exposed to programmers. However, we can roughly understand Void, Bool, and Unit as having definitions like these:
enum Void {}
enum Bool {
true()
false()
}
enum Unit {
unit()
}
Void cannot be constructed; Unit always has exactly one value, unit(); and Bool has two values, true() and false().
In actual Lane programs, there is no need to import the definitions of these types. The actual forms of unit(), true(), and false() are (), true, and false, respectively.
The Boolean type provides the special operators &&, ||, and !, called “and,” “or,” and “not,” respectively. They are used as follows:
assert_eq!(true && true, true)
assert_eq!(true && false, false)
assert_eq!(false && true, false)
assert_eq!(false && false, false)
assert_eq!(true || true, true)
assert_eq!(true || false, true)
assert_eq!(false || true, true)
assert_eq!(false || false, false)
assert_eq!(!true, false)
assert_eq!(!false, true)
It is also important to note that && and || are short-circuiting operators. For a && b, if a evaluates to false, b is not evaluated. Likewise, for a || b, if a evaluates to true, b is not evaluated. This matters especially when evaluating b may produce an effect. Short-circuiting will be discussed again in the later section on effects.
The integer type Int is a 64-bit integer, covering every integer from -(2^63) to 2^63 - 1.
The floating-point type Double is a 64-bit floating-point number conforming to the IEEE 754 standard. It includes positive infinity, double_inf; negative infinity, double_neg_inf; and not-a-number, double_nan.
Lane's string type is a sequence of ASCII codes.
Function Types
Function types use arrows: (A) -> B denotes a function that accepts one parameter of type A and returns a value of type B. For example:
fn f(x : Int) -> Int {
x * 2
}
Its type is:
f : (Int) -> Int
For a function f of type (A) -> B and a value x of type A, the expression f(x) always has type B.
The number of parameters of a function is called its arity. Here is an example of a binary function:
fn f(x : Int, y : Int) -> Int {
x + y
}
A function can also have arity zero, for example:
fn f() -> Int {
42
}
If the parameters of a function f include another function, then f is a higher-order function. If its parameters do not include functions, then it is a first-order function. Ordinary values can be regarded as zeroth-order. If the highest-order parameter of f is of order n, then f is an n + 1-order function.
For example, the following function is second-order:
fn[A, B] apply(f : (A) -> B, x : A) -> B {
f(x)
}
Function types can also carry type variables. For example, the type of the apply function above can be written as:
apply : [A, B]((A) -> B, A) -> B
This type can be read as follows: if A and B are types, f has type (A) -> B, and x has type A, then apply[A, B](f, x) has type B.
Here, type parameters can usually be inferred automatically by the compiler, so they need not always be written. Normally, apply[A, B](f, x) can be written simply as apply(f, x).
We can also read only half of the type above: if A and B are types, then apply[A, B] has type ((A) -> B, A) -> B.
This way of understanding types is essential for the existential types discussed below.
Existential Types
We have already seen an example of a generic type: the list type List. It can be written as type List : [Type] -> Type, which reads: if A is a type, then List[A] is also a type. In other words, List itself is not a type.
We can define a simplest generic type, Box, which stores only one value:
enum Box[T] {
box(T)
}
We can regard box as having type [T](T) -> Box[T]. This common kind of polymorphic type is called a universal type. But sometimes we need a box, Hide, that can store any content without reflecting the type of that content in the type of the box itself. In other words, we need a constructor of type [T](T) -> Hide and the corresponding definition of the type Hide. In Lane, we can write this as follows:
enum Hide {
hide[T](T)
}
Notice that the type variable T is no longer introduced by the enum declaration; it is introduced by the constructor hide. In this example, Hide itself is a type, namely Hide : Type; while hide needs a type parameter and has type [T](T) -> Hide. Its type has the same left-hand side as the type of box and differs only on the right-hand side, but the difference is fundamental.
How can we use such a type? We can use pattern matching, or a binding specifically for irrefutable patterns:
let v : Hide = hide[Int](10)
...
let hide[T](x) = v
// or
match v {
hide[T](x) => ...
}
Note, however, that because v has type Hide, using it does not tell us that it stores an integer. We know only that after unpacking it, x has type T. Therefore, neither the value x nor the type T can escape its scope. For example, the following program is illegal:
fn[T] escape(v : Hide) -> T {
let hide[T](x) = v
x
}
This is because unpacking v essentially matches the hidden type to the type variable T. This T shadows the type variable T introduced by the function's type parameter in the surrounding context. Thus, the program above is no different from the following program:
fn[R] escape(v : Hide) -> R {
let hide[T](x) = v
x
}
This makes the problem clear: x has type T, while the function must return R. There is clearly no evidence that these two types are the same, so the function cannot compile.
Inductive Types
Lane supports user-defined finite data types of arbitrary depth. A classic example is the List data structure in the Basic.Data.List package. Let us revisit its definition:
pub enum List[T] {
empty()
cons(T, List[T])
}
The constructor cons has two parameters: one of the element type T, and one of the list's own type, List[T]. This naturally raises a question: does List form an infinite data structure by containing itself? The answer is no. Lane uses a strict evaluation strategy: before a value is bound, every subexpression on which it depends must first be evaluated. For example:
let x = f(1 + 1, fib(30))
This binding first evaluates 1 + 1 and fib(30) from left to right, calls f after obtaining their results, and finally binds the result to x.
Therefore, it is impossible to define a list that contains itself:
let l = cons(1, l)
This code cannot compile because the expression on the right-hand side uses l before l is bound. By providing the empty() constructor, the definition of List ensures that at least one path lets a list eventually terminate rather than becoming an infinite structure.
Inductive types are used through pattern matching; we have already seen this in the definition of length. Pattern matching requires every case to be covered. For a list, for example, we must match both empty() and cons(x, xs).
Structs as Interfaces
An “interface” describes the requirements or constraints that a program places on a type. Lane has no language feature that corresponds exactly to interface in other languages, but structs can usually express this kind of constraint. We have already seen this when defining and using Add; now we will continue with the example of aggregating elements in data structures. This example gradually abstracts two questions: how elements are combined, and how a data structure is traversed.
First, consider summing an integer list:
fn sum(list : List[Int]) -> Int {
match list {
empty() => 0
cons(x, xs) => x + sum(xs)
}
}
This function is a special case of a more general program. Summation does not apply only to integers; it may also apply to floating-point numbers or other types that support addition. We can therefore first generalize it into the following list traversal function:
fn[T] visit(list : List[T], init : T, auto offer add_ops : Add[T]) -> T {
match list {
empty() => init
cons(x, xs) => x + visit(xs, init)
}
}
Here, Add[T] means that the element type T supports addition, while init is the result for an empty list. This example already shows that an aggregation operation depends both on the way the element type combines values and on the way the list itself is traversed.
More generally, a list has a general fold operation: it starts with init, takes elements from the list in turn, and accumulates the result.
pub fn[T, R] fold(list : List[T], init : R, f : (T, R) -> R) -> R {
match list {
empty() => init
cons(x, xs) => f(x, fold(xs, init, f))
}
}
The two parameters of the combining operation can even have different types: f has type (T, R) -> R, rather than (T, T) -> T. Thus, sum can be viewed as a special case of fold:
fn sum(list : List[Int]) -> Int {
fold(list, 0, int_add)
}
For lists, fold is a very general function; almost any list operation can be expressed as a fold.
However, aggregation is not limited to lists. The same task can be performed on a binary tree:
enum Tree[T] {
leaf()
node(Tree[T], T, Tree[T])
}
fn sum(tree : Tree[Int]) -> Int {
match tree {
leaf() => 0
node(l, x, r) => sum(l) + x + sum(r)
}
}
List.sum and Tree.sum have both similarities and differences. Both use integer addition and 0 as the result for an empty structure; their traversal strategies differ: List follows successor nodes, whereas Tree must visit its left and right subtrees. For a tree, we can first write a traversal function corresponding to the list visit:
fn[T] visit(tree : Tree[T], init : T, sum : (T, T) -> T) -> T {
match tree {
leaf() => init
node(l, x, r) => sum(sum(visit(l, init, sum), x), visit(r, init, sum))
}
}
At this point, we can clearly separate two kinds of abstraction: one constrains how elements are combined, and the other constrains how a container is traversed. Struct interfaces can express these two requirements separately.
First, use Monoid to describe the way an element type must combine values:
struct Monoid[T] {
empty : T
append : (T, T) -> T
}
offer int_impl_monoid : Monoid[Int] = ...
offer double_impl_monoid : Monoid[Double] = ...
empty and append cannot be filled in arbitrarily. append must satisfy associativity; appending empty to any x must produce x, which means that empty is an identity element. A structure satisfying these two laws is commonly called a monoid. The Lane compiler cannot verify these conventions, so they must be ensured by the implementer of the interface.
With this interface, each element type can provide its own aggregation rules. For example, the integer instance can use 0 and addition, while the floating-point instance can use its own identity element and combining operation. auto offer monoid : Monoid[T] means that the function requires a Monoid[T] implementation, but callers normally do not need to pass it manually. The tree traversal function can therefore stop receiving an initial value and combining function explicitly:
fn[T] visit(tree : Tree[T], auto offer monoid : Monoid[T]) -> T {
match tree {
leaf() => monoid.empty
node(l, x, r) => monoid.append(monoid.append(visit(l), x), visit(r))
}
}
Next, use Foldable to describe the traversal capability that a data structure must provide:
struct Foldable[F : [Type] -> Type] {
fold_map : [T, R](F[T], (T) -> R, Monoid[R]) -> R
}
Here, Foldable constrains not an individual type, but a type constructor such as Tree or List. The [Type] -> Type after the colon in F indicates that, for any type T, F[T] is a type. fold_map accepts a container, a function that maps elements to aggregation results, and a Monoid[R]; it traverses the container and returns the final aggregation result.
Therefore, List and Tree can each provide a Foldable implementation that describes their own traversal order, while a Monoid implementation independently determines how elements are combined. Together, they allow the same aggregation operation to apply to different data structures and element types. This is the key role of structs as interfaces in Lane: they do not impose an inheritance relationship on types, but explicitly record the capabilities and conventions that a program requires.