This module provides a way to declare new types that hook into the must_be/2 framework of library(error).

The type definition language is designed to be close to the one in Tom Schrijver's type_check package, supporting type synonyms, such as

:- type natnum == nonneg.

and algebraic type definitions like

:- type nat ---> zero ; succ(nat).

A built in type partial(T) is defined, which is satisfied by variables as well as terms that satisfy type T. This should be probably be extended to include all partial instantiations of type T, eg s(s(_)) should satisfy partial(nat), which it does not at the moment.

The result types can be used with must_be/2 and therefore in the record declarations provided by library(record) and the peristency declarations provided by library(persistency).

TODO

• Consider allowing duplicate type definitions if the definitions are the same.
• Consider extending partial(T) type.

 type(Spec)

Declares a new type. Spec can be one of two forms:

NewType ---> Constructor1 ; Constructor2 ; ... .
NewType == OldType

NewType can included type variables, which can be used in the constructor terms. The arguments of constructor terms are the types of the required arguments for that constructor. The second form declares a type synonym, so NewType is equivalent to OldType.

It is an error to declare the same type more than once, even if the definition is the same. Type name space is flat, not module scoped. This is directive. It cannot be called.

 current_type(+Type) is semidet

current_type(-Type) is multi

True if Type is a currently defined type. For example,

:- type foo ---> one ; two ; three.
:- type bar ---> hello ; goodbye.
?- current_type(Type).
Type = foo ;
Type = bar .

 current_type_constructor(?T, ?Constructor)

True if a type T allows the Constructor. For example,

:- type foo ---> one ; two ; three.
:- type bar ---> hello ; goodbye.
?- current_type_constructor(bar, C).
C = hello ;
C = goodbye .