Fall 98, CSE 520: Assignment 2

Distributed: Published on the web on Sep 29.
Due: Oct 13 (in class).
Total maximum score: 100 points.
The purpose of this assignment is to provide experience with type systems a' la Curry and programming in high-level languages.
The following grammar defines an extension of the Lambda Calculus with some primitives similar to those of ML. 
  Term ::= Var                                % variables 
         | Num | true | false                 % numerical and boolean constants
         | Term Op Term | Term = Term         % numerical ops and comparison 
         | if Term then Term else Term        % conditional
         | (Term,Term) | fst Term | snd Term  % pairs and projections
         | \Var.Term | Term Term              % abstraction and application
         | fix                                % the fixpoint operator (Y)
Var and Num are syntactical categories which generate the set of term variables and the set of (representations of) integer numbers. Op is a syntactical category which generates the numerical operations +, *, - and /.

The following grammar defines the type expressions for the above language. 

  Type ::= int             % integers 
         | bool            % booleans 
         | TVar            % type variable
         | Type -> Type    % functional type
         | Type * Type     % cartesian product type
TVar is a syntactical category which generates the set of type variables (distinguished from the term variables above).

The rules of the type system are those of the system of Curry (for term variables, abstraction and application) plus the following ones: 

  --------------  for any numerical constant n
   G |- n : int


 
  ------------------    -------------------
   G |- true : bool      G |- false : bool



   G |- M : int   G |- N : int                     G |- M : int   G |- N : int
  ----------------------------- op = +,*,- or /   -----------------------------
        G |- M op N : int                               G |- M = N : bool



   G |- M : bool   G |- N : A  G |- P : A
  ----------------------------------------  
        G |- if M then N else P : A 



   G |- M : A   G |- N : B       G |- M : A * B      G |- M : A * B       
  --------------------------    ----------------    ----------------
      G |- (M,N) : A * B         G |- fst M : A      G |- snd M : B



  --------------------------
   G |- fix : (A -> A) -> A
The assignment consists in writing a program that does type inference, i.e. takes in input a term in the language above, and outputs its principal type (or fails if the term is not typeable). You can use either ML, Prolog or lambda Prolog.

Hint: lambda Prolog is probably the easiest choice, because (1) it provides the facility for encoding abstractions, and (2) it provides unification. (In ML, for instance, you would have to simulate both of them.) You can use the solution given in Lecture 8 (see the corresponding slides) for type inference in lambda calculus, and extend it to the language defined above. The solution will consist of the code of the program, and sample sessions on the following inputs:

Please add comments to the program to help me understanding it.

Please keep the file with the program: I might need to test it.