[Agda] Re: with + continuation

[Andreas Abel]

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'.


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

Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY

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