:- use_module(library(mavis)).
%% even(+X:integer) is semidet.
even(X) :-
0 is X mod 2.
The mavis module (because she helps with typing ;-) allows one to
use optional type declarations in Prolog code. During development,
these declarations throw informative exceptions when values don't match
types. A typical development environment converts this into a helpful
stack track which assists in locating the error.
In production, the declarations are completely removed by macros
and do nothing. Production time
is defined as any time when optimization is enabled:
current_prolog_flag(optimise, true).
Type declarations can be give manually by calling the/2. mavis also inserts
type declarations for you based on your PlDoc structured comments. For
example, during development, the definition of even above becomes
even(A) :-
the(integer, A),
0 is A mod 2.
We love dynamic types. That's one reason we love Prolog. But sometimes more precise types are a helpful tool. They can:
Mavis types are defined using has_type/2. We might define an
even_integer type with
error:has_type(even_integer, X) :-
0 is X mod 2.
We can use the definition manually:
frobnify(A, B) :-
the(integer, A),
the(even_integer, B),
B is 2*A.
or simply add it to our PlDoc comments:
%% frobnify(+A:integer, -B:even_integer)
frobnify(A, B) :-
B is 2*A.
We can declare types for bound variables, like A, and not-yet-bound variables, like B. The type constraints are implemented with when/2 so they apply as soon as a variable is ground.
To disable type checking in production, start Prolog with the
-O command line argument. A macro eliminates calls to the/2 so they
have no runtime overhead.
Using SWI-Prolog 6.3.16 or later:
$ swipl 1 ?- pack_install(mavis).
Source code available and pull requests accepted on GitHub: https://github.com/mndrix/mavis
| mavis.pl | ||
|---|---|---|
| has_intersection/2 | True if some value of IntersectionType is also of Type. | |
| has_subtype/2 | True if all values of Subtype are also values of Type. | |
| known_type/1 | True if Type is a type known to has_type/2. | |
| the/2 | Declare that Value has the given Type. | |
| type_intersection/2 | Multifile predicate for declaring that Type has an IntersectionType. | |
| type_subtype/2 | Multifile predicate for declaring that a Type has a Subtype. | |