Did you know ... | Search Documentation: |

Pack perfunctory_types -- README.md |

`perfunctory_types`

`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](t/perfunctory_types.plt) 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. This is in some sense secondary to constraints but it enables finite expression of nontrivial type algebras.

Typechecking amounts to checking that a term is a member of the subalgebra 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".

`type_check`

pack.
There don't appear to be any technical blockers. Hopefully the `hilog`

pack can do the heavy-lifting.

Right now, type checking must be done manually with typecheck/2.

Type declarations currently just `assertz`

into the database, and can be retracted with retract_all_types/0. This is hacky and has no awareness of modules. What is the best way to do this?

?- pack_install(perfunctory_types).

$ swipl t/perfunctory_types.plt swipl t/perfunctory_types.plt % PL-Unit: perfunctory_types ...................................................... passed 0.016 sec % PL-Unit: examples .... passed 0.001 sec % All 58 tests passed

(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)]).