Dependent Types Assignment 4

In this assignment, you'll practice working with total functions dependently typed functions, mostly over vectors. The Pie exercises cover Chapters 6 and 7. You'll also extend your normalizer into a normalizer using typed normalization by evaluation, and work on a type checker.

The Pie assignment should be completed by writing a definition for each claim, and then uncommenting the tests so that they all pass. Passing the tests is necessary, but not sufficient, for completing the exercise - you should also follow the instructions in the file.

1. Start from this file, which contains the Pie exercises
2. I'll provide a skeleton of the normalizer and type checker in Haskell and Racket. You may choose any language at all to implement your evaluator, but these files may provide a starting point.
3. Submit your 4.pie and your evaluator implementation, as a .zip archive with all files on Gradescope.

Parts of this assignment are written by David Christiansen and used with permission.