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