[Agda] Agda assessed exercises

[Sam Staton]

I'd like to share a bit of teaching experience with you. As part of a  
graduate course on Categorical Logic, I asked my students to learn  
Agda as a way of learning dependent type theory. I then gave them an  
exam: see exam.agda in
http://www.cl.cam.ac.uk/teaching/0910/L20/agda/
(Please don't mirror it.)

It is difficult to understand how people learn dependent type theory  
for the first time, but it is important, especially if we can make  
this easier.

The students had a week to complete the exercises in the exam. I gave  
them a basic introduction, pointed them to some tutorials, and then  
left them to get on with it, offering one-to-one advice where  
necessary. All six students got full marks for the exam, which  
accounts for 25% of the marks for this module. I asked them for  
feedback, which is at the bottom of this message, in case it is  
helpful to developers or future teachers.

Sam.


--

Questionnaire.

 > How many hours did it take you to learn Agda and solve the  
exercises  (roughly)?

Answers were between 12 and 30 hours, averaging 20 hours.

 > What was the hardest language feature?

* Lack of good pattern matching! Makes it painful to deconstruct  
values, especially when you have Maybe's floating around.
* dependent type.
* To get the definitions right and to know what is allowed and what not.
* It was hard to find a difference between Types and Terms. It was  
unclear if an expression was a Type or a Term.
* Families of sets idea, I think. Getting to know how to use records  
properly.

 > What advice would you give to someone who is about to start  
learning Agda?

* Starting with simple exercise and practice.
* Read a quick and dirty tutorial first to get an idea what it is like  
to use agda, then practice, practice, practice.
* Given tutorial "Dependently Typed Programming in Agda" is a good  
start. I would suggest to read it thoroughly before writing any Agda.
* I wish I'd gotten more proficient with using the Agda/emacs  
environment earlier, might've saved a bit of time for some questions.
* Just sit down and try to write something. Tutorials aren't very  
clear, because they're mostly research papers. At this moment, one has  
to figure things out by oneself.

 > Would you ever consider using Agda again?

All students answered "yes".