Sebastian Hanowski wrote:
* Conor McBride [2005-01-25 18:50]:
I was just having the impression that in casing over some l:List Nat the
type constructor List has I already 'contributed' to the patterns
nil
(cons x l)
but Nat has not.
This is true, but the contribution the types make isn't whether or not to do
case analysis---for inductive datatypes, that's a decision best left to a
human being. The type determines how to do an atomic step of case analysis on
request. It can't be the machine's business to guess where to do case next
after an atomic step, for the same reason that the machine shouldn't be
guessing the step in the first place.
Now, if you have a particular combination of steps which you use frequently,
eg, the analysis of List Nat into
nil
(cons zero l)
(cons (suc n) l)
then there's nothing to prevent you defining your own elimination operator
which expresses that, reducing two atomic steps to one defined step.
And the other way round, these patterns wouldn't
suffice to infer List Nat.
Type inference is a non starter, but given these patterns and the type, it's
possible to infer a tree of case analyses which yields them (Augustsson '85).
That way, although you get to generate case trees one node at a time, you
only need to store the list of leaves.
Cheers
Conor
--
http://www.cs.nott.ac.uk/~ctm
