|Did you know ...||Search Documentation:|
|Pack typedef -- prolog/typedef.pl|
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.
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.
:- type foo ---> one ; two ; three. :- type bar ---> hello ; goodbye. ?- current_type(Type). Type = foo ; Type = bar .
:- type foo ---> one ; two ; three. :- type bar ---> hello ; goodbye. ?- current_type_constructor(bar, C). C = hello ; C = goodbye .