Project 4 - Fix and Type Checking

Note: This is a draft that is still being proofed.

This is the “put it all together” project. The objective is to add Boolean operations, state, 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 state for the extended FBAE language. S

As in earlier projects p4.hs contains function signatures and data structures for FBAE and its associated types, TFBAE. p4.hs also contains a test case for factorial to get you started.

Please note that I will only grade Exercise 4, the entire combined interpreter. The 4 exercises are laid out separately only to help you organize your project. If you choose, you may submit a solution that only contains the final FBAE interpreter.

Exercise 1 (Ungraded)

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 |
         lambda (id:T) in FBAE |
         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. You are taking the things we’ve learned so far and assembling them into a single language.

Implement and evaluator with the signature evalM :: Env -> FBAE -> (Maybe FBAVal) 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.

The syntax for lambda in FBAE includes specification of a type. Thus, Lambda has a placeholder for the domain type. While this would be populated by the parser if we were using one 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.

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. You are welcome to start from scratch. This is completely up to you.

Exercise 2 (Ungraded)

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

fix FBAE

to the original FBAE language from Exercise 1. Note that the AST provided for Project 4 already includes this construct. Thus, you need not change your AST for this exercise.

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

Exercise 3 (Ungraded)

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.

Write a function, typeofM :: Cont -> FBAE -> (Maybe TFBAE), that takes an FBAE data structure and returns its type given a context. If no type can be found, typeofM should return Nothing. Think of this as an evaluator that produces type values rather than traditional values.

An AST for the type values is included in the Project 4 template file.

Exercise 4 (Graded)

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

Combine your typeofM and evalM functions into a function interp :: FBAE -> (Maybe FBAEVal) that finds the type of the input AST and evaluates the result if a type is found.

Note that the type inference function is called before evaluation. Evaluation should only occur if type inference returns a type.

Exercise 5 (Bonus)

In this exercise you will add state to your interpreter from Exercise 3. To do this you will add the operations presented in class for allocating, setting, and dereferencing locations plus the function for sequencing execution:

new FBAE |
set FBAE FBAE |
deref FBAE |
FBAE ; FBAE

You will also need to add a new value for locations and type for locations. Note that we did not discuss typing locations in class, but it is not difficult to add.

Give that this is a bonus question and intended to be challenging, you will need to extend types and signatures for the type checker and interpreter yourself.

Notes

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

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

AST Structures

Following are the AST structures defined in the template 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)

EECS 662

Programming Languages