> > > > >>>f :: m:Nat -> n:Nat -> T m n -> T m n > >>>f 2 n t = t > >>>f 7 9 c4 = c5 > >>>f 7 9 c5 = c4 > >>> > >>> > >>> > >>> > >>Because, as a decision procedure for covering will tell you, that is not > >>a function. > >> > >> > >> > > > >Do you mean this is not a total function? I think it is. > > > > > > Maybe it is, in which case I'm sorry I'm too stupid. I don't see what it > does with the c6 and c7 constructors.
Yes, it is total. What we need is to give an algorithm to check this. I remember Nicolas Oury gave a talk about this. He said the case c6 and c7 could be automatically eliminated. But the process looks rather complicate. If you have carefully designed the > type so that these constructors can never be used for closed terms, > perhaps you could explain your design to me, so that I will believe you > have written a function. There may be another function with that type, > but so what? Why is /this/ a function? What's the evidence? Let's be clear that we don't distinguish functions and programs from programming point of view. Why do we need every program to be fully defined if we can check inhabitation? > > If you actively want to express a total function, then make that > totality clear. It is not clear to case-splitting, but may be clear to a powerful algorithm. After all, it doesn't need to be clear. If you had chosen a slightly different return type, eg > Divides m 14, your heuristic might not be clever enough to spot that the > type is inhabited, but you might still want to write a function. This is another kind of question. I treat pattern matching as addtional power to define function. If my algorithm is powerful enough to decide inhabitation of ..m.14.., then you are not allowed to use pattern matching, you must use other means such as eliminators. > > I don't know why you advocate partial definitions and all this machinery > to guess inhabitants of types if you want to write total functions. > Well, I only want to demonstrate that pattern matching and case-splitting are different. And the totality checking can be very complicate in some cases. That is why I developed the idea of partiality. Yong
