6 — Type Checking

Due Tuesday, 18 February, 6am

The purpose of this homework problem is to understand simple structural types and type checking.

Delivery Deliver your solutions in a folder called 6 in your github repo:

  • xcheck as specified in the testing task below.

  • CTests/ as specified in the testing task below.

  • Other/, which contains the solutions to the programming tasks.

Do read Make in case you need us to build your executables.

Programming Task

TPAL is SFVExpr program with all binding variable occurrences replaced by a TVAR, a typed binding variable, which is a JSON array of the shape [Var, ":", Type].

  A PType is one of:

  -- "int"

  -- [PType, ..., PType, "->", PType]

The prelude for TPAL programs may contain definitions for +, *, and ^, only. We will deal with cells next week.

All infix operator sequences are parsed into abstract syntax nodes for plain function calls of the operator variable on the full sequence of arguments.

The type checker traverses all sequences from left to right. It signals the first error as soon as it finds it:
  1. "variable x undeclared" a reference to a variable x without declaration;

  2. "int expected" an if-0 expression whose test expression is not of type int;

  3. "same type expected for if branches" an if-0 expression whose branch expressions have different types;

  4. "function type expected" a function-call expression whose first position does not have a function type;

  5. "number of arguments does not match number of parameters" a function-call expression whose function type lists a different number of domain types than there are arguments;

  6. "matching function and argument types expected" a function-call expression whose function type does not match the arguments’ types;

  7. "matching type declarations and types expected in Decl" a declaration block whose variable type specification does not match the type of the initialization expression.

Note the order in which these strings are listed. (This hint is too confusing.)

Testing Task Write the test harness and xcheck for your type-check programs.

Create ten tests for xcheck. Place them in CTests/. A test consists of two files: N-in.json and N-out.json for N in [0 .. 9].

An input file in ITests contains a single JSON TPAL expression. An output file contains a single JSON *AST expression (the result of type checking the given TPAL expression) or a JSON string that describes the first type error found.

  A *AST is a JSON object { "expr" : TAST, "type" : PType }.


  A TAST expression has one of these shapes:

   - a Var

   - an Int

   - a JSON array of the shape [*Decl,...,*Decl,*AST]

     all variables declared in one sequence are pairwise distinct

   - a JSON array of the shape ["fun*",[TVar, ..., TVar] ,*AST]

     all parameters in a sequence are pairwise distinct

   - a JSON array of the shape ["call",*AST,*AST,...,*AST]

     as in all mainstream languages, the first and required

     *AST is to evaluate to a function value

   - a JSON array of the shape ["if-0",*AST,*AST,*AST]


  A *Decl is a JSON array: ["let", TVar, "=", *AST ].

This grammar does not come with infix notation. If your abstract syntax representation has different representations for function calls and infix operations, render the infixes as calls.

Recall JSON: Simplicity and Complexity.