[Agda] Re: with + continuation

[Twan van Laarhoven]

On 2012-11-17 23:15, Peter Divianszky wrote:
>
>
> On 17/11/2012 14:51, Peter Divianszky wrote:
>> On 17/11/2012 14:25, Andreas Abel wrote:
>>> On 17.11.12 1:07 PM, Peter Divianszky wrote:
>>>>> It would be nice if one could write the following in Agda:
>>>>>
>>>>> ---------------------
>>>>> module _ (f : (A → B) → C) (g : A → B) where
>>>>>
>>>>>    c : C
>>>>>    c withcont f
>>>>>    ... | a = g a
>>>>> ---------------------
>>>>>
>>>>> Given 'f : (A → B) → C', 'withcont f' would give a value of 'A' and it
>>>>> would replace the goal 'C' with 'B'.
>>>>>
>>>>> This could be useful in the following situation:
>>>>>
>>>>> ---------------------
>>>>> open import Data.List using (List; []; _∷_)
>>>>> open import Data.Empty using (⊥)
>>>>> open import Relation.Nullary using (Dec; yes; no)
>>>>> open import Relation.Binary using (Decidable)
>>>>> open import Relation.Binary.PropositionalEquality using (_≡_; refl)
>>>>>
>>>>> module Try {A : Set} {{eq : Decidable {A = A} _≡_}} where
>>>>>
>>>>>    infix 2 _∈_ _∈?_
>>>>>
>>>>>    data _∈_ (x : A) : List A → Set where
>>>>>      here : ∀ {xs} → x ∈ x ∷ xs
>>>>>      there : ∀ {y ys} → x ∈ ys → x ∈ y ∷ ys
>>>>>
>>>>>    _∈?_ : ∀ (x : A) ys → Dec (x ∈ ys)
>>>>>    x  ∈? []  = no λ ()
>>>>>    x  ∈? y ∷ ys with eq x y
>>>>>    .y ∈? y ∷ ys | yes refl = yes here
>>>>>    x  ∈? y ∷ ys | no ¬p with x ∈? ys
>>>>>    x  ∈? y ∷ ys | no ¬p | yes q = yes (there q)
>>>>>    x  ∈? y ∷ ys | no ¬p | no ¬q = no (f x refl)  where
>>>>>      f : ∀ a → x ≡ a → (a ∈ y ∷ ys) → ⊥
>>>>>      f .y e here = ¬p e
>>>>>      f a e (there r) with a | e
>>>>>      f a e (there r) | .x | refl = ¬q r
>>>>> ---------------------
>>>>>
>>>>> This works but I find the following definition of _∈?_ easier to read:
>>>>>
>>>> ---------------------
>>>>     _∈?_ : ∀ (x : A) ys → Dec (x ∈ ys)
>>>>     x  ∈? []  = no λ ()
>>>>     x  ∈? y ∷ ys with eq x y
>>>>     .y ∈? y ∷ ys | yes refl = yes here
>>>>     x  ∈? y ∷ ys | no ¬p with x ∈? ys
>>>>     x  ∈? y ∷ ys | no ¬p | yes q = yes (there q)
>>>>     x  ∈? y ∷ ys | no ¬p | no ¬q withcont no
>>>>     .y ∈? y ∷ ys | no ¬p | no ¬q | here    = ¬p refl
>>>>     x  ∈? y ∷ ys | no ¬p | no ¬q | there r = ¬q r
>>>> ---------------------
>>>
>>> Makes sense.  I'd call this `refine' or `with-apply' instead of
>>> `withcont'.
>>
>> 'without' would also make sense because 'no' is missing in the result :)
>
> Alternative syntax:
>
> ---------------------
>    _∈?_ : ∀ (x : A) ys → Dec (x ∈ ys)
>    x  ∈? []  = no λ ()
>    x  ∈? y ∷ ys with eq x y
>    .y ∈? y ∷ ys | yes refl = yes here
>    x  ∈? y ∷ ys | no ¬p with x ∈? ys
>    x  ∈? y ∷ ys | no ¬p | yes q = yes (there q)
>    x  ∈? y ∷ ys | no ¬p | no ¬q = no
>    .y ∈? y ∷ ys | no ¬p | no ¬q | λ here    → ¬p refl
>    x  ∈? y ∷ ys | no ¬p | no ¬q |   there r → ¬q r
> ---------------------
>
> This syntax allows generalization like
>
> 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. 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.

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.


I do like the withcont idea, though. Especially because pattern matching lambdas 
are ugly.


Twan