Number of watchers on Github  55 
Number of open issues  0 
Average time to close an issue  6 days 
Main language  Agda 
Average time to merge a PR  3 days 
Open pull requests  0+ 
Closed pull requests  0+ 
Last commit  over 4 years ago 
Repo Created  almost 5 years ago 
Repo Last Updated  over 1 year ago 
Size  1.48 MB 
Organization / Author  pigworker 
Contributors  2 
Page Updated  20180321 
Do you use CS41014? Leave a review!  
View CS41014 activity  
View on github  
Fresh, new opensource launches 🚀🚀🚀  
Trendy new open source projects in your inbox!
View examples

This repository contains the materials for CS410 Advanced Functional Programming in the 201415 session. The class runs through semesters 1 and 2, with most of its teaching and assessment activity completed already in semester 1. Accordingly, for ease of reference, this page includes the exercises so far, and is intended to be a reasonably selfcontained account of how the class works.
CS410 is assessed entirely by coursework. It runs for all 15 weeks of
semester 1, in which there are 5 exercises, each lasting 3 weeks and
worth 15% of the class score, then it suspends for the 10 project
weeks of semester 2, before resuming in the last 5 weeks of semester 2
for a single capstone
exercise worth 25% of the class score.
The class is about programming in the advanced functional language,
Agda. Teaching is largely showandtell: I introduce concepts and
illustrate them with live programming
in the classroom. Agda
supports development by interactive typedirected refinementfilling
in holes
. Exercises thus consist of incomplete programs, to be
finished appropriately by each student. They are distributed via this
public code repository on GitHub. The students work in lab sessions
which I supervise: often, the discussion which breaks out in the lab
once they are handson with a problem is how the real learning
happens. The students each have their own private branch of the
repository on BitBucket, to which they invite me as a collaborator
whilst keeping everyone else out. After each deadline, the students
make individual appointments to see me, where we work through their
code. I quiz them about it, grade it, and issue oral feedback.
This is a challenging class, but the students are bright and enthusiastic for a challenge, having done well at the corresponding third year Haskell class. The precise direction and choice of material is informed by the progress the class makes as we go. This year, I was pleasantly surprised by their willingness to engage with some quite deep concepts.
The semester 1 exercises were as follows.
The exercise files, mark schemes and specimen solutions for exercises 14 are included below. For exercise 5, the main exercise file and the mark scheme is included.
At time of writing, exercise 6 is under construction. It will be issued to students at the start of the Easter break, giving them some chance of a head start. It will amount to
overlayingstructure, with a clear visual intuition (10 marks)
The exercises tend to be quite structured, designed to promote the grasping of key concepts. How far they get depends on their ability and determination to struggle to an understanding. They get out what they put in.
Below are the relevant files for the first 5 exercises.
problem file
module Ex1 where
open import Ex1Prelude
{}
{ Name: }
{}
{}
{ DEADLINE: Week 3 Monday 13 October 23:59 (preferably by BitBucket) }
{}
{
TOP TIP: if you have annoyingly many open goals, comment out big chunks of the
file with a multiline comment a bit like this one.
}
{}
{ 1.1: Tree Sort }
{}
 1.1.1 implement concatenation for lists
_++_ : {X : Set} > List X > List X > List X
xs ++ ys = {!!}
infixr 3 _++_
 a datatype of nodelabelled binary trees is given as follows
data Tree (X : Set) : Set where
leaf : Tree X
_<[_]>_ : Tree X > X > Tree X > Tree X
{
data Tree x = Leaf  Node (Tree X) X (Tree X)
Leaf :: Tree x
Node :: Tree x > x > Tree x > Tree x
}
demoTree : Tree Nat
demoTree = ({!!} <[ 3 ]> {!!}) <[ 5 ]> {!!}
 1.1.2 implement the insertion of a number into a tree, ensuring that
 the numbers in the tree are in increasing order from left to right;
 make sure to retain duplicates
insertTree : Nat > Tree Nat > Tree Nat
insertTree x t = {!!}
 1.1.3 implement the function which takes the elements of a list and
 builds an ordered tree from them, using insertTree
makeTree : List Nat > Tree Nat
makeTree xs = {!!}
 1.1.4 implement the function which flattens a tree to a list,
 using concatenation
flatten : {X : Set} > Tree X > List X
flatten t = {!!}
 1.1.5 using the above components, implement a sorting algorithm which
 works by building a tree and then flattening it
treeSort : List Nat > List Nat
treeSort = {!!}
 1.1.6 give a collection of unit tests which cover every program line
 from 1.1.1 to 1.1.5
 1.1.7 implement a fast version of flatten, taking an accumulating parameter,
 never using ++. and ensuring that the law

 fastFlatten t xs == flatten t ++ xs

 is true; for an extra style point, ensure that the accumulating parameter
 is never given a name in your program
fastFlatten : {X : Set} > Tree X > List X > List X
fastFlatten t = {!!}
 1.1.8 use fastFlatten to build a fast version of tree sort
fastTreeSort : List Nat > List Nat
fastTreeSort xs = {!!}
 1.1.9 again, give unit tests which cover every line of code
{}
{ 1.2: Shooting Propositional Logic Fish In A Barrel }
{}
 1.2.1 implement the following operations; try to use only
 [Cc Cc] and [Cc Ca]
orCommute : {A B : Set} > A /+/ B > B /+/ A
orCommute x = {!!}
orAbsorbL : {A : Set} > Zero /+/ A > A
orAbsorbL x = {!!}
orAbsorbR : {A : Set} > A /+/ Zero > A
orAbsorbR x = {!!}
orAssocR : {A B C : Set} > (A /+/ B) /+/ C > A /+/ (B /+/ C)
orAssocR x = {!!}
orAssocL : {A B C : Set} > A /+/ (B /+/ C) > (A /+/ B) /+/ C
orAssocL x = {!!}
 1.2.2 implement the following operations; try to use only
 [Cc Cc] and [Cc Ca]
