Hi Everyone,
More noise for this list!
I used Epigram in teaching this year, and, since summer is nearly
here I thought I'd give some feedback on my experiences. All of this
is very unscientific and subjective, so take with a pinch of salt.
The class was a final year BSc Hons class (Snr Hons in Scottish
terms) in functional programming. Most NZ students leave at the end
of 3rd year, and usually only strong students stay on for 4th year.
The class also had some students who were taking taught Master's
degrees. These students have a wider range of abilities. Before we
started on Epigram we covered (relatively) practical Haskell
programming, and some lambda calculus. Some of the students had taken
a paper on computational logic, which focusses on theorem proving and
logic programming, but also covers Gentzen systems.
With epigram I was aiming for several related goals:
1) introduce the Curry-Howard/Propositions as types/proofs as
programs idea, and give the flavour of programming in constructive logic
2) let students experience epigram's interactive programming environment
3) let students see dependent types doing something useful (or at
least something neat)
We did various things:
a) We gave the usual logical types, and Nats, lists, equality...
b) to get a flavour of the extra power of the type system we started
with lists and append in Haskell, and moved to defining lists and
append in type theory. Then we moved on to defining vectors and
exploring how we could use the type to express a full specification
for append.
c) to get a bit more of the flavour of programming constructively we
proved that very Nat is either even or odd. This is similar to, and
much simpler than, "either this string parses or it doesn't".
I gave the students an assignment which involved proving some
`logical' stuff and defining and proving that addition is commutative.
The logic went from showing |- A & B -> B & A, up to showing that A
v -A |- --A -> A, and showing --A -> A |- A v -A does not hold, and
showing A v -A |- ((A -> B) -> A) -> A.
I gave them two definition for addition:
plus 0 m = m
plus n' m = (plus n m)'
and
add 0 0 = 0
add 0 n' = n'
add n' 0 = n'
add n' m' = (add n m)''
To permit the latter definition I gave them an elimination rule (and
consequently a new refinement operator). Proving that add is
commutative is a lot easier than proving that plus is.
The reaction of the students to epigram was, predictably, mixed. I
had feared that they would complain about the UI (none were very
experienced emacs users, for example) but none of them raised this as
an issue. Curiously, one of them expressed a dislike for the style of
incremental program development with rapid feedback! The very best
students got a lot out of working with epigram. Some of the middle
students found the harder assignment questions beyond them, but some
of the middle students really got the idea of proofs as programs. At
least one of the weaker students just didn't understand what was
going on.
I intend to use epigram again next year. Two obvious things which I
could improve are:
i) fewer logical examples, and more programming examples;
ii) more motivating examples of quite basic uses for dependent types;
Anyhow, I hope that this is useful to someone, and I'm happy to
discuss further with anyone interested. I guess that eventually there
is a paper on teaching programming in constructive type theory
constructively in this somewhere.
Cheers,
Neil
School of Mathematics, Statistics and Computer Science &
Centre for Logic, Language and Computation
Victoria University
P. O. Box 600
Wellington Tel +64 4 463 6732
New Zealand mailto:[EMAIL PROTECTED]
The information in this e-mail message is confidential and may also
be privileged. If you are not the intended recipient, please notify
the sender immediately and destroy any copies of this e-mail.
