No edit summary |
No edit summary |
||
Line 12: | Line 12: | ||
Free types are sum types [https://en.wikipedia.org/wiki/Tagged_union]. | Free types are sum types [https://en.wikipedia.org/wiki/Tagged_union]. | ||
They make it easier to define recursive structures. | 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 === | === Syntax === | ||
Line 34: | Line 35: | ||
<Identifier> | <Identifier> | ||
<Identifier>(<Expression>) | <Identifier>(<Expression>) | ||
</pre> | |||
=== 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: | |||
<pre> | |||
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 | |||
</pre> | </pre> |
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)
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.
The FREETYPES machine clause contains a semicolon separated list of Freetype Definitions:
FREETYPES <Freetype Definition 1>; ...; <Freetype Definition N>
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>
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>)
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 ~.
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