andCommute : {A B : Set} > A /*/ B > B /*/ A
andCommute x = {!!}
andAbsorbL : {A : Set} > A > One /*/ A
andAbsorbL x = {!!}
andAbsorbR : {A : Set} > A > A /*/ One
andAbsorbR x = {!!}
andAssocR : {A B C : Set} > (A /*/ B) /*/ C > A /*/ (B /*/ C)
andAssocR x = {!!}
andAssocL : {A B C : Set} > A /*/ (B /*/ C) > (A /*/ B) /*/ C
andAssocL x = {!!}
 how many times is [Cc Cc] really needed?
 1.2.3 implement the following operations; try to use only
 [Cc Cc] and [Cc Ca]
distribute : {A B C : Set} > A /*/ (B /+/ C) > (A /*/ B) /+/ (A /*/ C)
distribute x = {!!}
factor : {A B C : Set} > (A /*/ B) /+/ (A /*/ C) > A /*/ (B /+/ C)
factor x = {!!}
 1.2.4 try to implement the following operations; try to use only
 [Cc Cc] and [Cc Ca]; at least one of them will prove to be
 impossible, in which case you should comment it out and explain
 why it's impossible
Not : Set > Set
Not X = X > Zero
deMorgan1 : {A B : Set} > (Not A /+/ Not B) > Not (A /*/ B)
deMorgan1 x y = {!!}
deMorgan2 : {A B : Set} > Not (A /*/ B) > (Not A /+/ Not B)
deMorgan2 x = {!!}
deMorgan3 : {A B : Set} > (Not A /*/ Not B) > Not (A /+/ B)
deMorgan3 x y = {!!}
deMorgan4 : {A B : Set} > Not (A /+/ B) > (Not A /*/ Not B)
deMorgan4 x = {!!}
 1.2.5 try to implement the following operations; try to use only
 [Cc Cc] and [Cc Ca]; at least one of them will prove to be
 impossible, in which case you should comment it out and explain
 why it's impossible
dnegI : {X : Set} > X > Not (Not X)
dnegI = {!!}
dnegE : {X : Set} > Not (Not X) > X
dnegE = {!!}
neg321 : {X : Set} > Not (Not (Not X)) > Not X
neg321 = {!!}
hamlet : {B : Set} > B /+/ Not B
hamlet = {!!}
nnHamlet : {B : Set} > Not (Not (B /+/ Not B))
nnHamlet = {!!}
specimen solution and mark scheme
module Ex1Sol where
open import Ex1Prelude
{}
{ Name: Conor McSpecimen }
{}
{}
{ DEADLINE: Week 3 Monday 13 October 23:59 (preferably by BitBucket) }
{}
{
TOP TIP: if you have annoyingly many open goals, comment out big chunks of the
file with a multiline comment a bit like this one.
}
{ Mark scheme:
The programming for each part is worth one mark.
the explanation of why the impossible cases are impossible is worth
one mark.
The total number of available marks is 15.
}
{}
{ 1.1: Tree Sort }
{}
 1.1.1 implement concatenation for lists
_++_ : {X : Set} > List X > List X > List X
[] ++ ys = ys
x :> xs ++ ys = x :> (xs ++ ys)
infixr 3 _++_
 a datatype of nodelabelled binary trees is given as follows
data Tree (X : Set) : Set where
leaf : Tree X
_<[_]>_ : Tree X > X > Tree X > Tree X
{
data Tree x = Leaf  Node (Tree X) X (Tree X)
Leaf :: Tree x
Node :: Tree x > x > Tree x > Tree x
}
demoTree : Tree Nat
demoTree = (leaf <[ 3 ]> leaf) <[ 5 ]> leaf
 1.1.2 implement the insertion of a number into a tree, ensuring that
 the numbers in the tree are in increasing order from left to right;
 make sure to retain duplicates
insertTree : Nat > Tree Nat > Tree Nat
insertTree x leaf = leaf <[ x ]> leaf
insertTree x (l <[ y ]> r) with x <= y  or use if_then_else_
insertTree x (l <[ y ]> r)  tt = insertTree x l <[ y ]> r
insertTree x (l <[ y ]> r)  ff = l <[ y ]> insertTree x r
 1.1.3 implement the function which takes the elements of a list and
 builds an ordered tree from them, using insertTree
makeTree : List Nat > Tree Nat
makeTree [] = leaf
makeTree (x :> xs) = insertTree x (makeTree xs)
 1.1.4 implement the function which flattens a tree to a list,
 using concatenation
flatten : {X : Set} > Tree X > List X
flatten leaf = []
flatten (l <[ x ]> r) = flatten l ++ x :> flatten r
 1.1.5 using the above components, implement a sorting algorithm which
 works by building a tree and then flattening it
treeSort : List Nat > List Nat
treeSort = flatten o makeTree
 1.1.6 give a collection of unit tests which cover every program line
 from 1.1.1 to 1.1.5
treeSortTest : treeSort (1 :> 5 :> 2 :> 4 :> 3 :> [])
== (1 :> 2 :> 3 :> 4 :> 5 :> [])
treeSortTest = refl
 1.1.7 implement a fast version of flatten, taking an accumulating parameter,
 never using ++. and ensuring that the law

 fastFlatten t xs == flatten t ++ xs

 is true;
{
fastFlatten : {X : Set} > Tree X > (List X > List X)
fastFlatten leaf xs
 = flatten leaf ++ xs  by specification
 = [] ++ xs  definition of flatten
= xs  definition of ++
fastFlatten (l <[ x ]> r) xs
 = flatten (l <[ x ]> r) ++ xs  by specification
 = (flatten l ++ x :> flatten r) ++ xs  definition of flatten
 = flatten l ++ x :> flatten r ++ xs  ++ is associative
 = flatten l ++ x :> fastFlatten r xs  by specification
= fastFlatten l (x :> fastFlatten r xs)  by specification
}
 for an extra style point, ensure that the accumulating parameter
 is never given a name in your program
fastFlatten : {X : Set} > Tree X > (List X > List X)
fastFlatten leaf = id
fastFlatten (l <[ x ]> r) = (fastFlatten l) o (_:>_ x) o (fastFlatten r)
 1.1.8 use fastFlatten to build a fast version of tree sort
fastTreeSort : List Nat > List Nat
fastTreeSort xs = fastFlatten (makeTree xs) []
 1.1.9 again, give unit tests which cover every line of code
fastTreeSortTest : fastTreeSort (1 :> 5 :> 2 :> 4 :> 3 :> [])
== (1 :> 2 :> 3 :> 4 :> 5 :> [])
fastTreeSortTest = refl
{}
{ 1.2: Shooting Propositional Logic Fish In A Barrel }
{}
 1.2.1 implement the following operations; try to use only
 [Cc Cc] and [Cc Ca]
orCommute : {A B : Set} > A /+/ B > B /+/ A
orCommute (inl a) = inr a
orCommute (inr b) = inl b
orAbsorbL : {A : Set} > Zero /+/ A > A
orAbsorbL (inl ())
orAbsorbL (inr a) = a
orAbsorbR : {A : Set} > A /+/ Zero > A
orAbsorbR (inl a) = a
orAbsorbR (inr ())
orAssocR : {A B C : Set} > (A /+/ B) /+/ C > A /+/ (B /+/ C)
orAssocR (inl (inl a)) = inl a
orAssocR (inl (inr b)) = inr (inl b)
orAssocR (inr c) = inr (inr c)
orAssocL : {A B C : Set} > A /+/ (B /+/ C) > (A /+/ B) /+/ C
orAssocL (inl a) = inl (inl a)
orAssocL (inr (inl b)) = inl (inr b)
orAssocL (inr (inr c)) = inr c
 1.2.2 implement the following operations; try to use only
 [Cc Cc] and [Cc Ca]
andCommute : {A B : Set} > A /*/ B > B /*/ A
andCommute (a , b) = b , a
andAbsorbL : {A : Set} > A > One /*/ A
andAbsorbL a = <> , a
andAbsorbR : {A : Set} > A > A /*/ One
andAbsorbR a = a , <>
andAssocR : {A B C : Set} > (A /*/ B) /*/ C > A /*/ (B /*/ C)
andAssocR ((a , b) , c) = a , (b , c)
andAssocL : {A B C : Set} > A /*/ (B /*/ C) > (A /*/ B) /*/ C
andAssocL (a , (b , c)) = (a , b) , c
 how many times is [Cc Cc] really needed?
 NEVER, but I'd rather use patterns than projections
 1.2.3 implement the following operations; try to use only
 [Cc Cc] and [Cc Ca]
distribute : {A B C : Set} > A /*/ (B /+/ C) > (A /*/ B) /+/ (A /*/ C)
distribute (a , inl b) = inl (a , b)
distribute (a , inr c) = inr (a , c)
factor : {A B C : Set} > (A /*/ B) /+/ (A /*/ C) > A /*/ (B /+/ C)
factor (inl (a , b)) = (a , inl b)
factor (inr (a , c)) = (a , inr c)
 1.2.4 try to implement the following operations; try to use only
 [Cc Cc] and [Cc Ca]; at least one of them will prove to be
 impossible, in which case you should comment it out and explain
 why it's impossible
Not : Set > Set
Not X = X > Zero
deMorgan1 : {A B : Set} > (Not A /+/ Not B) > Not (A /*/ B)
deMorgan1 (inl na) (a , b) = na a
deMorgan1 (inr nb) (a , b) = nb b
{
All I know is that A and B are not both true. That does not tell
me which of the two is false. To give a value in S /+/ T, I must
come off the fence and choose either the inl constructor and give
an S value or the inr constructor with a T. I can't just say "well,
I'm sure it isn't neither of those".
deMorgan2 : {A B : Set} > Not (A /*/ B) > (Not A /+/ Not B)
deMorgan2 x = inl (\ a > {!!})
Closer to the detail, a value of type Not (A /*/ B) is really a
function of type (A /*/ B) > Zero, so I can never get any actual
data out of it that would help me come off the fence. If I plump
for one side (inl, above), I get offered an A, but that isn't
enough to make use of the hypoothesis.
}
deMorgan3 : {A B : Set} > (Not A /*/ Not B) > Not (A /+/ B)
deMorgan3 (na , nb) (inl a) = na a
deMorgan3 (na , nb) (inr b) = nb b
deMorgan4 : {A B : Set} > Not (A /+/ B) > (Not A /*/ Not B)
deMorgan4 n = (\ a > n (inl a)) , (\ b > n (inr b))
 1.2.5 try to implement the following operations; try to use only
 [Cc Cc] and [Cc Ca]; at least one of them will prove to be
 impossible, in which case you should comment it out and explain
 why it's impossible
