[Agda-dev] Clauses and trailing implicit arguments

[Andreas Abel]

In short, yes, this is the intended behavior.

Of course, it seems weird that one clause has one more pattern variable, 
and the other a lambda instead.  One could try to canonize compiled 
clauses, e.g. that all the lambdas are turned into pattern variables, or 
all the trailing pattern variables that are not matched on are turned 
into lambdas.

But be aware that there are cases the clauses genuinely have different 
arities, e.g.

Sum : Nat → Set
Sum 0       = Nat
Sum (suc n) = Nat → Sum n

sum : (acc : Nat) (n : Nat) → Sum n
sum acc 0         = acc
sum acc (suc n) 0 = sum acc n
sum acc (suc n) m = sum (m + acc) n

Cheers,
Andreas

On 20.01.2015 01:39, Philipp Hausmann wrote:
> Hi,
>
> I have a question about the internal Clauses/CompiledClauses
> representation of Agda. I just learned that for certain corner-cases,
> different clauses of the same function may take a different number of
> arguments. This seems to break the Epic (and my own new) backend;
> MAlonzo  isn't affected.
>
> It happens when an implicit argument is in trailing position, for example:
>
> data Nat : Set where
>    Z : Nat
>    S : Nat -> Nat
>
> f : (k : Nat) {l : Nat} -> Nat
> f Z {l = q} = q
> f (S a) = a
>
> This will yield the following clause patterns:
> [[]r(ConP Test.Nat.Z(inductive)[] Nothing []),[]r{VarP "l"}] => length 2
> [[]r(ConP Test.Nat.S(inductive)[] Nothing [[]r(a = VarP "a")])] => length 1
>
> And the following CompiledClauses:
> case 0 of
>    Test.Nat.Z -> done[[]r{"l"}] Var 0 []
>    Test.Nat.S ->
>      done[[]r("a")] Shared #44{Lam (ArgInfo {argInfoHiding = Hidden,
> argInfoRelevance = Relevant, argInfoColors = []}) (Abs ".l" Var 1 [])}
>
> For the "f Z {l = q}", the clause has 2 arguments. For the "f (S a)"
> case, the clause has only one argument. Instead, a new lambda is
> introduced inside the clause itself.
>
> It seems to happen very rarely, the only two places I've seen it so far
> in the stdlib are:
> Data.Nat.DivMod._divMod_.dm
> Data.Vec.Properties.sum-++-commuteFun
>
>
> I think I can work around this in my own code, but I was wondering if
> this is indeed the intended behavior?
>
> Cheers,
> Philipp
> _______________________________________________
> Agda-dev mailing list
> Agda-dev at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda-dev

-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Department of Computer Science and Engineering
Chalmers and Gothenburg University, Sweden

andreas.abel at gu.se
http://www2.tcs.ifi.lmu.de/~abel/