Edwin Brady wrote:
On Tue, Jan 25, 2005 at 05:49:10PM +0100, Sebastian Hanowski wrote:
Why can't Epigram give me something like this for a case on l
(manipulated):
------------------------------------------------------------------------
( l : List Nat !
let !--------------!
! p l : * )
p l <= case l
{ p nil []
p (cons zero l) []
p (cons (suc n) l) []
}
------------------------------------------------------------------------
To me it's obvious that if i'll specify which things i expect in a data
structure, i intend to compute with them hence will inspect them. But
the signature doesn't suffice to communicate this to the elaborator.
It is perhaps obvious that you intend to compute with them, but it isn't so
obvious how. Case analysis is just one thing you might want to do - you may
also for example want to call a helper function, or use a view.
Quite so. If I want to add a list of numbers, I probably don't want to do
case on the numbers in the list: the implementation of plus does that.
Moreover, just doing case on the first element of the list isn't the only
'obvious' case analysis one might wish for: what about the tail of the
list in the cons case? what about the predecessor in the suc case? We really
could do quite a lot of obvious case analysis automatically, couldn't we?
That aside, the existing syntax is too noisy. Generally speaking, a nonempty
case analysis betrays its presence without the need for syntax. The
spontaneous appearance of constructor symbols where there ought to be
pattern variables is a bit of a giveaway. You don't get to infer when to do
case analysis given a programming problem, but you can infer (up to
irrelevant permutations) which case analysis delivered a particular
nonempty program you happen to be reloading, so you just click to split when
you're programming and don't put case in the text. Exercise: why must the
program be nonempty?
Cheers
Conor
--
http://www.cs.nott.ac.uk/~ctm
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.