dnegI : {X : Set} > X > Not (Not X)
dnegI = \ x nx nx x
{
dnegE : {X : Set} > Not (Not X) > X
dnegE = {!!}
Just because you can't prove that X's don't exist, it doesn't mean
you actually know how to compute an X.
}
neg321 : {X : Set} > Not (Not (Not X)) > Not X
neg321 = nnx x nnx \ nx > nx x
{
hamlet : {B : Set} > B /+/ Not B
hamlet = {!!}
For any proposition (e.g., the halting of a Turing machine), that
we can encode as a Set, hamlet promises to compute whether or not
it has a proof. That's far cleverer than a real computer.
}
nnHamlet : {B : Set} > Not (Not (B /+/ Not B))
nnHamlet z = z (inr (\ b > z (inl b)))
{ Just for fun... }
DEMORGAN2 : Set1
DEMORGAN2 = {A B : Set} > Not (A /*/ B) > (Not A /+/ Not B)
DNEGE : Set1
DNEGE = {X : Set} > Not (Not X) > X
HAMLET : Set1  also known as "the law of the excluded middle"
HAMLET = {B : Set} > B /+/ Not B  or "tertium non datur" (third (way) not given)
 and one more variation, Peirce's Law, also a classical truth
PEIRCE : Set1
PEIRCE = {P Q : Set} > ((P > Q) > P) > P
 DNEGE, PEIRCE and HAMLET are equivalent
imp1 : DNEGE > HAMLET
imp1 dne = dne nnHamlet
imp2 : HAMLET > PEIRCE
imp2 h {P} {Q} pqp with h {P}
imp2 h pqp  inl p = p
imp2 h pqp  inr np = pqp (\ p > magic (np p)) where
imp3 : PEIRCE > DNEGE
imp3 peirce nnx = peirce (\ nx > magic (nnx nx))
 they all imply DEMORGAN2
impDeMorgan : DNEGE > DEMORGAN2
impDeMorgan dne nab = dne (\ z > z (inl (\ a > z (inr (\ b nab (a , b))))))
 but (and sorry if I led some of you to believe the opposite)
 DEMORGAN2 is weaker than the others, because you can only
 get one bit at at time
{ So, the business of constructing values as evidence for
propositions corresponds to functional programming in a "total"
language, but it doesn't give us quite the same logic as the
Boolean logic we teach you when you start. That logic (aka
"classical logic") makes "true" some things which do not correspond
to computations.
The logic you get here is sometimes called "constructive logic"
because we ask not "is it true?" but "can you make the evidence?".
FUN FACT (due to Kurt Goedel): if something is true, classically,
you can prove that it's not false, constructively.
WEIRD POSSIBILITY: there are such things as "anticlassical" logics
which are even more constructive, in which things like HAMLET are
actually false; these logics build in the idea that the *only*
truths arise by construction.
}
problem file
module Ex2 where
{
Name:
}
{
CS410 Exercise 2, due 5pm on Monday of Week 6 (3 November 2014)
NOTE: I am well aware that week 6 is quite busy with deadlines,
what with CS408related obligations and so on. I'd much prefer
you did things to the best of your ability rather than on time,
so I would be sympathetic to requests for some flexibility.
Still, your best bet is to make an early start rather than a
late finish.
}
{
This exercise is based around extending Hutton's razor with Boolean
values and conditional expressions. By introducing a second value
type, we acquire the risk of type mismatch. The idea here is to
explore different approaches to managing that risk.
}
open import Ex1Prelude
open import Ex2Prelude
{ The extended Hutton's Razor syntax }
data HExpIf : Set where
num : Nat > HExpIf
boo : Two > HExpIf
_+++_ : HExpIf > HExpIf > HExpIf
hif_then_else_ : HExpIf > HExpIf > HExpIf > HExpIf
{ Note that an expression
hif eb then ex1 else ex2
makes sense only when
* eb produces a Boolean value
* ex1 and ex2 produce the same sort of value (numeric or Boolean)
}
HValIf : Set
HValIf = Two /+/ Nat
{ We now have the risk of run time type errors. Let's introduce a type
for things which can go wrong. }
data Error (E X : Set) : Set where
ok : X > Error E X
error : E > Error E X
{ 2.1 Add a constructor to the following datatype for each different
kind of run time error that can happen. (Come back to this exercise
when you're writing the evaluator in 2.3.) Make these error reports
as informative as you can.
}
data EvalError : Set where
 your constructors here
{ 2.2 Write a little piece of "glue code" to make it easier to manage
errors. The idea is to combine errorprone process in *sequence*, where
the second process can depend on the value produced by the first if it
succeeds. The resulting process is, of course, also errorprone, failing
as soon as either component fails.
}
_>>=_ : {E S T : Set}
> Error E S  process which tries to get an S
> (S > Error E T)  given an S, process which tries for a T
> Error E T  combined in sequence
es >>= s2et = {!!}
{ 2.3 Implement an evaluator for HExpIf. Be sure to add only numbers and
to branch only on Booleans. Report type mismatches as errors. You should
use _>>=_ to help with the propagation of error messages.
}
eval : HExpIf > Error EvalError HValIf
eval e = {!!}
{ Note that the type of eval is not specific about whether the value
expected is numeric or Boolean. It may help to introduce auxiliary
definitions of errorprone processes which are "ok" only for the
type that you really want.
}
{ Next up, stack machine code, and its execution. }
data HBCode : Set where
PUSHN : Nat > HBCode
PUSHB : Two > HBCode
ADD : HBCode
_SEQ_ : HBCode > HBCode > HBCode
_IFPOP_ : HBCode > HBCode > HBCode
{ The intended behaviour of (t IFPOP f) is as follows
* pop the (we hope) Boolean value from top of stack
* if it's tt, execute t, else execute f
* whichever branch is executed, it gets the popped stack to start
}
{ 2.4 Populate the type of possible execution errors and implement the
execution behaviour of HBCode, operating on a stack represented as
a list of HValIf values.
}
data ExecError : Set where
 your constructors here
exec : HBCode > List HValIf > Error ExecError (List HValIf)
exec c s = {!!}
{ Next, we take a look at code generation and type safety. }
data HTy : Set where  we have two types in HExpIf
NUM BOOL : HTy
_=HTy=_ : HTy > HTy > Two  we can test if two types are equal
NUM =HTy= NUM = tt
NUM =HTy= BOOL = ff
BOOL =HTy= NUM = ff
BOOL =HTy= BOOL = tt
{ 2.5 Write a typesynthesizing compiler, computing both the HTy type and
the HBCode executable for a given expression. Your compiler should
give an informative error report if the expression it receives is
ill typed. Your compiler should also ensure (at least informally) that
the code produced will never trigger any execution errors.
}
data CompileError : Set where
 your constructors here
compile : HExpIf > Error CompileError (HTy /*/ HBCode)
compile (num x) = {!!}
compile (boo x) = {!!}
compile (e1 +++ e2) = compile e1 >>= \
{ (BOOL , c1) > error {!!}
; (NUM , c1) > {!!}
}
compile (hif e then e else e) = {!!}
{ You have a little bit more room for creative problemsolving in what's
left of the exercise. The plan is to build the type system into expressions
and code, the same way we did with plain Hutton's Razor in class.
}
{ If we *know* which HTy type we want, we can compute which Agda type we
expect our value to take. }
HVal : HTy > Set
HVal NUM = Nat
HVal BOOL = Two
{ 2.6 Finish the type of typed expressions. You should ensure that only
well HTytyped expressions can be constructed. }
data THExpIf : HTy > Set where
val : {t : HTy} > HVal t > THExpIf t
 you fill in addition and ifthenelse
{ 2.7 Implement a typesafe evaluator. }
teval : {t : HTy} > THExpIf t > HVal t
teval e = {!!}
{ 2.8 Implement a type checker. }
data TypeError : Set where
 your constructors here
