vertical application (Re: [Agda] Re: with + continuation)

[Peter Divianszky]

>> f p11 p12 p13 = exp1
>> f p21 p22 p23 | λ q1 → e1
>> f p31 p32 p33 |   q2 → e2
>> f p11 p12 p13 | exp2
>> f p41 p42 p43 | λ r11 r12 → h1
>> f p51 p52 p53 |   r21 r22 → h2
>> f p61 p62 p63 |   r31 r32 → h3
>
> This syntax is very confusing to me, because the expression is split up
> over multiple lines.

Thanks for the feedback.

Only the top level application is split up over multiple lines, no other 
expressions. I would call this "vertical application".
One should consider that vertical application is more readable than 
individual local function definitions or not. For me, yes, it is.

> And what if you wanted to write "f (g l1 l2) l3"
> where l1, l2 and l3 are lambdas? Should there be unbalanced parentheses
> on some lines? Or should you rewrite the expression in some combinator
> form? I think you are better of just writing the functions explicitly.

This would I call nested vertical application.
I'll show examples at the end of the mail.

> Another alternative is to allow overriding of function arguments in
> pattern matching lambdas. I am thinking of something like:
>
>      x ∈? y ∷ ys | no ¬p | no ¬q = no
>        λ{ here where x = .y → ¬p refl
>         ; there r           → ¬q r }
>
> The idea would be that "where Var = Pat" replaces the variable by the
> given pattern in that case alternative. So a lambda containing a pattern
> with a 'where' clause desugars to one with the variable as an extra
> argument. But this might get a bit tricky with hidden arguments.

This would be another solution, I would use it if it was available.


I would like to adjust the syntax of my proposal a bit.
I would allow only lambda arguments in the vertical application, but 
maybe with zero arguments. For example,

f p11 p12 p13 = exp1
f p21 p22 p23 | λ q1 → e1
f p31 p32 p33 |   q2 → e2
f p41 p42 p43 | λ → exp2
f p51 p52 p53 | λ r11 r12 → h1
f p61 p62 p63 |   r21 r22 → h2
f p71 p72 p73 |   r31 r32 → h3

would stand for something like

f p11 p12 p13 = exp1 (g1 p11 p12 p13) g2 (p41 p42 p43) (g3 p11 p12 p13)
   where
    g1 : ...
    g1 p21 p22 p23 q1 = e1
    g1 p31 p32 p33 q2 = e2
    g2 : ...
    g2 p41 p42 p43 = exp2
    g3 : ...
    g3 p51 p52 p53 r11 r12 = h1
    g3 p61 p62 p63 r21 r22 = h2
    g3 p71 p72 p73 r31 r32 = h3

I would allow nested vertical application like

f p11 p12 p13 = e1
f p21 p22 p23 | λ q1 → e2
f p31 p32 p33 |   q2 → e3
f p41 p42 p43 |   q3 | λ q4 → e4
f p51 p52 p53 | λ q5  q6  → e5
f p61 p62 p63 |   q7  q8  | λ q9  → e6
f p71 p72 p73 |   q10 q11 |   q12 → e7

which would stand instead of

f p11 p12 p13 = e1
               ( λ { q1 → e2
                   ; q2 → e3
                        ( λ q4 → e4 ) } )
               ( λ { q5  q6  → e5
                             ( λ { q9  → e6
                                 ; q12 → e7 } ) } )

but it would allow overriding of function arguments as you called it.

Your example "f (g l1 l2) l3" would look like

... = f
... | λ → l1
... |   | l2
... | l3

where l1, l2 and l3 are lambdas.


I would like to extend the semantics of my proposal even more so that it 
could be used conveniently with arbitrary eliminators also.
I'm not sure how to do this, but I have the following example in mind:

-------------------------
ℕ-elim : ∀ (P : ℕ → Set)
            n (z : P zero) (s : ∀ m → P m → P (suc m)) → P n
ℕ-elim P zero z s = z
ℕ-elim P (suc n) z s = s _ (ℕ-elim P n z s)

data _≤_ : ℕ → ℕ → Set  where
   z≤n : ∀ n → zero ≤ n
   s≤s : ∀ n m → n ≤ m → suc n ≤ suc m

≤-refl : ∀ n → n ≤ n
≤-refl n = ℕ-elim (λ k → k ≤ k) n
≤-refl .zero    | λ → z≤n zero
≤-refl .(suc m) | λ m r → s≤s m m r
-------------------------

which would mean

-------------------------
≤-refl : ∀ n → n ≤ n
≤-refl n = ℕ-elim (λ k → k ≤ k) n (f1 zero refl) (λ m r → f2 (suc m) m r 
refl)  where

   f1 : (n : ℕ) → n ≡ zero → n ≤ n
   f1 .zero  refl = z≤n zero

   f2 : (n : ℕ) → ∀ m → m ≤ m → n ≡ suc m → n ≤ n
   f2 .(suc m)  m r refl = s≤s m m r
-------------------------

but I am not sure how to make the transformation in the general case.
Note that this example is not a "useful" example, the normal definition 
of ≤-refl is shorter.


Cheers,
Peter