Problem sets
5.1 PS1
5.2 PS2
5.3 PS3
5.4 PS4
5.5 PS5
5.5 PS5
On this page:
5.5.1 Problem 1
6.2.0.5

5.5 PS5

Due: Midnight, December 20

Purpose: The goal of this problem set is to demonstrate you can design and implement a type system for an advanced language feature.

You should work with your most recent homework partner on this assignment and submit to your pair’s repo.

5.5.1 Problem 1

Design and implement a type system and inference algorithm for a language with first-class contracts.

This language should include the following features:
  • Anonymous functions without type annotations, Fun(X, E),

  • Monitors between contracts and expressions, Mon(C, E),

  • Predicate contracts, Pred(E), which is a contract on values of type T if E has type Arr(T, Bool),

  • Function contracts, CArr(C_1, C_2), which is a contract on values of type Arr(T_1, T_2) if C_1 is a contract on values of type T_1 and C_2 is a contract on values of type T_2, and

  • Conditionals, natural numbers, Booleans, and other operations we’ve seen.

In the above description, the metavariable C is synonymous with E; contracts are just expressions.

Define the language of types (as a grammar). Write down a type judgment relation, either as text or in Redex. Implement a type inference algorithm using any technique and written in any programming language.

 

Web Accessibility