Hi Jan, Jesper, and Dominique,
Unfortunately, the termination checker and 'with' do not harmonize. The
problem, as already been outlined by Dominique, is that the termination
checker works on the desugared code, where 'with' has been replaced by
an auxiliary function. So, even if in the source code the recursive
call arguments are looking smaller, the termination checker might not
see it due to the generated auxiliary function.
On 30.10.2013 15:04, Dominique Devriese wrote:
> I believe that a with-pattern-match is internally translated to a call
> of a local helper function with the scrutinee as an extra argument and
> an appropriate type to use the information learned from the pattern
> match. Strangely, if I perform this translation manually here:
> merge′ : List Nat → List Nat → List Nat
> merge′ nil ys = ys
> merge′ xs nil = xs
> merge′ (x :: xs) (y :: ys) = go x xs y ys (order x y)
> where go : Nat → List Nat → Nat → List Nat → Order → List Nat
> go x xs y ys le = x :: merge xs (y :: ys)
> go x xs y ys gt = y :: merge (x :: xs) ys
>
> Then the termination checker does succeed. It seems weird (at least
> to me) that it doesn't work on the same code without the
> with-desugaring.
Yes that is weird. It does not succeed when I try your code. Note that
the apparent success might be to the fact that you actually have no
recursive calls, since your function merge' only calls merge (which is,
to your bad luck, in scope here).
So, let me emphasize that the termination checker refutes this call pattern.
merge (x :: xs) (y :: ys)
--> go x xs y ys ...
--> merge xs (y :: ys)
The termination checker sees that in merge-->go, the arguments all
become smaller, but in go--->merge, one argument becomes bigger. Since
it has simplistic, it cannot remember where y and ys came from and that
taken together, they are actually the same as we started out. Thus, it
fails to see that, in the composed call
merge (x :: xs) (y :: ys) -->---> merge xs (y :: ys),
one argument actually got smaller where the other did not become bigger.
If it did not fail to see this, it would accept merge.
There are several ways out of this dilemma:
1. (preferred) Avoid 'with' when possible. In your case, there is no
dependency in the types on (order x y), thus, use an if-then-else-like
function instead.
2. Use the trick to put the recursive calls into the 'with' as well.
merge (x :: xs) (y :: ys) with order x y | merge xs (y :: ys) | merge
(x :: xs) ys
... | le | call1 | call2 = call1
... | ge | call1 | call2 = call2
This basically corresponds to the use of an if-like function, only
that it is "defined on the fly" here.
3. Define your auxiliary function yourself and in a way that lets the
termination checker see that your call patterns are ok.
4. Use sized types (experimental) and --termination-depth=2. This is
maybe not ripe for production-use.
http://gc.codehum.com/p/agda/issues/detail?can=2&q=709
>>> >>The problem with the definition of merge is that the termination checker
>>> >>looks for one argument to the function that becomes structurally smaller in
>>> >>all recursive calls.
This is not correct. Lexicographic orders are also accepted, for instance.
Cheers,
Andreas