Did you know ... | Search Documentation: |
Packs (add-ons) for SWI-Prolog |
Title: | Per-functor, static, polymorphic types |
---|---|
Rating: | Not rated. Create the first rating! |
Latest version: | 0.1 |
SHA1 sum: | 3abefa2fa8e6763658fdc4c19b1bc8cc685f21bd |
Author: | Geoffrey Churchill <geoffrey.a.churchill@gmail.com> |
Home page: | https://github.com/GeoffChurch/perfunctory_types |
No reviews. Create the first review!.
Version | SHA1 | #Downloads | URL |
---|---|---|---|
0.1 | 3abefa2fa8e6763658fdc4c19b1bc8cc685f21bd | 4 | http://github.com/GeoffChurch/perfunctory_types/archive/0.1.zip |
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:
pack.pl
?- make_directory(potato), pack_install(perfunctory_types, [url('http://github.com/GeoffChurch/perfunctory_types/archive/13.17.zip'), package_directory(potato)]).
Pack contains 5 files holding a total of 54.0K bytes.