[Agda] Re: with + continuation
Peter Divianszky
divipp at gmail.com
Sat Nov 17 14:51:12 CET 2012
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 :)
More information about the Agda
mailing list