1. Homepage
  2. Programming
  3. CS 440 Programming Languages and Translators - Homework 4: MiniML Type checker

CS 440 Programming Languages and Translators - Homework 4: MiniML Type checker

Engage in a Conversation
USIITIllinois Institute of TechnologyCS 440Programming Languages and TranslatorsMiniML Type checker

CS 440 HW4

Updated 3/13 to give more specifics about substitution in problem 3 and fix a Markdown conversion error. CourseNana.COM

In this homework you will be writing a typechecker for the MiniML language, for which you wrote an interpreter on HW3. See the language spec and README.md in your starter code repo for more information on MiniML and the codebase. Note that you will be using the same starter code that you used for HW3. Your finished toplevel will also use your interpreter code from HW3. You will not be graded on the interpreter part, so don't worry if your interpreter code has bugs (but we do still encourage you to fix any bugs we or you have found in your code, so you learn from them!) CourseNana.COM

Your code for this homework will go in unify.ml and typecheck.ml. CourseNana.COM


This assignment is to be completed individually, subject to the academic integrity policy on the course website. Make sure you read and understand these. CourseNana.COM

At the end of this assignment, we will ask you to list any students you discussed the homework with, as well as any websites or other resources (please list specific URLs when applicable) you referred to. CourseNana.COM

Important notes about grading

Your submissions will be graded automatically for correctness, as well as checked by hand. Please keep our autograder (and Xincheng, who has to run it) happy: CourseNana.COM

  1. Do not change or remove any lines that start with (*>*. CourseNana.COM

  2. Do not change the names or types of any functions defined in the starter code. This includes adding rec to functions that don't have it. CourseNana.COM


The file unify.ml contains code to unify two types, which is used in type checking. Recall that unification takes two types τ1 and τ2, potentially with unification variables like ?1. These are "holes" that can be unified with anything. Each instance of a particular variable must be filled with the same thing though (for example, if ?1 appears in both types, you must replace ?1 with the same type in both). CourseNana.COM

Recall that unification returns a substitution, which is a list of pairs (?i,τi) meaning "replace ?i with τi". For a substitution σ, we'll write [[σ]]τ to mean "τ with all the replacements in σ". So, for example, CourseNana.COM

[(?0, int); (?1, string)](?0 -> ?1) = int -> string CourseNana.COM

and CourseNana.COM

(?0, list(?1)); (?1, int)]?0 = int list CourseNana.COM

The OCaml definition for substitutions is given in unify.ml: CourseNana.COM

    type substitution = (int * typ) list

In that definition, ?0 is represented as just the integer 0. We also include a function sub_all: substitution -> typ -> typ, where sub_all s t computes [s]t, and a function sub_ctx: substitution -> ctx -> ctx where sub_ctx s c substitutes s into all of the types in the context c. CourseNana.COM

Recall the (recursive) unification algorithm from class: CourseNana.COM

Algorithm: Unify(τ1,τ2) Returns a substitution or an error. CourseNana.COM

  1. If τ1 and τ2 are both the same base type (int, string, bool, or unit), return the empty list [].
  2. If τ1 = τ2 = ?i (i.e., they are the same unification variable), return [].
  3. If τ1 = ?i, then: a. If ?i occurs in τ2, then error. b. Otherwise, return [(?i, τ2)].
  4. If τ2 = ?i, then: a. If ?i occurs in τ1, then error. b. Otherwise, return [(?i, τ1)].
  5. If τ1 = list(τ1') and τ2 = list(τ2'), then return Unify(τ1', τ2').
  6. If τ1 = τ1' -> τ1'' and τ2 = τ2' -> τ2'', then let σ = Unify(τ1', τ2') and return σ ++ Unify([σ]τ1'', [σ]τ2''), where ++ is the concatenation of substitutions.
  7. Similar to above for if τ1 = τ1' * τ1'' and τ2 = τ2' * τ2''.
  8. Otherwise, error.

The file unify.ml also contains one other function you might want: new_type : unit -> typ generates a new type consisting of just a unification variable ?n where ?n hasn't been used in the program before. This is useful for when we need to "guess" types to unify later. CourseNana.COM


  1. Implement the function unify : typ -> typ -> typ in unify.ml, following the algorithm above. Remember that we implemented two cases in class on Mar. 9, and the code is posted next to that lecture on the schedule on the website, and you are welcome to use this code.

Type Checking

