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.

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>)