Introduction

In this assignment you will implement a simple structural typechecker inspired by the Typed Classes discussed in Lecture 14. Starting with the interpreter of Assignment 2, the given skeleton adds a syntax for anonymous objects with named fields. An example is the following taken from the tests

{obj
 {hello true}
 {goodbye false}
 {a-num 42}
 {n-func {lam {x : num} x}}
 {b-func {lam {x : bool} x}}}

This object has 5 fields: two boolean fields, one number field, and two function fields, AKA methods. There are no classes in this language, but each object has a type. In this case the object has the type (e.g. for annotating function variables) of

{obj {hello bool}
     {goodbye bool}
     {a-num num}
     {n-func {num -> num}}
     {b-func {bool -> bool}}}

You task is to update the typecheck function in the given skeleton to understand these objects and the corresponding msg operation. For example following expression has type {num -> num}

{msg
 {obj {func {lam x {+ x 1}} 3}}
 func}

Changes from Assignment 2

The type Exp for abstract syntax has been augmented with two new variants. objE defines an object with a list of named fields, each an arbitrary expression. msgE defines message sending operation. In order to make the type system easier to manage, the messages are symbols rather than expressions. The parser has been updated to support a corresponding concrete syntax, used in the tests below.

[objE (fields : (Listof (Symbol * Exp)))]
[msgE (obj : Exp) (selector : Symbol)]

Since the goal is implement a typed language, the abstract syntax for type annotations has similarly been extended.

(define-type TypeExp
  [numTE]
  [boolTE]
  [arrowTE (arg : TypeExp)
           (result : TypeExp)]
  [objTE (fields : (Listof (Symbol * TypeExp)))])

Finally the type for representing types in our toy language has been extended. Note that in the actual Type objT variants, the fields are a hash table rather than a list. This makes field lookup more efficient. The interp-te function that translates from TypeExp to Type has been extended to convert from the list of fields to a hash table.

(define-type Type
  [numT]
  [boolT]
  [arrowT (arg : Type)
           (result : Type)]
  [objT (fields : (Hashof Symbol Type))])

1. Typecheck objects

Your first task is to complete the objE and msgE cases for the typecheck function. In the language of the textbook, objE introduces an object (like lamE for functions) and msgE eliminates them (i.e. evaluates to one of the fields). Your solution should pass the following tests, including throwing errors for typing issues like using an known field name. Thus, the set of fields for a given object does not change after it is created.

Your completed typecheck function should pass the following tests. In order to re-use the same toy language fragments between tests, these tests make extensive use of quasiquote syntax.

(module+ test
  (define sampler `{obj {hello true}
                        {goodbye false}
                        {a-num 42}
                        {n-func {lam {x : num} x}}
                        {b-func {lam {x : bool} x}}
                        })
  (test (tc sampler)
        (objT (hash (list (pair 'hello (boolT))
                          (pair 'goodbye (boolT))
                          (pair 'a-num (numT))
                          (pair 'n-func (arrowT (numT) (numT)))
                          (pair 'b-func (arrowT (boolT) (boolT)))))))
  (test (tc `{msg ,sampler hello}) (boolT))
  (test/exn (tc `{msg 1 hello}) "object")
  (test/exn (tc `{msg ,sampler blah}) "unknown field")
  (define obj-fun `{lam {x : (obj (n-func (num -> num)))} {{msg x n-func} 3}})
  (test (tc obj-fun) (arrowT
                      (objT (hash (list (pair 'n-func (arrowT (numT) (numT))))))
                      (numT)))
  (test (tc `{,obj-fun {obj {n-func {lam {x : num} x}}}}) (numT))
  (test/exn (tc `{,obj-fun 2}) "argument type")
  (test/exn (tc `{if true ,obj-fun 2}) "branches")
  (test (tc `{rec {fact : (obj (run (num -> num)))}
                  {obj {run {lam {n : num}
                                 {if {<= n 0} 1 {* n {{msg fact run} {- n 1}}}}}}}
                  {{msg fact run} 10}})
        (numT))

  )

2. Structural typing

According to the substitution principle, we call type $X$ a subtype of type $Y$ of another if any value with type $X$ it can be safely used where some expression expects a value of type $Y$. Surprisingly, for our object types this means that the fields of $X$ are a superset of the fields of $Y$.

2.1 Write subtype?

Write a function subtype? the checks whether the first argument is a subtype of the second argument. This means that every field of the second argument must be present in the first argument with the matching type.

(module+ test
  (define hello-t (objT (hash (list (pair 'hello (numT))))))
  (define hello-goodbye-t (objT (hash (list
                                       (pair 'hello (numT))
                                       (pair 'goodbye (boolT))))))
  (test (subtype? (numT) (boolT)) #f)
  (test (subtype? (numT) (numT)) #t)
  (test (subtype? (numT) hello-t) #f)
  (test (subtype? hello-t (objT (hash (list (pair 'hello (boolT)))))) #f)
  (test (subtype? hello-goodbye-t hello-t) #t)
  (test (subtype? hello-t hello-goodbye-t) #f))

2.2 Use subtype?

Update the appE case of the typechecker to use subtype?, so that the following tests pass.

(module+ test
    (test (tc `{,obj-fun {obj {n-func {lam {x : num} x}}
                              {b-func {lam {x : bool} x}}}}) (numT))

    (test (tc `{let1 {f : {(obj (n-func (num -> num))) -> num}}
                     ,obj-fun
                     {f ,sampler}})
          (numT)))

Tests

Referring to the grading grading rubric for guidance, add any needed tests for your solution.

As always, make sure you have complete test coverage.