EECS 662

Programming Languages

Index
Blog

Project 4 - Type Checking

Project 4 - Adding Type Checking and Recursion EECS 662 - Programming Languages

The objective of this project is to add Boolean operations, type checking, and a fixed point operation to FBAE from Project 3. You will first add boolean operations to the FBAE interpreter by extending the AST and updating the evaluator. You will then add a fixed point operator to your AST and interpreter. Finally, you will define a type checker for the extended FBAE language and integrate type checking into the FBAE interpreter. Specifically, you will parse your FBAE expression, type check the resulting AST, elaborate to FBAE, and evaluate the result.

Exercise 1

The base language for this project is the extension of FBAE defined as follows:

FBAE ::= number |
         id |
         FBAE * FBAE  |
         FBAE - FBAE |
         FBAE * FBAE |
         FBAE / FBAE |
		 bind id = FBAE in FBAE |
         lambda (id:T) in FBAE |
         app FBAE FBAE |
         if FBAE then FBAE else FBAE |
         true | false |
         FBAE && FBAE |
         FBAE || FBAE |
         FBAE <= FBAE |
         isZero FBAE
 T ::= Num | Boolean | T -> T

None of these operations is new. We have implemented them in some form in earlier projects or in class.

  1. Implement and evaluator with the signature eval :: Env -> FBAE -> FBAValue that performs call-by-value function interpretation using static scoping. Your interpreter need only do minimal runtime error checking as it will be integrated with a type inference function later in the project.

  2. Using the eval function, implement a function interp :: String -> FBAEValue that parses its input and evaluates the resulting structure.

The syntax for lambda in FBAE includes specification of a type. Thus, Lambda has a placeholder for the domain type. While this will be populated by the parser and you must include types in your AST, they are ignored by the evaluator. Note specifically that ClosureV has no domain type specified. Think carefully about why this is the case.

A parser and data structures for FBAE are provided in the project utilities file. If you choose to you may continue to use the elaborator from Project 3 to implement bind and reuse your evaluator for CFAE. Alternatively, you may extend the CFAE interpreter to include bind as the beginning of your new interpreter.

Exercise 2

In this exercise you will add recursion to CFWAE by adding a fix operator to CFWAE. This is accomplished by adding the term:

fix FBAE

to the original FBAE language from Exercise 1. Note that the parser and AST provided for Project 4 already include these constructs. Thus, you need not change you parser or your AST for this exercise.

  1. Update your eval function from Exercise 1 to include the fix operation.

Your interp function need not be updated. Once again types must be included, but will be ignored by the evaluator and interpreter.

Exercise 3

In this exercise you will write a type checker for the FBAE language identical to that used in Project 2 with the addition of syntax for types.

  1. Write a function, typeof :: Cont -> FBAE -> TFBAE, that takes an FBAE data structure and returns its type given a context. If no type can be found, typeof should throw an error indicating why. Think of this as an interpreter that produces type values rather than traditional values.

An AST for the type values is included in the Project 3 utilities file.

Exercise 4

In this exercise you will put all the pieces together to write an interpreter for FBAE and its extensions.

  1. Combine your parser, typeof and eval functions into a function interp :: String -> FBAEValue that parses its input, finds the type of the result, and evaluates the result if a type is found.

Note that the type inference function is called after parsing, but before evaluation. Evaluation should only occur if type inference works.

Notes

You can get quite a bit of your code from class notes or the text. However, you will need to write typeof and eval cases for Boolean operations on your own.

Keep error checking in eval to a minimum. If the purpose of typeof is to predict errors, then very little error checking need be performed during evaluation. This is one advantage of type inference and type checking.

I strongly suggest writing this project either using error to throw errors or using the Either monad. You can use Either without treating it as a monad, but you will end up writing quite a bit more code. It’s not complicated, just bigger.

proj4Utils contains a parser and data structures for FBAE and TFBAE. Feel free to roll your own if you prefer. The parser utilities file used in previous projects is no longer needed. Just use the project utilities file by itself.

AST Structures

Following are the AST structures defined in the utilities file.

FBAE Abstract Syntax

data FBAE where
  Num :: Int -> FBAE
  Plus :: FBAE -> FBAE -> FBAE
  Minus :: FBAE -> FBAE -> FBAE
  Mult :: FBAE -> FBAE -> FBAE
  Div :: FBAE -> FBAE -> FBAE
  Bind :: String -> FBAE -> FBAE -> FBAE
  Lambda :: String -> TFBAE -> FBAE -> FBAE
  App :: FBAE -> FBAE -> FBAE
  Id :: String -> FBAE
  Boolean :: Bool -> FBAE
  And :: FBAE -> FBAE -> FBAE
  Or :: FBAE -> FBAE -> FBAE
  Leq :: FBAE -> FBAE -> FBAE
  IsZero :: FBAE -> FBAE
  If :: FBAE -> FBAE -> FBAE -> FBAE
  Fix :: FBAE -> FBAE
  deriving (Show,Eq)

FBAE Type Abstract Syntax

data TFBAE where
  TNum :: TFBAE
  TBool :: TFBAE
  (:->:) :: TFBAE -> TFBAE -> TFBAE
  deriving (Show,Eq)

FBAE Value Type

data FBAEVal where
  NumV :: Int -> FBAEVal
  BooleanV :: Bool -> FBAEVal
  ClosureV :: String -> FBAE -> EnvS -> FBAEVal
  deriving (Show,Eq)