Free Types

Summary

Free types exist in Z and in the Rodin theory plugin and are supported by ProB. You can also define new free types in classical B by adding a FREETYPES clause with free type definitions separated by semicolon.

Here is a definition of an inductive type IntList for lists of integers constructed using inil and icons:

FREETYPES
  IntList = inil, icons(INTEGER*IntList)

What is a Free Type

Free types are sum types [1]. They make it easier to define recursive structures. A free type value may take exactly one of the defined subtypes, with additional payload data, and later the exact subtype can be queried and the payload data retrieved.

Syntax

FREETYPES

The FREETYPES machine clause contains a semicolon separated list of Freetype Definitions:

FREETYPES
  <Freetype Definition 1>;
  ...;
  <Freetype Definition N>

Freetype Definition

Each Freetype Definition consists of an identifier (the name of the free type), followed by an equals symbol and one or more Freetype Constructors separated by commas:

<Identifier> = <Freetype Constructor 1>, ..., <Freetype Constructor N>

Freetype Constructor

A Freetype Constructor may be a single identifier (the name of the free type constructor) or an identifier with a single expression argument (the type of the payload data) in parentheses.

<Identifier>
<Identifier>(<Expression>)

Semantics

The name of the free type can be used anywhere in the machine as a type identifier (like a set) to define the type of a value.

To actually create a value of the free type one needs to use one of the free type constructors. Free type constructors that do not take an argument can be used as the right side of an assignment as-is, while free type constructors that have an argument need a value parameter of that type - this works like a function call. Because those constructor calls work like function calls, we benefit from the tuple-function syntactic sugar and can use one tuple parameter as a way to represent multiple logical parameters and call the constructor with values separated by commas without having to create a tuple first.

Internally constructors without parameter are just values, while constructors with parameters are functions that take the payload data and return the free type value with the given payload. To check whether a free type value has a specific subtype one can use equality for parameter-less constructors and membership in the range for constructors with a parameter.

To get the contained value out of a free type value one can use the inverse constructor (also called deconstructor), simply created by applying the B operator ~.

Example

In our example from the introduction we have a free type with two constructors that represents a list. The constructor inil represents an empty list and takes no argument, while the icons constructor represents a list head with the first value and the rest of the list combined as a tuple.

To create a list with content we are using the simplified function call syntax, so we do not have to construct the tuple (head, tail) directly.

To get values out of the icons subtype we use the the deconstructor icons~. The resulting value is a tuple which we need to project to the first or second value respectively.

Here we implement a stack:

MACHINE IntListTest
FREETYPES IntList = inil, icons(INTEGER*IntList)
VARIABLES list
INVARIANT list : IntList
INITIALISATION list := inil
OPERATIONS
    push(value) = PRE value : INTEGER THEN
        list := icons(value, list)
    END;
    pop = PRE list /= inil THEN
        list := prj2(icons~(list)) 
    END;
    value <-- peek = PRE list : ran(icons) THEN
        value := prj1(icons~(list)) 
    END
END

Example usage in ProB2-UI: