Types

IML has a rich type system rooted in OCaml's. You can define algebraic datatypes (variants), records, and use polymorphism. Every type admitted into the logic must be well-founded — there are no infinite data structures.

Algebraic datatypes (variants)

Algebraic datatypes are the backbone of modelling in IML. They define types as a choice between named constructors, each carrying zero or more values:

(* A simple enumeration *)
type color = Red | Green | Blue
 
(* A type with data *)
type shape =
  | Circle of real
  | Rectangle of real * real
  | Triangle of real * real * real
 
(* A recursive type — binary trees *)
type 'a tree =
  | Leaf of 'a
  | Node of 'a tree * 'a tree

Algebraic datatypes can be polymorphic (like 'a tree above) and recursive. Recursive types give rise to structural induction principles that ImandraX can use in proofs.

Well-foundedness

Every type admitted into the logic must be well-founded: there must be no infinite descending chains. This means every recursive type must have at least one base case (non-recursive constructor).

(* Well-founded: Leaf is a base case *)
type 'a tree = Leaf of 'a | Node of 'a tree * 'a tree
 
(* NOT well-founded — no base case, would be rejected *)
(* type bad = More of bad *)

This requirement ensures that induction over the type always terminates.

Records

Records group named fields together:

type point = {
  x : real;
  y : real;
}
 
type person = {
  name : string;
  age : int;
  active : bool;
}

Create record values and access fields:

let origin = { x = 0.0; y = 0.0 }
 
let distance p =
  Real.sqrt (p.x *. p.x +. p.y *. p.y)

Functional update

Create a new record that's like an existing one but with some fields changed:

let moved = { origin with x = 3.0 }
(* { x = 3.0; y = 0.0 } *)

Records are immutable — functional update creates a new record, leaving the original unchanged.

Tuples

Tuples group values without naming them:

let pair : int * string = (42, "hello")
let triple : int * bool * string = (1, true, "yes")
 
(* Destructure with pattern matching *)
let fst (a, _) = a
let snd (_, b) = b
 
let swap (a, b) = (b, a)

Type aliases

You can create aliases for existing types:

type name = string
type coordinate = real * real
type matrix = real list list

Type aliases are transparent — name and string are fully interchangeable.

Polymorphism

IML supports parametric polymorphism. Type variables start with ':

(* A polymorphic identity function *)
let id (x : 'a) : 'a = x
 
(* A polymorphic pair type *)
type ('a, 'b) either =
  | Left of 'a
  | Right of 'b
 
(* Polymorphic list functions *)
let rec length = function
  | [] -> 0
  | _ :: xs -> 1 + length xs
 
let rec map f = function
  | [] -> []
  | x :: xs -> f x :: map f xs

Specialization

When ImandraX reasons about a polymorphic function, it specializes (monomorphizes) it to the concrete types involved in the proof. For example, length applied to int list becomes a specialized length_int_list function internally. This allows ImandraX to use first-order reasoning techniques on higher-order definitions.

Mutually recursive types

Types can be mutually recursive using and:

type expr =
  | Lit of int
  | Add of expr * expr
  | Neg of expr
  | Block of stmt list
 
and stmt =
  | Assign of string * expr
  | Return of expr

Both types must be well-founded together.

Examples from the ImandraX repos

Here's a realistic type definition from the expression compiler example:

type expr =
  | Int of int
  | Plus of expr * expr
  | Times of expr * expr
  | Sub of expr * expr
  | Div of expr * expr
 
type instr =
  | Add
  | Mult
  | Minus
  | Quot
  | Push of int
 
type state = {
  stack : int list;
}

These types model an expression language and a stack machine — and ImandraX can prove that a compiler from expr to instr list is correct. See the Compiler Verification tutorial.