Hi Neil,
good to see that you are trying out Epigram.
I'm think of using epigram to teach some dependently typed programming
to my 4th year functional programming student next year, so I'm having
fun writing and trying to understand little programs just now.
Indeed, I am using Epigram in a 2nd/3rd year course here, see
http://www.cs.nott.ac.uk/~txa/g5bcfr/
and I still hope that I find the time to write some lecture notes.
In the meantime, I find that Conor's tutorial is a valuable resource,
it is available from the Epigram homepage http://www.e-pig.org/:
http://www.e-pig.org/downloads/epigram-notes.pdf
I am not sure whether I understand your questions properly, but here
are some comments...
There is no need to define "fibber" because structural recursion is
built-in into Epigram, actually the elaborator translates structural
recursion into uses of standard elimination constants. That is you can
just write
-----------------------------------------------------------
( n : Nat !
let !-------------!
! fib n : Nat )
fib n <= rec n
{ fib n <= case n
{ fib zero => zero
fib (suc n) <= case n
{ fib (suc zero) => one
fib (suc (suc n)) => add (fib n) (fib (suc n))
}
}
}
-----------------------------------------------------------
and let Epigram do all the fibbing...
But to address your program:
( n : Nat !
let !-------------!
! fib n : Nat )
fib n <= case (fibber n (pair (succ zero) zero))
{ fib n => a
}
I am not sure why Epigram actually allows you to do this, it should be
an error. Case is a program refinement tactic, not a program language
construct and it only works well for variables, not for expressions
(like "fibber ..."). What you want to use here is called the "with"
rule, which is not yet implemented - see "The view from the left"
http://www.e-pig.org/downloads/view.pdf
There are a number of work-arounds (e.g. define projections or use an
auxilliary function)... But at least in the fib case it turns out not
to be necessary.
Cheers,
Thorsten
--
Dr. Thorsten Altenkirch phone : (+44) (0)115 84 66516
Lecturer http://www.cs.nott.ac.uk/~txa/
School of Computer Science & IT University of Nottingham
This message has been checked for viruses but the contents of an attachment
may still contain software viruses, which could damage your computer system:
you are advised to perform your own checks. Email communications with the
University of Nottingham may be monitored as permitted by UK legislation.