The file typecheck.ml includes code to typecheck MiniCaml programs. It uses the unification function you wrote above. We did most of the work, you just need to implement a few cases. CourseNana.COM

  1. Implement the function type_of_const : const -> typ in typecheck.ml. The function should return the type of the given constant. You shouldn't need to do any unification. In the case of Nil, which represents the empty list [], the type is of course t list for some t. What's t? We have no way of knowing at this point, so you'll just have to take a guess... CourseNana.COM

  2. Fill in the remaining cases of typecheck_exp in typecheck.ml. This function takes an expression and returns a pair of its type and a substitution. You can take a look at the cases we've implemented so far, many of which we want over in class. You need to implement the cases for EApp, EUnop and ECons (these are listed at the end of the function and currently have raise Unimplemented as a placeholder). CourseNana.COM

    Here's an outline of how to implement these cases: CourseNana.COM

    1. EApp (e1, e2):
      • Infer the type of e1; call this t1 and the resulting substitution s1.
      • Infer the type of e2 (using s1 on the context); call this type t2 and the resulting substitution s2.
      • sub_all s2 t1 must be the same as TArrow (t2, tr) (that is, a function from t2 to tr), where tr is some type, but we don't know what type yet.
      • The type of the application expression is tr. Before you return it, apply the substitution you got from unify to it.
    2. EUnop (o, e):
      • Infer the type of e; call this t1.
      • Use type_of_unop to get the expected argument and return types for the unary operation o (like we did for the Binop case in class).
      • t1 must be the same type as the argument of o.
      • The type of the Unop expression is the return type of o.
    3. ECons (e1, e2):
      • Infer the type of e1; call this t1 and the resulting substitution s1.
      • Infer the type of e2 (using s1 on the context); call this type t2 and the resulting substitution s2.
      • Let tl be TList t1' (where t1' is t1 substituted with s2).
      • t2 must be the same as tl.
      • The type of the Cons expression is tl. Before you return it, apply the substitution you got from unify to it.


Compile and run your code using: CourseNana.COM

    make hw4

This will open something similar to the OCaml toplevel, which will let you type declarations and will print out the bindings and types introduced: CourseNana.COM

    Welcome to MiniCaml. Type #quit;; to exit.
    # let x = 1;;
    x : int = 1
    # let f y = x + y;;
    f : int -> int = <fun>
    # let x = 2;;
    x : int = 2
    # f 2;;
    - : int = 3

You can also use the binary hw4 in "batch mode" by giving it a .ml file on the command line, e.g. CourseNana.COM

    ./hw4 ../src/examples/rec.ml

    sum: int list -> int
    length: 'a list -> int
    map: ('d -> 'c * 'd list) -> 'c list
    int_to_string: int -> string
    onetwothree: string list

    sum = <fun>
    length = <fun>
    map = <fun>
    int_to_string = <fun>
    onetwothree = (""one")::((""two")::((""three")::([])))

This will interpret the entire file and print out the type and value of every top-level binding. We've provided some sample files in the examples folder, and you're welcome to write your own. CourseNana.COM

It's also important to make sure that, in addition to allowing well-typed programs, your type checker appropriately rejects programs with type errors. We've provided a few of these in examples/error. CourseNana.COM


When you are done with your work, make sure you have compiled your code using make (and ideally tested it using the instructions above). Submissions that do not compile will receive no credit. CourseNana.COM

When you're finished, use the following commands to submit: CourseNana.COM

    git add unify.ml
    git add typecheck.ml
    git commit -m "HW4 submit"
    git push

Please do actually use the commit message "HW4 submit" so we know when you intended to submit your homework and can also differentiate this from when you submitted HW3. CourseNana.COM

There are no additional files you need to add to the repo, just unify.ml and typecheck.ml. There are also no automatic tests, so you will not see a green check mark (or red X) on GitHub. As usual, double check GitHub and make sure you can see your latest code. CourseNana.COM

Get in Touch with Our Experts

WeChat WeChat
Whatsapp WhatsApp
US代写,IIT代写,Illinois Institute of Technology代写,CS 440代写,Programming Languages and Translators代写,MiniML Type checker代写,US代编,IIT代编,Illinois Institute of Technology代编,CS 440代编,Programming Languages and Translators代编,MiniML Type checker代编,US代考,IIT代考,Illinois Institute of Technology代考,CS 440代考,Programming Languages and Translators代考,MiniML Type checker代考,UShelp,IIThelp,Illinois Institute of Technologyhelp,CS 440help,Programming Languages and Translatorshelp,MiniML Type checkerhelp,US作业代写,IIT作业代写,Illinois Institute of Technology作业代写,CS 440作业代写,Programming Languages and Translators作业代写,MiniML Type checker作业代写,US编程代写,IIT编程代写,Illinois Institute of Technology编程代写,CS 440编程代写,Programming Languages and Translators编程代写,MiniML Type checker编程代写,USprogramming help,IITprogramming help,Illinois Institute of Technologyprogramming help,CS 440programming help,Programming Languages and Translatorsprogramming help,MiniML Type checkerprogramming help,USassignment help,IITassignment help,Illinois Institute of Technologyassignment help,CS 440assignment help,Programming Languages and Translatorsassignment help,MiniML Type checkerassignment help,USsolution,IITsolution,Illinois Institute of Technologysolution,CS 440solution,Programming Languages and Translatorssolution,MiniML Type checkersolution,