Hello, if you have any need, please feel free to consult us, this is my wechat: wx91due

Mini-Project 3: Type Inference

CAS CS 320: Principles of Programming Languages

Due May 1, 2025 by 8:00PM

In this project, you’ll be building yet another interpreter for a subset of OCaml. It’ll be your task to implement the following functions:

val principle_type : ty -> constr list -> ty_scheme option

val type_of : stc_env -> expr -> ty_scheme option

val is_well_typed : prog -> bool

val eval_expr : dyn_env -> expr -> value

The types used in the above signature appear in the module Utils. Your implementation of these functions should appear in the file interp3/lib/interp3.ml. Please read the following instructions completely and carefully.

Part 1: Parsing

You’ll be given part of the parser for the language you’ll be implementing. A program in our language is given by the grammar in Figure 1. We present the operators and their associativity in order of increasing precedence in Figure 2. It will be up to you to read through the existing parser and determine what is missing from it, based on the given grammar (Hint. the lexer is complete).

Note that there is a desugaring process going on within the parser, so the target type expr does not match the grammar exactly. Please make sure you understand how programs in the language correspond to expressions in expr, and how the given code for evaluating programs depends on your code for evaluating expressions.

Part 2: Type Inference

We’ll be using a constraint-based inference system to describe the type inference procedure for our language. We write Γ ⊢ e : τ ⊣ C to means that the expression e (expr) has type τ (ty) in the context Γ (stc_env) relative to the set of constraints C (const list). See the file lib/utils/utils.ml for more details on the associated types. What follows is the typing rules of the inference system for our language.

Literals

Figure 1: The grammar for our language

Figure 2: The operators (and their associativity) of our language in order of increasing precedence

Options

Here (and below), fresh means not appearing anywhere in the derivation. You should use gensym in the module Utils to create fresh variables.

Note that this isn’t really pattern matching. We’re not using any notion of a pattern, but instead defining a shallow destructor.

Lists

Pairs

Variables

Note that this rule will require implementing substitution on types.

Annotations

Assertions

Operators

Conditionals

Functions

Let-Expressions

Remarks

The expression type_of Γ e should be Some τ ′ where τ ′ is the principle type scheme of the expression e in the context Γ. That is, given that Γ ⊢ e : τ ⊣ C, you must

▷ determine the most general unifier S of the unification problem defined by C;

▷ determine the type Sτ , i.e., the type τ after the substitution S;

▷ quantify over the free variables of Sτ to get the principle type scheme τ ′ . Note that the principle type scheme τ ′ should be the result of evaluating principle_type τ C.

type_of Γ e should be None if there is no unifier for C. Finally, the expression is_well_typed p should be true if and only if each individual binding in the collection of top-level let-expressions has a type relative to the context containing previously defined bindings. That is, the program

is well-typed if

▷ e1 is well-typed with type scheme τ1 in the empty context ∅

▷ e2 is well-typed with type scheme τ2 in the context {x1 : τ1}

▷ e3 is well-typed with type scheme τ3 in the context {x1 : τ1, x2 : τ2}

and so on. The empty program is well-typed.

The last thing we’ll mention: type schemes are defined using the VarSet module defined in Utils. Make sure to take a look at this module for hints on how to use it. It defines a standard set type with operations like union, singleton, and to_list.

Part 3: Evaluation

The evaluation of a program in our language is given by the big-step operational semantics presented below. It’s identical to that of mini-project 2, with some additional constructs. We write ⟨ ε , e ⟩ ⇓ v to indicate that the expression e evaluates to the value v in the dynamic environment ε. We use the following notation for environments.

We take a value to be:

▷ an integer (an element of the set Z) denoted 1, −234, 12, etc.

▷ a floating-point number (an element of the set R), denote 1.2, −3.14, etc.

▷ a Boolean value (an element of the set B) denoted ⊤ and ⊥

▷ unit, denoted •

▷ a closure, denoted (ε , s 7→ e ), where ε is an environment, s is a name, and e is an expression. We’ll write (ε , · 7→ e ) for a closure without a name.

▷ a pairs of values, denoted (u, v)

▷ a list of values, denoted [v1, v2, . . . , vk]

▷ an option value, denoted None or Some(v)

The expression eval_expr ε e should the value v (value) in the case that ⟨ ε , e ⟩ ⇓ v is derivable according to the given semantics. There are three cases in which this function may raise an exception.

▷ DivByZero, the second argument of a division operator was 0 (this includes integer modulus).

▷ AssertFail, an assertion within our language (not an OCaml assert) failed.

▷ CompareFunVals, a polymorphic comparison operator (e.g., = or <) was applied to closures.

Literals

Options

Lists

Pairs

Variables, Annotations, Assertions

Operators

Note that there is no division-by-zero error in the case of floating-point numbers.

To save room, all of the following rules do not include the side condition that v1 and v2 cannot be closures.

Conditionals

Functions

Let-Expressions

Putting Everything Together

After you’re done with the required functions, you should be able to run:

dune exec interp3 filename

in order to execute code you’ve written in other files (replace filename with the name of the file which contains code you want to execute). Our language is subset of OCaml so you should be able to easily write programs, e.g., here is an implementation of sum_of_squares without type annotations:

(* sum of squares function *)

let sum_of_squares x y =

let x_squared = x * x in

let y_squared = y * y in

x_squared + y_squared

let _ = assert (sum_of_squares 3 (-5) = 34)

There are a large number of examples in the file examples.ml. If you’re code is correct, you should be able to run this entire file (the inverse is not true, being able to run this file does not guarantee that your code is correct). You can pull out individual test cases as you work through the project.

Final Remarks

▷ There is a lot of repetition here, this is just the nature of implementing programming languages. So even though there is a lot of code to write, it should go pretty quickly. Despite this, it may be worthwhile to think about how to implement the interpreter without too much code replication.

▷ Test along the way. Don’t try to write the whole interpreter and test afterwards.

▷ You must use exactly the same names and types as given at the top of this file. They must appear in the file interp3/lib/lib.ml. If you don’t do this, we can’t grade your submission. You are, of course, allowed to add your own functions and directories.

▷ You’re given a skeleton dune project to implement your interpreter. Do not change any of the given code. In particular, don’t change the dune files or the utility files. When we grade your assignment we will be assume this skeleton code.

▷ Even though we’ve given a lot more starter code this time around, you still need to make sure you understand how the starter code works. This means reading code that you didn’t write (which is what you’ll spend most of your life doing if you go on to be a software engineer). A word of advice: don’t immediately ask on Piazza "what does this code do?" Read it, try it out, and try to come up with a more specific question if you’re still confused.