Generics

Generics let you prove things once, and use the result for many different types.

Several different Acorn keywords can be used in a generic way, by adding a list of type parameters.

Generics with structure

You can define a generic structure by putting a list of generic parameters after the type name.

For example, let's define a LatticePoint that doesn't just have to be composed of integers, but can be any type.

structure LatticePoint[T] {
    x: T
    y: T
}

Here, T is the generic parameter.

If we define LatticePoint this way, then LatticePoint[Int] works exactly the same as if we had defined it with:

structure LatticePoint {
    x: Int
    y: Int
}

You can have multiple generic parameters in a single parameter list.

structure Pair[T, U] {
    first: T
    second: U
}

Generics with inductive

Similarly, you can define a generic inductive type.

For example, let's define the generic List type.

inductive List[T] {
    nil
    cons(T, List[T])
}

A list can be a list of anything, but a particular list can only be a list of one type of thing. A List[Int] is a list of Int, a List[Nat] is a list of Nat, a List[List[Bool]] is a list of List[Bool], and so on.

Generics with attributes

You can define attributes for a parametrized type by adding parameters to the attributes statement. The parameters have to match those used in the initial definition of the type.

For example:

attributes List[T] {
    // Whether this list contains a particular item.
    define contains(self, item: T) -> Bool {
        match self {
            List.nil {
                false
            }
            List.cons(head, tail) {
                if head = item {
                    true
                } else {
                    tail.contains(item)
                }
            }
        }
    }
}

Acorn tries to infer the type for generics, so that you don't have to include the [T] everywhere. In this example, we only have to use the type parameter T to specify the type of the item argument.

Generics with define

You can define a generic function by including type parameters after the function name.

define colinear[T](a: LatticePoint[T], b: LatticePoint[T]) -> Bool {
    a.x = b.x or a.y = b.y
}

Similarly, you can define member functions on a generic structure.

attributes LatticePoint[T] {
    define swap(self) -> LatticePoint[T] {
        LatticePoint.new(self.y, self.x)
    }
}

When you call generic functions, you generally do not need to provide the type parameters, because they can be inferred from the types of the arguments.

from int import Int
numerals Int

// No parameters on LatticePoint.new are needed.
let origin: LatticePoint[Int] = LatticePoint.new(0, 0)

// No parameters on colinear are needed.
theorem origin_self_colinear {
    colinear(origin, origin)
}

Generics with theorem

Similarly, you can define generic theorems by including type parameters after the theorem name.

theorem swap_is_involutive[T](p: LatticePoint[T]) {
    p.swap.swap = p
} by {
    p.swap.x = p.y
    p.swap.y = p.x
}

When you prove a generic theorem, it can be instantiated to any type.

Generics with let

If I told you that the let statement supported generics, and I didn't give you any sample code, I bet you could guess how it worked anyway.

But just in case. It looks like this:

let is_finite[T]: Bool = exists(xs: List[T]) {
    forall(x: T) {
        xs.contains(x)
    }
}

The generic let statement defines a constant for each type. You can think of it as a property of the type itself. In this case, it's defining whether the type itself is finite.