[Agda] primitive recursion over the natural numbers

[Conor McBride]

Hi Ed

On 9 Aug 2008, at 06:13, Ed Morehouse wrote:

> I'm quite new to agda, so please forgive me if I'm overlooking the  
> obvious.

Nope, you're looking at the highly non-obvious. Interesting
stuff.

[..]

>   recNat : (A : Nat -> Set) -> A zero -> ((i : Nat) -> A i -> A  
> (suc i)) -> (n : Nat) -> A n

[..]

> Then I tried it out on a vector ( ([0] , _:::_) are my vector  
> (nil , cons) ).

Let's just write down the types of those constructors:

   [0]   : {X : Set} -> Vec X zero
   _:::_ : {X : Set}{n : Nat} -> X -> Vec X n -> Vec X (suc n)

> This worked as I expected:
>
>   recNat (Vec Nat) [0] (\ n v -> (n ::: v)) 5

Filling in the blanks, that's

   \ n v -> _:::_ {Nat}{n} n v

> But the eta equivalent:

Oh no it isn't! Not when you can see the hidden
parts. Your instincts about eta-contraction get
thrown when you can't see the whole of the term
where the argument must not occur free.

>   recNat (Vec Nat) [0] _:::_ 5

What's happening here is that Agda is trying to
solve for the hidden arguments in the scope
where _:::_ is used. Whether or not that's a
good choice, it's certainly the obvious choice
(and "obvious" is usually a virtue with choices).

Let me see if I can write down the problem, binding
variables with ? if we are to solve them, and with \
if they are abstract. Scope runs downward, and I'll
insert constraints where they're scoped. (Remark:
what follows is an educated guess, but I've had an
unusually helpful education in this respect...)

We start like this:

   ? X : Set
   ? n : Nat
   [ X -> Vec X n -> Vec X (suc n)    -- from _:::_ {X}{n}
   = (i : Nat) -> Vec Nat i -> Vec Nat (suc i)   -- wanted
   ]

To unify function types, unify the domains, then the
ranges for an arbitrary domain value. That gives

   ? X : Set
   ? n : Nat
   [ Nat = X ]
   \ i : Nat
   [ Vec Nat i = Vec Nat n ]
   [ Vec Nat (suc i) = Vec Nat (suc n) ]

Solving for X is no problem, for Nat is globally scoped.
Instantiating and simplifying, we have the problem

   ? n : Nat
   \ i : Nat
   [ n = i ]

That is, choose a number that's equal to all other
numbers. Not gonna happen.

> yields the error:
>
>   The metavariable _839 cannot depend on i
>   because it does not depend on any variables
>   when checking that the expression _:::_ has type
>   (i : Nat) -> Vec Nat i -> Vec Nat (suc i)

I'm hoping this message makes more sense, given this
constraint solving narrative.

> I don't understand why there should be a difference.

The difference is that the hidden arguments are
scoped more generously in

   \ n v -> _:::_ {?}{?} n v

than in

   _:::_ {?}{?}

which raises the question of whether it would be kind
(or just bizarre) to perform "eta-expansion" when
deploying partially applied functions with hidden
arguments. This would maximize the context in which
the arguments are scoped --- in case the term we
really want is not, once elaborated, an eta-expansion.

Of course, you have to have some means of deciding
how much eta expansion to do, especially if you have
incomplete type information. How to typecheck when
even the types have holes is not always obvious: the
whole thing can deadlock if you rely on the presence
of type information to tell you whether or not to do
something clever.

> Next I noticed that when the result type does not depend on Nat,  
> that is, when A is a constant function, agda seems to be able to  
> reliably infer the first argument of recNat.  For example, this  
> worked fine ( ([] , _::_) are my list (nil , cons) ):
>
>   recNat _ [] _::_ 5
>
> (even the issue above doesn't come up).  How can I check (prove or  
> disprove) that agda can always infer the first argument in this case?

The reason that thing works is subtle but predictable.
The structure of recursors (recursors, mind!) is good
at delivering the kinds of problems which have
solutions in this setting. Let's look inside, checking

   ? T : Set
   ? A : Nat -> Set
   ? X Y : Set
   [ recNat {A} ([] {X}) (_::_ {Y}) 5 : T ]

We get T = A 5, soon enough. The business happens with
the methods. For these, we get

   [ A 0 = List X ]

and

   [ Y = Nat ]
   \ i : Nat
   [ List Y = A i ]
   [ List Y = A (suc i) ]

ok, filling in Y = Nat, we now have, amongst others

   ? A : Nat -> Set
   ...
   \ i : Nat
   [ List Nat = A i ]

for which

   A = \ i -> List Nat

presents itself as a most general solution, even up to
the highly intensional definitional equality. With that
in place, the rest is easy.

So it's because recursors (on simple datatypes, I might
add), have recursive arguments whose types (the "inductive
hpotheses") are *arbitrary* instances (ie abstracted over
distinct, locally quantified variables) of the motive
parameter (the thing like A here), that you get good
behaviour for non-dependent recursions. That favourable
combination of circumstances gives you

   A <linear vars> = <constant>

and hence

   A = \ <linear vars> -> <constant>

What luck!

Note that the method return types are too specific to
allow this:

   A (suc i) = List Nat

doesn't help at all. It's the recursive arguments that
do the work here. But with more involved inductive
families of types, there's no reason why the arbitrary
recursive argument should have an arbitrary index.

   (n : Nat)(t : Term (suc n)) -> A (suc n) t -> A n (lam t)

will never tell you A (but you might get lucky elsewhere).

>   recNatConst : {A : Set} -> A -> (Nat -> A -> A) -> Nat -> A
>   recNatConst = recNat (constType _)
>
> which I suppose should be equivalent to non-dependent primitive  
> recursion over the naturals.
>
> I realize that, in general, the first argument to recNat is not  
> inferable, but I wonder if when A is--i'm not really sure about  
> terminology here--maybe, an inductive family, then the first  
> argument could be inferable.  Concretely, I'm asking is there a  
> function:
>
>
>   recNatInd : {A : ???} -> A zero -> ((i : Nat) -> A i -> A (suc  
> i) ) -> (n : Nat) -> A n
>
> such that
>
>   recNatInd [0] (\ n v -> (n ::: v)) 5
>
> normalizes to a value?

Well, it has to typecheck first, and with the dependent
motive A, the constraint system is rather subtle... See
if you can figure out why

   recNat _ [0] (\ n v -> _:::_ {Nat}{n} n v) 5

actually does typecheck! But, more generally, there's
an understandable conflict between figuring out A and
figuring out the length index of _:::_ which only has
a solution for pretty subtle reasons.

Meanwhile, you may be pleased to note that

downFrom : (n : Nat) -> Vec Nat n
downFrom = recNat _ [0] (\ n v -> n ::: v)

typechecks. Can you see why it's easier to infer the
motive for an arbitrary recNat than for recNat ... 5 ?

Anyhow, once again we have fun and games with implicit
syntax and mixed-prefix unification. As other threads
have indicated, it's far from "well understood" let
alone "widely understood". I hope I've exposed enough
of the rationale behind the voodoo to make slightly
more sense here, but it still feels like there's a long
way to go.

All the best

Conor