* Thorsten Altenkirch [2005-01-25 17:16]:
> I don't get this. Which case analysis do you have to do but you don't
> want to do?
I was argueing whether i didn't get 'enough' case analyis since the case
analysis i get for l is the same as if i had declared l:List X .
> > --------------------------------------------------------------------
> > ( l : List Nat !
> > let !--------------!
> > ! p l : * )
> >
> > p l <= case l
> > { p nil []
> > p (cons x l) []
> > }
> > --------------------------------------------------------------------
> >
> > Why do i have to do one more case analysis eventually? If i had
> > wanted to write some generic code for lists i would not have
> > instantiated its signature. Why is my explanation not effective
> > enough to decompose my programs input in one go?
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.
> > I'm aware that what i ask for doesn't generalize nicely, since i
> > don't want to be forced to invent n answers for a single case on
> > some i:Fin n whose n has been is fixed.
> > But for polymorphic types (Fin drops out, it's 'polyvalent'), do i
> > always have to start off with some code that's more generic than its
> > signature possibly says?
Sebastian
