I don't get this. Which case analysis do you have to do but you don't want to do?
T.
Sebastian Hanowski wrote:
Hi
Epigram doesn't write the programs for me that i want it to.
Equipped with some declarations...
------------------------------------------------------------------------ ( n : Nat ! data (---------! where (------------! ; !-------------! ! Nat : * ) ! zero : Nat ) ! suc n : Nat ) ------------------------------------------------------------------------ ( X : * ! ( x : X ; l : List X ! data !------------! where (--------------! ; !---------------------! ! List X : * ) ! nil : List X ) ! cons x l : List X ) ------------------------------------------------------------------------
... type inference takes the type of arguments to constructor functions into account as usual:
------------------------------------------------------------------------ inspect cons zero nil => cons zero nil : List Nat ------------------------------------------------------------------------
But program inference doesn't seem to take the arguments to type constructors too serious:
------------------------------------------------------------------------
( 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?
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?
Best regards, Sebastian
-- 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.
