CS 5510 Homework 9

Due: Thursday, November 10th, 2011 10:45am

Install plai-typed.plt to use the PLAI Typed language.

Part 1 – True, False, equals, and if

Start with tfae-t.rkt. The implementation already includes a boolean type, but no expressions of boolean type.

Add support for true, false, {= ... ...}, and {if ... ... ...} expressions, where = produces a boolean given two numbers, and if requires a boolean expression for the test.

The examples below use suggested constructor names. If you use different names, then adjust the tests. You don't need to write a parser; just test directly on abstract syntax.

Examples:

  (test (interp (eq (num 13)
                    (ifthenelse (eq (num 1) (add (num -1) (num 2)))
                                (num 12)
                                (num 13)))
                (mtSub))
         (boolV false))

  (test (typecheck (eq (num 13)
                       (ifthenelse (eq (num 1) (add (num -1) (num 2)))
                                   (num 12)
                                   (num 13)))
                   (mtEnv))
         (boolT))

  (test/exn (typecheck (add (num 1)
                            (ifthenelse (bool true)
                                        (bool true)
                                        (bool false)))
                       (mtEnv))
            "no type")

Part 2 – Pairs

Implement {pair ... ...}, {fst ...}, and {snd ...} expressions as shown in lecture for TPFAE (but not implemented in lecture).

Examples:

  (test (interp (fst (pair (num 10) (num 8)))
                (mtSub))
        (numV 10))
  (test (interp (snd (pair (num 10) (num 8)))
                (mtSub))
        (numV 8))

  (test (typecheck (pair (num 10) (num 8))
                   (mtEnv))
        (crossT (numT) (numT)))
  (test (typecheck (add (num 1) (snd (pair (num 10) (num 8))))
                   (mtEnv))
        (numT))

  (test (typecheck (fun 'x (crossTE (numTE) (boolTE))
                    (ifthenelse (snd (id 'x)) (num 0) (fst (id 'x))))
                   (mtEnv))
       (arrowT (crossT (numT) (boolT)) (numT)))

  (test/exn (typecheck (fst (num 10)) (mtEnv))
            "no type")
  (test/exn (typecheck (add (num 1) (fst (pair (bool false) (num 8))))
                       (mtEnv))
            "no type")
  (test/exn (typecheck (fun 'x (crossTE (numTE) (boolTE))
                             (ifthenelse (fst (id 'x)) (num 0) (fst (id 'x))))
                       (mtEnv))
            "no type")

Part 3 – Functions that Accept Multiple Arguments, Yet Again

With pairs, functions can accept multiple arguments by accepting paired values, but we can also add direct support for multiple arguments.

Change the interpreter to allow multiple function arguments and multiple arguments at function calls. The grammar of the language is now as follows:

  <TMFAE> = <number>
          | true
          | false
          | {+ <TMFAE> <TMFAE>}
          | {- <TMFAE> <TMFAE>}
          | {= <TMFAE> <TMFAE>}
          | <id>
          | {if <TMFAE> <TMFAE> <TMFAE>}
          | {fun {[<id> : <tyexp>]*} <TMFAE>}
          | {<TMFAE> <TMFAE>*}
          | {pair <TMFAE> <TMFAE>}
          | {fst <TMFAE>}
          | {snd <TMFAE>}

To support this grammar, change the fun/Fun and app/App constructors in FAE/fae, and the arrowTE/ArrowTE constructor in TE/te (plus other constructors that do not represent the input program):

  (define-type FAE
    ...
    [fun (params : (listof symbol))
         (argtys : (listof TE))
         (body : FAE)]
    [app (fun-expr : FAE)
         (arg-exprs : (listof FAE))]
    ...)

  (define-type TE
    ...
    [arrowTE (args : (listof TE))
             (result : TE)]
    ...)
  

Examples:

  (test (interp (app (fun (list) (list) (num 10)) (list))
               (mtSub))
        (numV 10))
  (test (interp (app (fun (list 'x 'y) (list (numTE) (numTE))
                          (sub (id 'x) (id 'y)))
                     (list (num 10) (num 20)))
                (mtSub))
        (numV -10))

  (test (typecheck (app (fun (list 'x 'y) (list (numTE) (boolTE))
                             (id 'y))
                        (list (num 10) (bool false)))
                   (mtEnv))
        (boolT))
  (test/exn (typecheck (app (fun (list 'x 'y) (list (numTE) (boolTE))
                             (id 'y))
                        (list (num 10) (num 10)))
                       (mtEnv))
            "no type")