perfunctory_types
is a static type system for SWI-Prolog.
It might be bugged or at least irreparably flawed. Feedback is very welcome!
See the tests for lots of examples.
The basic idea is that type declarations constrain and coalesce the ambient "term algebra" into a "type algebra".
The algebra is constrained into a subalgebra by constraining the types of a constructor's arguments.
The algebra is coalesced into a quotient algebra by declaring types with multiple constructors.
Typechecking amounts to checking that a term is a member of the algebra induced by the type constraints.
The algebra is left free except where explicitly coalesced/constrained by type declarations.
?- typecheck(f(x), Type).
Type = f(x).
?- type list(X) ---> [] ; [X|list(X)].
true.
?- typecheck([[]], Type).
Type = list(list(_)).
?- typecheck('[|]', Type).
Type = (_A->list(_A)->list(_A)).
?- type natF(X) ---> z ; s(X).
true.
?- NatT = natF(NatT), (type nat == NatT). % Declare `nat` as an alias for `natF(natF(...))`.
NatT = natF(NatT).
?- typecheck(s(z), Type). % Types are not aliased by default.
Type = natF(natF(_)).
?- typecheck(s(z), nat). % Only upon request.
true.
?- Omega = s(Omega), typecheck(Omega, Type).
Omega = s(Omega),
Type = natF(Type).
?- Omega = s(Omega), typecheck(Omega, nat).
Omega = s(Omega).
Unification forces us to preserve polymorphic arguments (see Frank Pfenning's lecture on polymorphism in LP).
?- type natvector ---> natxyz(nat, nat, nat). % This is okay.
true.
?- type vector ---> xyz(A, A, A). % This is not okay - polymorphic `A` is not preserved.
ERROR: Goal vars_preserved(xyz(_13642,_13642,_13642),vector) failed
?- type vector(A) ---> xyz(A, A, A). % This is okay - polymorphic `A` is preserved.
true.
This is an implementation-friendly consequence of type preservation. So (anyway questionable) entities like ST
are prohibited.
Typechecking is applied to terms, which may be entire programs. Types are "per-functor-y".
Syntax is similar to that of the very different type_check
pack.
Right now, type checking is "syntactic" in that it applies to terms and is completely unaware of predicates. More powerful semantic checking will be added soon, and will amount to inferring the type of a predicate's head functor as the unification of its per-clause head types.
There don't appear to be any technical blockers. Hopefully the hilog
pack can do the heavy-lifting.
Some options are:
?- pack_install(perfunctory_types).
$ cd t/
$ swipl -g "consult('*.plt'), run_tests" -t halt
(Note to self) To publish a new version:
- update
pack.pl
- do GitHub release with new tag matching the pack.pl version
- execute:
?- make_directory(potato), pack_install(perfunctory_types, [url('http://github.com/GeoffChurch/perfunctory_types/archive/13.17.zip'), package_directory(potato)]).