[SOLVED] AgdaPLC: Homework 7

PLC: Homework 7 [90 points]

Due date: Wednesday, November 1, 9pm
3 extra-credit points if you turn in by Tuesday, October 31st, 9pm

About This Homework

For this homework, you will start implement operations on vectors in Agda, thus using internal verification to reason about how the lengths of vectors are affected by various operations.

How to Turn In Your Solution

You should create a hw7 subdirectory in your personal repo. You will copy files from subdirectories of the hw7 directory in the course repo.

As for previous homeworks, you can check that you have submitted correctly by going to the URL for your subversion repository. Remember to use exactly the file names we are requesting (so do not change the names of these files).

Partners Allowed

You may work by yourself or with one partner (no more). See the instructions from hw1 for details on how to submit your assignment if you work with a partner.

How To Get Help

You can post questions in the hw7 section on Piazza.
You are also welcome to come to our office hours. See the courses Google Calendar, linked from

the Resources tab of the Resources page on Piazza, for the locations and times for office hours.

1

1 Reading

Read Chapter 5 of Verified Functional Programming in Agda, available for free (on campus or VPN) here:

https://dl.acm.org/citation.cfm?id=2841316

2 Vector operations

In vector-todo.agda, you will find code in progress for various operations taken from Haskells Data.List package (see https://hackage.haskell.org/package/base-4.10.0.0/docs/Data-List. html), modified to work for vectors. You should write your code so that the functions in vector-todo.agda work as described for the corresponding functions of Data.List.

I have arranged the problems in order of what I believe is increasing difficulty. Each problem is worth 10 points (for 90 total). A couple notes:

For tailsV, spanV, and takeV, you get 4 points if you fill in the hole in the type, and the remaining 6 for defining the function.

insertionsV does not have a corresponding Data.List function (not that I noticed); see the comment in vector-todo.agda for what insertionsV is supposed to do.

For insertionsV, intersperseV, and permutationsV, you get 7 points for filling in the hole(s) in the type, and the remaining 3 for defining the function (intersperseV was a bit involved and I did not complete permutationsV yet but expect it to involve insertionsV). This means that if you cannot figure out how to write the code, you still get most of the points for figuring out how the code will affect the lengths of the vectors in question.

2