Assignment 5
Polymorphic type checking
in and for Prolog

1. Input format

Declarations are specified as ordinary Prolog clauses
(with modified precedence of ':', and ':' declared
a dynamic predicate, see starter code).

C : [type,...,type] -> type.   % type constructors
F : [Sigma,...,Sigma] -> Tau.  % function symbols
P : [Sigma,...,Sigma] -> o.    % predicate symbols

Function and predicate symbol declarations may contain
free variables that will be interpreted as schematic
type variables, implicitly quantified over the whole
declaration.

Programs are specified as ordinary Prolog clauses,
implicitly quantified over their free variables.
Programs should be directly executabale in Prolog
without regard to types.

2. Invoking the checker

Just load the file with declarations and clauses into Prolog.
The call the checker with check_all.

?- check_all.

This should verify the well-formedness of the declarations and
then type-check the clauses making up the declared predicates.
As it goes along it should print some minimal information,
say, the declaration or predicate definition that is checked.

If all goes well, it should just succeed.

If there is a type error, it should just fail.

It is not necessary to print any error messages.

3. Type system

Your need only check pure Horn clauses, but if you treat some
common built-in predicates and constants I won't object.

Declarations should be checked according to the specification
in the notes for Lecture 10.  I suggest to proceed with
the implementation in four stages.  I will accept partial
solutions along this dimension.

a. Only simple types (no polymorphism)
b. Polymorphic types (no parametricity checks)
c. Parametric polymorphic types
   i. functions symbols are type-preserving
   ii. clause heads are parametric

4. Starter code

I have provided some starter code that works in Gnu Prolog.
If you find bugs, or have to change it for other Prologs, please
send a note to lp-course@cs.  Feel free to throw away or
modify any of the provided code.

- reify.pl  provides some predicates to take Prolog clauses
            and terms and reify them into an explicit representation.
            Among other things, free variables are explicitly
            quantified.  The representation is defined in the fil.

- decls.pl  some example declarations and clauses to be checked.

- typecheck.pl  some Skeleton calls and Prolog mumbo-jumbo so that
            ':' is parsed correctly.

When it was complete, I invoked it with

| ?- [reify,typecheck,decls].
| ?- check_all.              
Decl int : []->type.
Decl + : [int,int]->int.
Decl list : [type]->type.
Decl [] : []->list(_201).
Decl . : [_185,list(_185)]->list(_185).
Decl nat : []->type.
Decl z : []->nat.
Decl s : [nat]->nat.
Decl plus : [nat,nat,nat]->o.
Decl sort_ : [list(int),list(int)]->o.
Decl member_ : [_121,list(_121)]->o.
Decl append_ : [list(_105),list(_105),list(_105)]->o.
Decl insert : [_85,list(_85),list(_85)]->o.
Decl perm : [list(_73),list(_73)]->o.
Decl diverge : []->o.
Clauses for plus/3: reifying...checking...done
Clauses for sort_/2: reifying...checking...done
Clauses for member_/2: reifying...checking...done
Clauses for append_/3: reifying...checking...done
Clauses for insert/3: reifying...checking...done
Clauses for perm/2: reifying...checking...done
Clauses for diverge/0: reifying...checking...done

true ? ;

no
| ?-

5. Hand-in

Please send me a tar file of a directory with your code.  Your code
directory should include a readme.txt file that gives (hopefully
simple!) instructions how to load and run your code.  Please restrict
yourself to GNU Prolog or SWI Prolog, because I do intend to
run your code.

If your code has limitations (for example, unimplemented features),
please note this in the readme.txt file.

Please document your code sufficiently so I can read it.