Package "perfunctory_types"

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

Reviews

No reviews. Create the first review!.

Details by download location

Version	SHA1	#Downloads	URL
0.1	3abefa2fa8e6763658fdc4c19b1bc8cc685f21bd	3	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.

Overview

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.

Salient aspects

Gradual typing

The algebra is left free except where explicitly coalesced/constrained by type declarations.

?- typecheck(f(x), Type).
Type = f(x).

Parametric polymorphism

?- type list(X) ---> [] ; [X|list(X)].
true.

?- typecheck([[]], Type).
Type = list(list(_)).

Function types

?- typecheck('[|]', Type).
Type = (_A->list(_A)->list(_A)).

Equirecursive fixpoints

?- 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.

Cycle safety

?- Omega = s(Omega), typecheck(Omega, Type).
Omega = s(Omega),
Type = natF(Type).

?- Omega = s(Omega), typecheck(Omega, nat).
Omega = s(Omega).

Type preservation

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.

No higher-rank types

This is an implementation-friendly consequence of type preservation. So (anyway questionable) entities like ST are prohibited.

No distinction between predicates and other terms

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.

---

TODOs

Higher-kinded types

There don't appear to be any technical blockers. Hopefully the hilog pack can do the heavy-lifting.

Tooling integration

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

style_check/1

lsp_server

prolog_lsp

Module-awareness

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?

Installation in SWI-Prolog

?- pack_install(perfunctory_types).

Testing

$ 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:

1. update pack.pl
2. do GitHub release with new tag matching the pack.pl version
3. execute:

   ?- make_directory(potato), pack_install(perfunctory_types, [url('http://github.com/GeoffChurch/perfunctory_types/archive/13.17.zip'), package_directory(potato)]).

Contents of pack "perfunctory_types"

Pack contains 5 files holding a total of 54.0K bytes.