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
