[Agda] Re: with + continuation

[Peter Divianszky]

On 17/11/2012 12:57, Peter Divianszky wrote:
> Hi,
>
> 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 e
>    x  ∈? y ∷ ys | no ¬p | no ¬q | there r = ¬q r
> ---------------------
>
> What do you think, is there any chance for 'withcont'?
>
> Cheers,
> Peter
>

I made a typo, 'e' should be 'refl':

---------------------
    _∈?_ : ∀ (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
---------------------