| Starter code (and tests): | pa7.pl |
The purpose of this assignment is to get some hands-on experience with logic programming in Prolog, and to exercise your understanding of type inference. It is to be completed individually according to the course collaboration policy.
You can work on this assignment using
SWI-Prolog
on ACS machines or on your own machine.
On an ACS GNU/Linux machine you will need to run
prep cs130u before you can run
pl, the SWI-Prolog binary.
You can cause SWI-Prolog to load a file at startup
using the -f switch, as in
pl -f pa7.pl.
You can also load a file at the Prolog prompt by entering, for example,
[pa7]. (without the .pl file extension).
The tests included use the PLUnit framework. To run all the tests at the Prolog prompt, enter run_tests. You can run the tests from the command line using pl -f pa7.pl -t run_tests.
Many of the test cases use
Prolog equality tests,
the var predicate, and
the setof predicate
in combination to ensure exactly (and only) the correct result is obtained.
Beginning with the Prolog code given in PLAI, develop a type-inference engine for the following grammar:
<expr> ::= num(<number>)
| add(<expr>,<expr>)
| with(<name>,<expr>,<expr>)
| id(<name>)
| fun(<name>,<expr>)
| app(<expr>,<expr>)
| bool(t) | bool(f)
| if(<expr>,<expr>,<expr>)
| rec(<name>,<expr>,<expr>)
<type> ::= t_num
| t_bool
| t_fun(<type>,<type>)
Above,
<number> is any Prolog number, and
<name> is any Prolog constant.
PLAI provides working type-inference rules in Prolog for the constructs
if,
fun, and
app.
It also provides a rule for
var—which we're calling id
as in previous assignments—but this rule has a bug:
it allows multiple type bindings for the same identifier
to be in effect simultaneously!
Modify the rule to rectify this.
The \= operator will come in handy; it's
introduced in this tutorial section about
equality of Prolog expressions.
Note also the primitive types are
t_num and t_bool,
not num and bool as in the rule from PLAI.
Instead of numConst and boolConst,
permit:
bool(B) with type t_bool
where B is either t or f, and
num(X) with type t_num
where X is any Prolog number.
You can use SWI-Prolog's number predicate
to tell if something is a number; see help(number)..
type_of and is_zero
Define a predicate type_of(Expr,T)
such that Expr has type T
in the initial type environment.
You can define type_of in terms of the
type predicate from PLAI.
In the initial type environment, include a binding that gives
the identifier is_zero
a function type taking a t_num and giving a t_bool.
add Expressions
Define a rule for binary add expressions
where both operands have type t_num
and the result has type t_num.
with Expressions
A with expression has three parameters:
As in PLAI and the previous assignment, the entire expression has the type of the body wherein the name is bound to the type of the named expression.
rec Expressions
A rec expression has three parameters:
As in PLAI and the previous assignment, the entire expression has the type of the body wherein the name is bound to the type of the named expression, and the named expression's type is consistent under this binding, which must be verified since the name may appear within it.
Do not restrict the named expression to be a fun.
Given the basic type-judgement rule for rec,
Prolog will correctly infer the types of cyclic definitions
without any special effort on your behalf!
You may earn bonus points by supporting
let-polymorphism in with expressions
as demonstrated by the following PLUnit test:
test(polymorphic_identity) :-
setof(T,
type_of(with(g,fun(x,id(x)),
if(app(id(g),bool(t)),app(id(g),num(0)),num(0))),
T),
[A]), A==t_num.
Hint: You need to treat with bindings differently
from fun bindings.
The chapter of PLAI titled "Implicit Polymorphism" and
this discussion of Prolog's
copy_term predicate
(the okpair example) should help you understand why and how.
For yet more points, support let-polymorphism in rec expressions
and demonstrate this with your own tests.
As with previous assignments, you will need to think carefully about where your code might fail and add your own test cases. Your submission will be tested against a more comprehensive suite of tests than we gave you and we may also assess the quality of your tests.