Package "perfunctory_types"

Title:	Per-functor, static, polymorphic types
Rating:	Not rated. Create the first rating!
Latest version:	0.3
SHA1 sum:	d23f2290c698365bed766ce065e25c40ff36a2b7
Author:	Geoffrey Churchill <geoffrey.a.churchill@gmail.com>
Home page:	https://github.com/GeoffChurch/perfunctory_types
Requires:	subsumes

Reviews

No reviews. Create the first review!.

Details by download location

Version	SHA1	#Downloads	URL
0.3	d23f2290c698365bed766ce065e25c40ff36a2b7	3	https://github.com/GeoffChurch/perfunctory_types/archive/0.3.zip
0.2	0eee503c182811781c110b4b0ed569ec47a307f9	7	http://github.com/GeoffChurch/perfunctory_types/archive/0.2.zip
			https://github.com/GeoffChurch/perfunctory_types/archive/0.2.zip
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.

There might be bugs. Feedback is welcome!

See [the tests](t/) for lots of examples.

Overview

There is a syntactic and a semantic side to the type system. The semantic side builds on top of the syntactic side.

Syntactic checking

The basic idea is that type declarations constrain and coalesce the ambient "term algebra" (the Herbrand 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.

Syntactic typechecking amounts to checking that a term is a member of the algebra induced by the type declarations.

Semantic checking

Prolog's semantics are handled by inferring a conservative (GLB) type for each untyped predicate, and checking that each usage of the predicate conforms to the inferred type. The inference is implemented by simply unifying the types of the heads of all clauses for a given predicate, where each clause is syntactically typechecked in isolation. The checking is implemented by constraining each usage to be subsumed by the inferred type, using library(subsumes) for pure/relational subsumption.

For example, the following is ill-typed because color and list(_) cannot be unified:

:- type color --> r ; g ; b.
:- type list(X) ---> [] ; [X|list(X)].

p(red).
p([]).

Key features

Gradual typing

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

?- typecheck(f(x), Type).
Type = f(x). % x/0 and f/1 are "skolemized" so that type(x) = x and type(f(A)) = f(A).

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.

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 aka red squigglies

Some options are:

style_check/1

lsp_server

prolog_lsp

Installation in SWI-Prolog

?- pack_install(perfunctory_types).

Testing

for file in t/*.plt; do swipl -g "consult('$file'), run_tests" -t halt; done

---

(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 19 files holding a total of 65.9K bytes.