%%% SPRING 98, CSE 520 %%% Solution of Assignment #2: %%% Type inference for a subset of ML (Mini-ML) %%% Proposal II. %%% In this solution, everything is a term except for the %%% lazy functions (ite and fix). This will constitute a better %%% representation for the evaluation program. %%% Note that the rules for typing terms containing numerical %%% operators are more "liberal" than the rules of the text of %%% the assignment: they allow also typing higher order terms %%% like (plus 2). The rule for fix, on the other hand, is %%% less liberal. %%% This corresponds to having the following grammar for the terms %%% %%% Term ::= Var | Num | tt | ff %%% | plus | minus | times | dv | equal %%% | ite Term Term Term %%% | pair | fst | snd %%% | \Var Term | Term Term %%% | fix Term module type_inference_for_Mini_ML. %%% main syntactic categories: kind tm type. % terms of Mini-ML kind tp type. % types of Mini-ML %%% constructors for representing terms of Mini-ML. type v string -> tm. % term vars (not needed if we use only closed tms) type c int -> tm. % numerical constant type tt, ff tm. % boolean constants type plus, minus, times, dv tm. % numerical ops type equal tm. % comparison type ite tm -> tm -> tm -> tm. % conditional type pair tm. % pairing type fst, snd tm. % projections type ab (tm -> tm) -> tm. % abstaction type app tm -> tm -> tm. % application type fix tm -> tm. % fixpoint operator %%% constructors for representing types of Mini-ML %%% we use the prefix notation for functional and product constructors type num, bool tp. % integers and booleans type tv string -> tp. % type vars (not needed if we use lambda Pr. vars) type arr tp -> tp -> tp. % functional type type prod tp -> tp -> tp. % cartesian product type infixr arr 5. infixl prod 6. %%% predicate representing type inference type infer tm -> tp -> o. %%% clauses representing the rules of the type system infer (c N) num. infer tt bool. infer ff bool. infer plus (num arr num arr num). infer minus (num arr num arr num). infer times (num arr num arr num). infer dv (num arr num arr num). infer equal (num arr num arr bool). infer (ite M N P) A :- infer M bool , infer N A , infer P A. infer pair (A arr B arr (A prod B)). infer fst ((A prod B) arr A). infer snd ((A prod B) arr B). infer (ab M) (A arr B) :- pi x\ (infer x A => infer (M x) B). infer (app M N) A :- infer M (B arr A) , infer N B. infer (fix M) A :- infer M (A arr A). %%% definition of the terms for testing the program type test int -> tm -> o. %%% #1: factorial: test 1 (fix (ab (f\ ab (x\ ite (app (app equal x) (c 0)) (c 1) (app (app times x) (app f (app (app minus x) (c 1)))))))). %%% #2: term \x. x x test 2 (ab (x\ app x x)). %%% #3: term \f g x. (f x , g x) test 3 (ab (f\ ab (g\ ab (x\ (app (app pair (app f x)) (app g x)))))). %%% end