%%% SPRING 98, CSE 520 %%% Solution of Assignment #2: %%% Type inference for a subset of ML (Mini-ML) %%% Proposal I 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. %%% we use the prefix notation for plus, minus etc. type v string -> tm. % term vars (not needed if we use only closed terms) type c int -> tm. % numerical constant type tt, ff tm. % boolean constants type plus, minus, times, dv tm -> tm -> tm. % numerical ops type equal tm -> tm -> tm. % comparison type ite tm -> tm -> tm -> tm. % conditional type pair tm -> tm -> tm. % pairing type fst, snd tm -> tm. % projections type ab (tm -> tm) -> tm. % abstaction type app tm -> tm -> tm. % application type fix 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 M N) num :- infer M num , infer N num. infer (minus M N) num :- infer M num , infer N num. infer (times M N) num :- infer M num , infer N num. infer (dv M N) num :- infer M num , infer N num. infer (equal M N) bool :- infer M num , infer N num. infer (ite M N P) A :- infer M bool , infer N A , infer P A. infer (pair M N) (A prod B) :- infer M A , infer N B. infer (fst M) A :- infer M (A prod B). infer (snd M) B :- infer M (A prod 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 ((A arr A) arr A). %%% definition of the terms for testing the program type test int -> tm -> o. %%% #1: factorial: test 1 (app fix (ab (f\ (ab (x\ (ite (equal x (c 0)) (c 1) (times x (app f (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\ (pair (app f x) (app g x)))))). %%% end