tcheck : (t : HTy) > HExpIf > Error TypeError (THExpIf t)
tcheck t e = {!!}
{ 2.9 Adapt the technique from Hutton.agda to give a typesafe underflowfree
version of HBCode. You will need to think what is a good type to represent
the "shape" of a stack: before, we just used Nat to represent the *height* of
the stack, but now we must worry about types. See next question for a hint. }
data THBCode : { your indices here } Set where
 your constructors here
{ 2.10 Implement the execution semantics for your code. You will need to think
about how to represent a stack. The Ex2Prelude.agda file contains a very
handy piece of kit for this purpose. You write the type, too. }
 your code here
{ 2.11 Write the compiler from well typed expressions to safe code. }
tcompile : {t : HTy} > THExpIf t > {!!}
tcompile e = {!!}
specimen solution and mark scheme
module Ex2Sol where
{
Name: Conor McSpecimen
}
{
CS410 Exercise 2, due 5pm on Monday of Week 6 (3 November 2014)
NOTE: I am well aware that week 6 is quite busy with deadlines,
what with CS408related obligations and so on. I'd much prefer
you did things to the best of your ability rather than on time,
so I would be sympathetic to requests for some flexibility.
Still, your best bet is to make an early start rather than a
late finish.
}
{
This exercise is based around extending Hutton's razor with Boolean
values and conditional expressions. By introducing a second value
type, we acquire the risk of type mismatch. The idea here is to
explore different approaches to managing that risk.
}
{ Mark scheme
Each part is worth one mark each, apart from the four labelled
as worth two. The total number of marks available is 15.
}
open import Ex1Prelude
open import Ex2Prelude
{ The extended Hutton's Razor syntax }
data HExpIf : Set where
num : Nat > HExpIf
boo : Two > HExpIf
_+++_ : HExpIf > HExpIf > HExpIf
hif_then_else_ : HExpIf > HExpIf > HExpIf > HExpIf
{ Note that an expression
hif eb then ex1 else ex2
makes sense only when
* eb produces a Boolean value
* ex1 and ex2 produce the same sort of value (numeric or Boolean)
}
HValIf : Set
HValIf = Two /+/ Nat
{ We now have the risk of run time type errors. Let's introduce a type
for things which can go wrong. }
data Error (E X : Set) : Set where
ok : X > Error E X
error : E > Error E X
{ 2.1 Add a constructor to the following datatype for each different
kind of run time error that can happen. (Come back to this exercise
when you're writing the evaluator in 2.3.) Make these error reports
as informative as you can.
}
data EvalError : Set where
wantedANatButGotALousy : HExpIf > EvalError
wantedATwoButGotALousy : HExpIf > EvalError
 your constructors here
{ 2.2 Write a little piece of "glue code" to make it easier to manage
errors. The idea is to combine errorprone process in *sequence*, where
the second process can depend on the value produced by the first if it
succeeds. The resulting process is, of course, also errorprone, failing
as soon as either component fails.
}
_>>=_ : {E S T : Set}
> Error E S  process which tries to get an S
> (S > Error E T)  given an S, process which tries for a T
> Error E T  combined in sequence
ok s >>= s2et = s2et s
error e >>= s2et = error e
{ 2.3 Implement an evaluator for HExpIf. Be sure to add only numbers and
to branch only on Booleans. Report type mismatches as errors. You should
use _>>=_ to help with the propagation of error messages.
(2 marks)
}
natOrBust : {E : Set} > E > HValIf > Error E Nat
natOrBust e (inl b) = error e
natOrBust e (inr n) = ok n
twoOrBust : {E : Set} > E > HValIf > Error E Two
twoOrBust e (inl b) = ok b
twoOrBust e (inr n) = error e
eval : HExpIf > Error EvalError HValIf
eval (num n) = ok (inr n)
eval (boo x) = ok (inl x)
eval (d +++ e) =
(eval d >>= natOrBust (wantedANatButGotALousy d)) >>= \ dn >
(eval e >>= natOrBust (wantedANatButGotALousy e)) >>= \ en >
ok (inr (dn + en))
eval (hif e then t else f) =
(eval e >>= twoOrBust (wantedATwoButGotALousy e)) >>= \ eb >
if eb then eval t else eval f
{ Note that the type of eval is not specific about whether the value
expected is numeric or Boolean. It may help to introduce auxiliary
definitions of errorprone processes which are "ok" only for the
type that you really want.
}
{ Next up, stack machine code, and its execution. }
data HBCode : Set where
PUSHN : Nat > HBCode
PUSHB : Two > HBCode
ADD : HBCode
_SEQ_ : HBCode > HBCode > HBCode
_IFPOP_ : HBCode > HBCode > HBCode
{ The intended behaviour of (t IFPOP f) is as follows
* pop the (we hope) Boolean value from top of stack
* if it's tt, execute t, else execute f
* whichever branch is executed, it gets the popped stack to start
}
{ 2.4 Populate the type of possible execution errors and implement the
execution behaviour of HBCode, operating on a stack represented as
a list of HValIf values. (2 marks)
}
data ExecError : Set where
stackUnderflowInADD : ExecError
stackUnderflowInIFPOP : ExecError
addingATwo : HValIf > ExecError
iffingANat : HValIf > ExecError
 your constructors here
exec : HBCode > List HValIf > Error ExecError (List HValIf)
exec (PUSHN n) s = ok (inr n :> s)
exec (PUSHB b) s = ok (inl b :> s)
exec ADD (y :> x :> s)
= natOrBust (addingATwo x) x >>= \ xn >
natOrBust (addingATwo y) y >>= \ yn >
ok (inr (xn + yn) :> s)
exec ADD _ = error stackUnderflowInADD
exec (c SEQ d) s = exec c s >>= exec d
exec (t IFPOP f) [] = error stackUnderflowInIFPOP
exec (t IFPOP f) (x :> s)
= twoOrBust (iffingANat x) x >>= \ xb >
if xb then exec t s else exec f s
{ Next, we take a look at code generation and type safety. }
data HTy : Set where  we have two types in HExpIf
NUM BOOL : HTy
_=HTy=_ : HTy > HTy > Two  we can test if two types are equal
NUM =HTy= NUM = tt
NUM =HTy= BOOL = ff
BOOL =HTy= NUM = ff
BOOL =HTy= BOOL = tt
{ 2.5 Write a typesynthesizing compiler, computing both the HTy type and
the HBCode executable for a given expression. Your compiler should
give an informative error report if the expression it receives is
ill typed. Your compiler should also ensure (at least informally) that
the code produced will never trigger any execution errors.
(2 marks)
}
data CompileError : Set where
addingABool : HExpIf > CompileError
iffingANumber : HExpIf > CompileError
ifBranchesMismatchedTypes : (HExpIf /*/ HTy) > (HExpIf /*/ HTy) > CompileError
compile : HExpIf > Error CompileError (HTy /*/ HBCode)
compile (num x) = ok (NUM , PUSHN x)
compile (boo x) = ok (BOOL , PUSHB x)
compile (e1 +++ e2) = compile e1 >>= \
{ (BOOL , _) > error (addingABool e1)
; (NUM , c1) > compile e2 >>= \
{ (BOOL , _) > error (addingABool e2)
; (NUM , c2) > ok (NUM , (c1 SEQ c2) SEQ ADD)
}
}
compile (hif e then t else f) = compile e >>= \
{ (NUM , _) > error (iffingANumber e)
; (BOOL , c) > compile t >>= \
{ (tty , tc) > compile f >>= \
{ (fty , fc) >
if tty =HTy= fty then ok (tty , c SEQ (tc IFPOP fc))
else error (ifBranchesMismatchedTypes (t , tty) (f , fty))
}
}
}
{ You have a little bit more room for creative problemsolving in what's
left of the exercise. The plan is to build the type system into expressions
and code, the same way we did with plain Hutton's Razor in class.
}
{ If we *know* which HTy type we want, we can compute which Agda type we
expect our value to take. }
HVal : HTy > Set
HVal NUM = Nat
HVal BOOL = Two
{ 2.6 Finish the type of typed expressions. You should ensure that only
well HTytyped expressions can be constructed. }
data THExpIf : HTy > Set where
val : {t : HTy} > HVal t > THExpIf t
_+++_ : THExpIf NUM > THExpIf NUM > THExpIf NUM
hif_then_else_ : {t : HTy} > THExpIf BOOL > THExpIf t > THExpIf t > THExpIf t
 you fill in addition and ifthenelse
{ 2.7 Implement a typesafe evaluator. }
teval : {t : HTy} > THExpIf t > HVal t
teval (val x) = x
teval (d +++ e) = teval d + teval e
teval (hif e then t else f) = if teval e then teval t else teval f
{ 2.8 Implement a type checker. (2 marks) }
data TypeError : Set where
wanted_got_ : HTy > HExpIf > TypeError
 your constructors here
tcheck : (t : HTy) > HExpIf > Error TypeError (THExpIf t)
tcheck NUM (num x) = ok (val x)
tcheck BOOL (num x) = error (wanted BOOL got num x)
tcheck NUM (boo x) = error (wanted NUM got boo x)
tcheck BOOL (boo x) = ok (val x)
tcheck NUM (d +++ e) = tcheck NUM d >>= \ dt > tcheck NUM e >>= \ et > ok (dt +++ et)
tcheck BOOL (d +++ e) = error (wanted BOOL got (d +++ e))
tcheck t (hif e then th else el) =
tcheck BOOL e >>= \ et >
tcheck t th >>= \ tht >
tcheck t el >>= \ elt > ok (hif et then tht else elt)
{ 2.9 Adapt the technique from Hutton.agda to give a typesafe underflowfree
version of HBCode. You will need to think what is a good type to represent
the "shape" of a stack: before, we just used Nat to represent the *height* of
the stack, but now we must worry about types. See next question for a hint. }
data THBCode : List HTy > List HTy > Set where
PUSHV : {t : HTy}{s : List HTy} > HVal t > THBCode s (t :> s)
ADD : {s : List HTy} > THBCode (NUM :> NUM :> s) (NUM :> s)
_SEQ_ : {i j k : List HTy} > THBCode i j > THBCode j k > THBCode i k
_IFPOP_ : {i j : List HTy} > THBCode i j > THBCode i j > THBCode (BOOL :> i) j
{ 2.10 Implement the execution semantics for your code. You will need to think
about how to represent a stack. The Ex2Prelude.agda file contains a very
handy piece of kit for this purpose. You write the type, too. }
Stack : List HTy Set
Stack i = All HVal i
 forward composition
_followedBy_ : {A B C : Set} (f : A B) (g : B C) A C
f followedBy g = z g (f z)
tsemantics : {i j : List HTy} (c : THBCode i j) (s : Stack i) Stack j
tsemantics (PUSHV x) s = x , s
tsemantics ADD (m , n , s) = m + n , s
tsemantics (c SEQ d) s = (tsemantics c followedBy tsemantics d) s
tsemantics (t IFPOP f) (b , s) = if b then tsemantics t s else tsemantics f s
{ 2.11 Write the compiler from well typed expressions to safe code. }
tcompile : {t : HTy} > THExpIf t > {s : List HTy} > THBCode s (t :> s)
tcompile (val x) = PUSHV x
tcompile (d +++ e) = (tcompile d SEQ tcompile e) SEQ ADD
tcompile (hif e then t else f) = tcompile e SEQ (tcompile t IFPOP tcompile f)
problem file
module Ex3 where
open import Ex1Prelude
open import FuncKit
{ 3.1 Numbers in the Kit }
{ We can define the type of natural numbers using the tools
from the functor kit like this: }
kNat : Kit
kNat = kK One k+ kId
NAT : Set
NAT = Data kNat
 Define the function which sends "ordinary" numbers to
 the corresponding kitencoded numbers.
Nat2NAT : Nat > NAT
Nat2NAT n = {!!}
 Use fold to define the function which sends them back.
NAT2Nat : NAT > Nat
NAT2Nat = fold (kK One k+ kId) {!!}
 Show that you get the "round trip" property (by writing
 recursive functions that use rewrite.
Nat2NAT2Nat : NAT2Nat o Nat2NAT =^= id
Nat2NAT2Nat n = {!!}
NAT2Nat2NAT : Nat2NAT o NAT2Nat =^= id
NAT2Nat2NAT n = {!!}
{ 3.2 Lists in the Kit }
 find the code which gives you lists with a given element
 type (note that the kId constructor marks the place for
 recursive *sublists* not for list elements
kLIST : Set > Kit
kLIST A = {!!}
LIST : Set > Set
LIST A = Data (kLIST A)
 define nil and cons for your lists
nil : {A : Set} > LIST A
nil = {!!}
cons : {A : Set} > A > LIST A > LIST A
cons a as = {!!}
 use fold to define concatenation
conc : {A : Set} > LIST A > LIST A > LIST A
conc {A} xs ys = fold (kLIST A) {!!} xs
 prove the following (the yellow bits should disappear when
 you define kLIST);
 maddeningly, "rewrite" won't do it, but this piece of kit
 (which is like a manual version of rewrite) will do it
cong : {S T : Set}(f : S > T){a b : S} > a == b > f a == f b
cong f refl = refl
concNil : {A : Set}(as : LIST A) > conc as nil == as
concNil as = {!!}
concAssoc : {A : Set}(as bs cs : LIST A) >
conc (conc as bs) cs == conc as (conc bs cs)
concAssoc as bs cs = {!!}
{ 3.3 Trees in the Kit }
 give a kit code for binary trees with unlabelled leaves
 and nodes labelled with elements of NAT
kTREE : Kit
kTREE = {!!}
TREE : Set
TREE = Data kTREE
 give the constructors
leaf : TREE
leaf = {!!}
node : TREE > NAT > TREE > TREE
node l n r = {!!}
 implement flattening (slow flattening is ok) as a fold
flatten : TREE > LIST NAT
flatten = fold kTREE {!!}
{ 3.4 "rec" from "fold" }
 The recursor is a variation on the theme of fold, but you
 get a wee bit more information at each step. In particular,
 in each recursive position, you get the original substructure
 *as well as* the value that is computed from it.
rec : (k : Kit){X : Set} >
(kFun k (Data k /*/ X) > X) >
 ^^^^^^ ^
 substructure value
Data k > X
 Demonstrate that rec is no more powerful than fold by constructing
 rec from fold. The trouble is that fold throws away the original
 substructures. But you can compensate by computing something extra
 as well as the value you actually want.
rec k {X} f d = outr (fold k {{!!} /*/ X} {!!} d)
 use rec to implement "insList", being the function which inserts
 a number in a list, such that if the input list is in increasing
 order, so is the output list; you may assume that "lessEq" exists
lessEq : NAT > NAT > Two
insList : NAT > LIST NAT > LIST NAT
insList n = rec (kLIST NAT) {!!}
 justify the assumption by defining "lessEq"; do not use explicit
 recursion;
 note that the thing we build for each number is its lessorequal
 test;
 do use "rec kNat" once more to take numbers apart
lessEq x y = rec kNat {NAT > Two} {!!} x y
 implement insertion for binary search trees using "rec"
insTree : NAT > TREE > TREE
insTree n = rec kTREE {!!}
specimen solution and mark scheme
module Ex3Sol where
{ Mark Scheme
3.1 is work 3; 3.2 is worth 4; 3.3 is worth 3; 3.4 is worth 5
The total number of marks available is 15.
See below for individual mark breakdown.
}
open import Ex1Prelude
open import FuncKit
{ 3.1 Numbers in the Kit (3 marks) }
{ We can define the type of natural numbers using the tools
from the functor kit like this: }
kNat : Kit
kNat = kK One k+ kId
NAT : Set
NAT = Data kNat
 Define the function which sends "ordinary" numbers to
 the corresponding kitencoded numbers. (1 mark)
Nat2NAT : Nat > NAT
Nat2NAT zero = [ inl <> ]
Nat2NAT (suc n) = [ inr (Nat2NAT n) ]
 Use fold to define the function which sends them back. (1 mark)
NAT2Nat : NAT > Nat
NAT2Nat = fold (kK One k+ kId) (\
{ (inl <>) > zero
; (inr NAT2Nat_n) > suc NAT2Nat_n
})
 Show that you get the "round trip" property (by writing
 recursive functions that use rewrite. (1 mark)
Nat2NAT2Nat : NAT2Nat o Nat2NAT =^= id
Nat2NAT2Nat zero = refl
Nat2NAT2Nat (suc n) rewrite Nat2NAT2Nat n = refl
NAT2Nat2NAT : Nat2NAT o NAT2Nat =^= id
NAT2Nat2NAT [ inl <> ] = refl
NAT2Nat2NAT [ inr x ] rewrite NAT2Nat2NAT x = refl
{ 3.2 Lists in the Kit (4 marks) }
 find the code which gives you lists with a given element
 type (note that the kId constructor marks the place for
 recursive *sublists* not for list elements (1 mark)
kLIST : Set > Kit
kLIST A = kK One k+ (kK A k* kId)
LIST : Set > Set
LIST A = Data (kLIST A)
 define nil and cons for your lists (1 mark)
nil : {A : Set} > LIST A
nil = [ inl <> ]
cons : {A : Set} > A > LIST A > LIST A
cons a as = [ inr (a , as) ]
 use fold to define concatenation (1 mark)
conc : {A : Set} > LIST A > LIST A > LIST A
conc {A} xs ys = fold (kLIST A)
(\ { (inl <>) > ys
; (inr (a , conc_as_ys)) > cons a conc_as_ys
})
xs
 prove the following (the yellow bits should disappear when
 you define kLIST); (1 mark)
 maddeningly, "rewrite" won't do it, but this piece of kit
 (which is like a manual version of rewrite) will do it
cong : {S T : Set}(f : S > T){a b : S} > a == b > f a == f b
cong f refl = refl
concNil : {A : Set}(as : LIST A) > conc as nil == as
concNil [ inl <> ] = refl
concNil [ inr (a , as) ] = cong (cons a) (concNil as)
concAssoc : {A : Set}(as bs cs : LIST A) >
conc (conc as bs) cs == conc as (conc bs cs)
concAssoc [ inl <> ] bs cs = refl
concAssoc [ inr (a , as) ] bs cs = cong (cons a) (concAssoc as bs cs)
{ 3.3 Trees in the Kit (3 marks) }
 give a kit code for binary trees with unlabelled leaves
 and nodes labelled with elements of NAT (1 mark)
kTREE : Kit
kTREE = kK One k+ (kId k* (kK NAT k* kId))
TREE : Set
TREE = Data kTREE
 give the constructors (1 mark)
leaf : TREE
leaf = [ inl <> ]
node : TREE > NAT > TREE > TREE
node l n r = [ inr (l , n , r) ]
 implement flattening (slow flattening is ok) as a fold (1 mark)
flatten : TREE > LIST NAT
flatten = fold kTREE (\
{ (inl <>) > nil
; (inr (flatten_l , n , flatten_r)) > conc flatten_l (cons n flatten_r)
})
{ 3.4 "rec" from "fold" (5 marks) }
 The recursor is a variation on the theme of fold, but you
 get a wee bit more information at each step. In particular,
 in each recursive position, you get the original substructure
 *as well as* the value that is computed from it.
rec : (k : Kit){X : Set} >
(kFun k (Data k /*/ X) > X) >
 ^^^^^^ ^
 substructure value
Data k > X
 Demonstrate that rec is no more powerful than fold by constructing
 rec from fold. The trouble is that fold throws away the original
 substructures. But you can compensate by computing something extra
 as well as the value you actually want. (1 mark)
rec k {X} f d = outr (fold k {Data k /*/ X}
(\ kdx > [ kitMap k outl kdx ] , f kdx) d)
 use rec to implement "insList", being the function which inserts
 a number in a list, such that if the input list is in increasing
 order, so is the output list; you may assume that "lessEq" exists (1 mark)
lessEq : NAT > NAT > Two
insList : NAT > LIST NAT > LIST NAT
insList n = rec (kLIST NAT) (\
{ (inl <>) > cons n nil
; (inr (a , (as , insList_n_as))) >
if lessEq n a
then cons n (cons a as)
else cons a insList_n_as
})
 justify the assumption by defining "lessEq"; do not use explicit
 recursion; do use "rec kNat" once more to take numbers apart
 (2 marks, one for each "rec")
lessEq x y = rec kNat {NAT > Two}
(\ { (inl <>) > \ y > { lessEq zero y } tt
; (inr (x , lessEq_x)) > rec kNat (\
{ (inl <>) > { lessEq (suc x) zero } ff
; (inr (y , lessEq_[suc_x]_y)) > { lessEq (suc x) (suc y) } lessEq_x y
})
})
x y
 implement insertion for binary search trees using "rec" (1 mark)
insTree : NAT > TREE > TREE
insTree n = rec kTREE (\
{ (inl <>) > node leaf n leaf
; (inr ((l , insTree_n_l) , y , (r , insTree_n_r))) >
if lessEq n y then node insTree_n_l y r else node l y insTree_n_r
})
problem file
module Ex4 where
{ I'm sorry I haven't quite finished setting this exercise yet, but by
the joy of version control, the rest of it can be merged in later
(quite soon). At least you can get cracking: I promise not to break
anything, just to add a bit more on the end.
The deadline for this is midnight on the Monday of Week 12 (15 Dec).
It'd be good to get the marks in before Christmas, but if the end of
term is looking deadlinetastic, please open negotiations.
}
open import Ex1Prelude
open import IxCon
{# BUILTIN BOOL Two #}
{# BUILTIN TRUE tt #}
{# BUILTIN FALSE ff #}
{# BUILTIN LIST List #}
{# BUILTIN NIL [] #}
{# BUILTIN CONS _:>_ #}
postulate  this means that we just suppose the following things exist...
Char : Set
String : Set
{# BUILTIN CHAR Char #}
{# BUILTIN STRING String #}
primitive  these are baked in; they even work!
primCharEquality : Char > Char > Two
primStringAppend : String > String > String
primStringToList : String > List Char
primStringFromList : List Char > String

 WRITING FILES, AN INTERFACE

{ If you possess the ability to open a file for writing, you might
have the following interface. }
 States
data WriteState : Set where
opened closed : WriteState  do you currently have a file open or not?
 Commands
data WriteC : WriteState > Set where
openWrite : (fileName : String) > WriteC closed
writeChar : Char > WriteC opened
closeWrite : WriteC opened
 Responses
WriteR : (j : WriteState)(c : WriteC j) > Set
WriteR .closed (openWrite fileName) = WriteState  we get told whether it worked
WriteR .opened (writeChar x) = One  always works
WriteR .opened closeWrite = One  always works
{ 4.1 Implement the following operation which determines the next
state. You should ensure that you can write characters only to
a successfully opened file, and that you can write as many as
you want. It should also be possible to insist that a process
closes its file. }
writeNext : (j : WriteState)(c : WriteC j) > WriteR j c > WriteState
writeNext j c r = {!!}
 the file writing interface, assembled as an indexed container
WRITE : WriteState => WriteState
WRITE = WriteC <! WriteR / writeNext

 READING FILES, AN INTERFACE

{ To read from a file, it should be open, and you shouldn't be at the
end of it. }
 States
data ReadState : Set where
opened : (eof : Two) > ReadState  eof is tt if we're at end of file
closed : ReadState
{ 4.2 Finish the READ implementation, in accordance with the description. }
 Commands
data ReadC : ReadState > Set where
openRead : { your stuff } ReadC {!!}  needs a filename; might not open successfully;
 might open an empty file
readChar : { your stuff } ReadC {!!}  makes sense only if we're not at end of file
 and might take us to end of file
closeRead : { your stuff } ReadC {!!}  makes sense only if the file is open
 Responses
ReadR : (j : ReadState)(c : ReadC j) > Set
ReadR j c = {!!}
 next State; you need to make sure the response gives enough info
readNext : (j : ReadState)(c : ReadC j) > ReadR j c > ReadState
readNext j c r = {!!}
READ : ReadState => ReadState
READ = ReadC <! ReadR / readNext

 COMBINING TWO INTERFACES WITH SHARED STATE

{ 4.3 Let's suppose we have two commandresponse interfaces which offer
different functionality for the same system. Correspondingly, we'll
have two indexed containers for the same index set. Show that you
can combine them into one indexed container which lets you choose a
command from either menu and evolves the state as specified by
whichever interface offered the chosen command.
}
_=+=_ : {I : Set} > I => I > I => I > I => I
CRn0 =+= CRn1 = {!!}

 WHEN IGNORANCE IS BLISS, BIS

{ 4.4 If we have a commandresponse interface with index I representing
states of the system, show that we can index basically the same
commands and responses over a state, I /*/ J, where the J is just
useless information which never changes. (This operation isn't
superuseful on its own, but it's handy in combination with other
things. }
GrowR : {I J : Set} > I => I > (I /*/ J) => (I /*/ J)
GrowR CRn = {!!}
 do the same for "growing the index on the left"
GrowL : {I J : Set} > I => I > (J /*/ I) => (J /*/ I)
GrowL CRn = {!!}

 COMBINING TWO INTERFACES WITH SEPARATE STATE

{ 4.5 Making use of 4.4 and 4.5, show how to combine two interfaces which
operate independently on separate state: commands from one should
not affect the state of the other.
}
_<+>_ : {I0 I1 : Set} > I0 => I0 > I1 => I1 > (I0 /*/ I1) => (I0 /*/ I1)
CRn0 <+> CRn1 = {!!}

 ERROR REPORTING, AN INTERFACE

{ I'm building the next bit for you.
When things go wrong, we need to trigger an error condition and abort
mission. However, if we have other stuff going on (open files, etc),
it may not always be ok to drop everything and run away. There will
be some states in which it is safe to escape (and deliver a suitable
error message, perhaps) and other states in which escape should be
impossible.
If it is safe to issue an error message, we should be able to do so
without fear of any response from the environment that would oblige
us to carry on.
}
data ErrorC {I : Set}(SafeMessage : I > Set)(i : I) : Set where
error : SafeMessage i > ErrorC SafeMessage i
 the SafeMessage parameter tells us what is an acceptable
 error message in any given state; in states where this gives
 Zero, it will be impossible to trigger an error!
ErrorR : {I : Set}{SafeMessage : I > Set}(i : I)(c : ErrorC SafeMessage i) > Set
ErrorR _ _ = Zero  there's no comeback
errorNext : {I : Set}{SafeMessage : I > Set}
(i : I)(c : ErrorC SafeMessage i) > ErrorR i c > I
errorNext i c ()  so we don't have to say how the state will evolve
ERROR : {I : Set}(SafeMessage : I > Set) > I => I
ERROR SafeMessage = ErrorC SafeMessage <! ErrorR / errorNext

 COPY A FILE

{ 4.6 Implement a process which, given access to suitable interfaces, will
give the process for copying a named source file to a named target
file. This goes in two phases.
}
{ 4.6.1 Firstly, you should identify the commandreponse interface within
which you need to work. You will need to be able to read and write files,
but also to signal errors (in case a file fails to open for some reason).
You must ensure that it is impossible for any process using your interface
to escape with an error leaving a file open. You must also make it
possible to guarantee that your copying process will, error or not, leave
all files closed.
}
CPState : Set
CPState = {!!}
CPInterface : CPState => CPState
CPInterface = {!!}
{ 4.6.2 Secondly, you should implement your copying process, working to your
interface. I will let you switch off the termination checker: you cannot
predict in advance how long the copying process will go on, as you have
not seen the source file yet. (Later, we'll learn how to be honest about
things which might go on for ever, but for now, let's cheat.)
}
{# NO_TERMINATION_CHECK #}
cp : (sourceFile targetFile : String) > Game CPInterface {!!} {!!}
cp sourceFile targetFile = {!!}
{ HINTS
You will certainly need to build some extra bits and pieces.
You have the components for reading, writing and error handling, and
suitable kit with which to combine them. Reading and writing don't
interfere with each other, but it's important to make sure that you
can't bomb out with an error, so some shared state seems important.
There are really two phases to the process:
(1) getting the files open  this may go wrong
(2) copying from one to the other  this will work if we reach it
You might want to split these phases apart.
}

 SCRIPTING INTERACTION

{ 4.7.1 Show how to take a commandresponse interface and deliver its
"scripted" version, where a script command consists of any permitted
(possibly empty) sequence of the given commands. }
SCRIPT : {I : Set} > I => I > I => I
SCRIPT {I} CRn = Game CRn (\ I > One) <! Rs / ns where
Rs : (i : I) > Game CRn (\ I > One) i > Set
Rs i cs = {!!}
ns : (i : I)(cs : Game CRn (\ I > One) i) > Rs i cs > I
ns i cs rs = {!!}
{ 4.7.2 Show how to take a strategy for scripted interaction and turn
it into a strategey for unscripted interaction, by running the scripts
one command at a time. You may find it useful to build a helper function
to process one script. }
unScript : {I : Set}(CRn : I => I){X : I > Set}{i : I} >
Game (SCRIPT CRn) X i > Game CRn X i
unScript CRn g = {!!}
 HINT doing recursion in the "fold" pattern may help

 INDEXED CONTAINER DRIVERS(*)
 (*) The researchers who invented this stuff are fans of The Fall
 (by which I mean the group led my Mark E Smith who wrote the song
 The Container Drivers, not some johnnycomelately Northern Irish
 serial killer drama).

record Driver {I J : Set}(Sync : I > J > Set)
(Hi : I => I)(Lo : J => J) : Set where
 Hi is a highlevel commandresponse interface
 Lo is a lowlevel commandresponse interface
 Sync specifies which high and low level states are compatible
 and what you expect to know at the time
field
 assuming states are in sync; it should be possible to map
 highlevel commands to lowlevel commands...
hiClo : (i : I)(j : J) > Sync i j >
Command Hi i > Command Lo j
 ...and afterwards to translate the lowlevel response to that
 command back up to the highlevel
loRhi : (i : I)(j : J)(s : Sync i j)(c : Command Hi i) >
Response Lo j (hiClo i j s c) > Response Hi i c
 moreover, the resulting states should be in sync
nSync : (i : I)(j : J)(s : Sync i j)(c : Command Hi i)
(r : Response Lo j (hiClo i j s c)) >
Sync (next Hi i c (loRhi i j s c r)) (next Lo j (hiClo i j s c) r)
open Driver public

 A DANGEROUS HASKELL IO COMMANDRESPONSE SYSTEM

data Maybe (X : Set) : Set where
yes : X > Maybe X
no : Maybe X
data IOMode : Set where
readMode writeMode appendMode readWriteMode : IOMode
postulate Handle : Set
data HaskellIOCommand (_ : One) : Set where
hOpen : String > IOMode > HaskellIOCommand <>
hClose hIsEOF hGetChar : Handle > HaskellIOCommand <>
hPutChar : Handle > Char > HaskellIOCommand <>
hError : String > HaskellIOCommand <>
HaskellIOResponse : (i : One) > HaskellIOCommand i > Set
HaskellIOResponse i (hOpen f m) = Maybe Handle
HaskellIOResponse i (hClose h) = One
HaskellIOResponse i (hIsEOF h) = Two
HaskellIOResponse i (hGetChar h) = Char
HaskellIOResponse i (hPutChar h c) = One
HaskellIOResponse i (hError e) = Zero
HASKELLIO : One => One
HASKELLIO = HaskellIOCommand <! HaskellIOResponse / _

 SCRIPTING INTERACTION

{ 4.8 Your mission is to translate your lovely, safe characterisation
of reading and writing into its dodgy Haskell counterpart. Of course,
your code shouldn't do anything dodgy. You will need to think what
information must be available when you are in each state.
}
safe2unsafe : Driver (\ i j > {!!}) CPInterface (SCRIPT HASKELLIO)
safe2unsafe = {!!}

 TO BE CONTINUED... BUT NOT WITH ANY MORE CODING OBLIGATIONS

specimen solution and mark scheme
module Ex4Sol where
{ Mark Scheme
as indicated, below, totalling 15
}
open import Ex1Prelude
open import IxCon
{# BUILTIN BOOL Two #}
{# BUILTIN TRUE tt #}
{# BUILTIN FALSE ff #}
{# BUILTIN LIST List #}
{# BUILTIN NIL [] #}
{# BUILTIN CONS _:>_ #}
postulate  this means that we just suppose the following things exist...
Char : Set
String : Set
{# BUILTIN CHAR Char #}
{# BUILTIN STRING String #}
primitive  these are baked in; they even work!
primCharEquality : Char > Char > Two
primStringAppend : String > String > String
primStringToList : String > List Char
primStringFromList : List Char > String

 WRITING FILES, AN INTERFACE

{ If you possess the ability to open a file for writing, you might
have the following interface. }
 States
data WriteState : Set where
opened closed : WriteState  do you currently have a file open or not?
 Commands
data WriteC : WriteState > Set where
openWrite : (fileName : String) > WriteC closed
writeChar : Char > WriteC opened
closeWrite : WriteC opened
 Responses
WriteR : (j : WriteState)(c : WriteC j) > Set
WriteR .closed (openWrite fileName) = WriteState
WriteR .opened (writeChar x) = One
WriteR .opened closeWrite = One
{ 4.1 Implement the following operation which determines the next
state. You should ensure that you can write characters only to
a successfully opened file, and that you can write as many as
you want. It should also be possible to insist that a process
closes its file. (1 mark) }
{
writeNext : (j : WriteState)(c : WriteC j) > WriteR j c > WriteState
writeNext j c r = {!!}
}
writeNext : (j : WriteState)(c : WriteC j) > WriteR j c > WriteState
writeNext ._ (openWrite fileName) j = j
writeNext .opened (writeChar x) r = opened
writeNext .opened closeWrite r = closed
 the file writing interface, assembled as an indexed container
WRITE : WriteState => WriteState
WRITE = WriteC <! WriteR / writeNext

 READING FILES, AN INTERFACE

{ To read from a file, it should be open, and you shouldn't be at the
end of it. }
 States
data ReadState : Set where
opened : (eof : Two) > ReadState  eof is tt if we're at end of file
closed : ReadState
{ 4.2 Finish the READ implementation, in accordance with the description.
(3 marks, for commands, responses and next) }
{
 Commands
data ReadC : ReadState > Set where
openRead : { your stuff } ReadC {!!}  needs a filename; might not open successfully;
 might open an empty file
readChar : { your stuff } ReadC {!!}  makes sense only if we're not at end of file
 and might take us to end of file
closeRead : { your stuff } ReadC {!!}  makes sense only if the file is open
 but you should not be forced to read the whole file
 Responses
ReadR : (j : ReadState)(c : ReadC j) > Set
ReadR j c = {!!}
 next State; you need to make sure the response gives enough info
readNext : (j : ReadState)(c : ReadC j) > ReadR j c > ReadState
readNext j c r = {!!}
}
 Commands
data ReadC : ReadState > Set where
openRead : String > ReadC closed  needs a filename; might not open successfully;
 might open an empty file
readChar : ReadC (opened ff)  makes sense only if we're not at end of file
 and might take us to end of file
closeRead : {b : Two} > ReadC (opened b)  makes sense only if the file is open
 Responses
ReadR : (j : ReadState)(c : ReadC j) > Set
ReadR .closed (openRead x) = ReadState
ReadR .(opened ff) readChar = Char /*/ Two
ReadR ._ closeRead = One
 next State; you need to make sure the resonse gives enough info
readNext : (j : ReadState)(c : ReadC j) > ReadR j c > ReadState
readNext .closed (openRead x) s = s
readNext .(opened ff) readChar (c , b) = opened b
readNext ._ closeRead r = closed
 the file reading interface, assembled as an indexed container
READ : ReadState => ReadState
READ = ReadC <! ReadR / readNext

 COMBINING TWO INTERFACES WITH SHARED STATE

{ 4.3 Let's suppose we have two commandresponse interfaces which offer
different functionality for the same system. Correspondingly, we'll
have two indexed containers for the same index set. Show that you
can combine them into one indexed container which lets you choose a
command from either menu and evolves the state as specified by
whichever interface offered the chosen command.
(2 marks, one for commands, one for the rest)
}
_=+=_ : {I : Set} > I => I > I => I > I => I
(C0 <! R0 / n0) =+= (C1 <! R1 / n1)
= (\ i > C0 i /+/ C1 i)
<! (\ { i (inl c0) > R0 i c0 ; i (inr c1) > R1 i c1 })
/ (\ { i (inl c0) r0 > n0 i c0 r0 ; i (inr c1) r1 > n1 i c1 r1 })

 WHEN IGNORANCE IS BLISS, BIS

{ 4.4 If we have a commandres