Assignment 5 – Agda

The GitHub Classrooms link for this assignment is https://classroom.github.com/a/BWok5loM.

The deadline for the assignment is shown on the schedule. The deadline for the peer reviews is shown on the schedule.

Exercise 1 – Programming to spec (5 pt)

Complete the definitions in ListLib.agda, FinLib.agda, MatrixLib.agda, and GMatrixLib.agda.

Each hole is worth 0.2 pt.

Exercise 2 – Refactoring (1 pt)

In ListProperties, avoid passing the argument f argument around, by moving it into a module parameter. Ensure that you do not make functions depend on f which do not actually use f. (0.2 pt)

In ListLib, de-sugar the variable block into extra implicit arguments for the appropriate functions. (0.2 pt)

In MatrixLib, write a variable block to replace all the manually-written implicit arguments. (0.2 pt)

In MatrixLib, give every argument of the function scale both a name and a type. (0.2 pt)

In FinLib, rewrite the type of enumerate-is-complete to omit the type of the argument f. (0.2 pt)

Exercise 3 – Generalizing (2 pt)

Generalize the definitions from MatrixLib.agda to work with the GMatrix A type instead of the Matrix type.

Put the modified definitions in the GMatrixLib.agda file.

Ensure that each definition only takes extra arguments that it actually uses. For example, your generalized print function should not take an argument for adding As, and your generalized mul function should not take an argument for printing As.

Ensure that your definitions remain readable (hint: Agda has typeclasses)

These definitions are worth 0.1 pt: Vec,to-List,_!_,transpose,row,col

These definitions are worth 0.2 pt: print,_^_,mul,_∙_,scale,add,id

Exercise 4 – Type design (2 pt)

In the file PermutationLib.agda, implement the Perm type, and any helper definitions it requires.

You may choose how to implement Perm (e.g. using data, record, function types, application, pattern-matching, etc.).

Also complete the other definitions in the file.

A correct definition of Perm is worth 1 pt, the other holes are worth 0.2 pt each.