[Agda] Re: with + continuation

[Peter Divianszky]

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 would be translated to something like this (g1 and g2 would be 
applied on the pattern variables instead of the patterns):

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

Cheers,
Peter