Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Higher order matching in rewrite rules #1563

Closed
GoogleCodeExporter opened this issue Aug 8, 2015 · 17 comments
Assignees

Comments

@GoogleCodeExporter
Copy link

@GoogleCodeExporter GoogleCodeExporter commented Aug 8, 2015

Having higher order matching in rewrite rules would be nice.

Here are three concrete examples of things that I would really like to be able to do. They might be simpler to implement than higher order matching because it seems like they only involve recognizing constant things. I also welcome workarounds, if someone has some.

postulate
  _↦_ :  {i} {A : Set i}  A  A  Set i
  idr :  {i} {A : Set i} {a : A}  a ↦ a
{-# BUILTIN REWRITE _↦_ #-}

infix 3 _==_

data _==_ {A : Set} (a : A) : A → Set where
  idp : a == a

ap : {A B : Set} (f : A  B) {x y : A} 
  x == y  f x == f y
ap f idp = idp

record _×_ (A B : Set) : Set where
  constructor _,_
  field
    fst : A
    snd : B
open _×_



{- Cartesian product -}

module _ {A B : Set} where

  _,=_ : {a a' : A} (p : a == a') {b b' : B} (q : b == b')  (a , b) == (a' , b')
  idp ,= idp = idp

  -- Does not work
  ap-,-l : (b : B) {a a' : A} (p : a == a') 
    ap (λ z  z , b) p ↦ (p ,= idp)
  ap-,-l b idp = idr
  {-# REWRITE ap-,-l #-}

  -- Does not work
  ap-,-r : (a : A) {b b' : B} (p : b == b') 
    ap (λ z  a , z) p ↦ (idp ,= p)
  ap-,-r a idp = idr
  {-# REWRITE ap-,-r #-}
  --
  -- Workaround for [ap-,-r] : use [_,_ a] for the function instead
  -- of [λ z → a , z]
  -- I haven’t found a similar workaround for [ap-,-l]



{- Function extensionality -}

module _ {A B : Set} {f g : AB} where

  postulate
    funext : ((x : A)  f x == g x)  f == g

  -- Does not work
  postulate
    ap-app-funext : (a : A) (h : (x : A)  f x == g x) 
      ap (λ f  f a) (funext h) ↦ h a
  {-# REWRITE ap-app-funext #-}



{- Dependent paths -}

module _ where
  PathOver : {A : Set} (B : A  Set)
    {x y : A} (p : x == y) (u : B x) (v : B y)  Set
  PathOver B idp u v = (u == v)

  -- Does not work
  postulate
    PathOver-triv : {A B : Set} {x y : A} (p : x == y) (u v : B) 
      (PathOver (λ _  B) p u v) ↦ (u == v)
  {-# REWRITE PathOver-triv #-}

Original issue reported on code.google.com by guillaum...@gmail.com on 12 Jun 2015 at 9:50

@GoogleCodeExporter

This comment has been minimized.

Copy link
Author

@GoogleCodeExporter GoogleCodeExporter commented Aug 8, 2015

Also, I don’t think I care at all about non-linearity, so if removing non-linearity of matching makes the implementation of higher order matching easier, that’s completely fine by me.

Why was non-linear matching introduced? I can’t find any example of non-linear rewrite rule in the test suite.

Original comment by guillaum...@gmail.com on 12 Jun 2015 at 7:28

@GoogleCodeExporter

This comment has been minimized.

Copy link
Author

@GoogleCodeExporter GoogleCodeExporter commented Aug 8, 2015

Also, I don’t think I care at all about non-linearity, so if removing 
non-linearity of matching makes the implementation of higher order matching 
easier, that’s completely fine by me.

Why was non-linear matching introduced? I can’t find any example of 
non-linear rewrite rule in the test suite.

Original comment by guillaum...@gmail.com on 12 Jun 2015 at 7:28

@GoogleCodeExporter

This comment has been minimized.

Copy link
Author

@GoogleCodeExporter GoogleCodeExporter commented Aug 8, 2015

We had a bit of fun experimenting with REWRITE to quote expressions during AIM and non-linear matchings allow you to determine whether two variables are equal or not which is handy. See myComparemm in the attached file (or below).

Not sure if it could be pushed far enough to actually be useful.

module RewriteQuote where

open import Data.Bool
open import Data.Nat
open import Function

open import Relation.Nullary
open import Relation.Binary.PropositionalEquality

infixr 5 _`+_
data Q : Set → Set₁ where
  `0   : Q ℕ
  `s   : Q ℕ  Q ℕ
  _`+_ : Q ℕ  Q ℕ  Q ℕ
  lift : (A : Set) (a : A)  Q A
  pair : (m n : ℕ)  Q Bool

postulate

  myQuote : (A : Set)  Q A  Q A  Set
  myQuote0 : myQuote ℕ (lift ℕ 0) `0
  myQuotes : (m : ℕ)  myQuote ℕ (lift ℕ (suc m)) (`s (lift ℕ m))
  myQuote+ :  m p  myQuote ℕ (lift ℕ (m + p)) (lift ℕ m `+ lift ℕ p)
  myComparemm : (m : ℕ)    myQuote _ (pair m m) (lift _ true)
  myComparemn : (m n : ℕ)  myQuote _ (pair m n) (lift _ false)

{-# BUILTIN REWRITE myQuote #-}
{-# REWRITE myQuote0 #-}
{-# REWRITE myQuotes #-}
{-# REWRITE myQuote+ #-}
{-# REWRITE myComparemm #-}

Original comment by g.x.all...@gmail.com on 15 Jun 2015 at 10:01

Attachments:

@GoogleCodeExporter

This comment has been minimized.

Copy link
Author

@GoogleCodeExporter GoogleCodeExporter commented Aug 8, 2015

So the idea is that "myQuote _ (pair m m)" can potentially be rewritten to both "lift _ true" (with myComparemm) and to "lift _ false" (with myComparemn), but it happens that myComparemm is defined first, so Agda will choose that one. Is that correct?

Doesn’t seem very safe to me :)

Original comment by guillaum...@gmail.com on 15 Jun 2015 at 10:08

@GoogleCodeExporter

This comment has been minimized.

Copy link
Author

@GoogleCodeExporter GoogleCodeExporter commented Aug 8, 2015

Non-linear matching was introduced because we needed to do equality checks during matching anyway, so adding it was not a big effort. You can use it to implement primTrustMe-like constructs, though I'm not sure if it's useful for anything else.

In other news, I added made a first attempt at higher order matching by adding lambdas to the pattern language (056df10). You can now match against a lambda on the left-hand side:

{-# BUILTIN REWRITE _≡_ #-}

postulate is-id :  {A : Set}  (A  A)  Bool
postulate is-id-true :  {A}  is-id {A} (λ x  x) ≡ true

{-# REWRITE is-id-true #-}

test₁ : is-id {Nat} (λ x  x) ≡ true
test₁ = refl

postulate is-const :  {A : Set}  (A  A)  Bool
postulate is-const-true :  {A} (x : A)  is-const (λ _  x) ≡ true

{-# REWRITE is-const-true #-}

test₂ : is-const {Nat} (λ _  42) ≡ true
test₂ = refl

Your first and third example should work now, though the second doesn't work yet because there is no application pattern. This shouldn't be too hard to add as well.

Please confirm that the rewrite rules in your example work as intended :)

Original comment by jesper.c...@gmail.com on 20 Jun 2015 at 6:42

@GoogleCodeExporter

This comment has been minimized.

Copy link
Author

@GoogleCodeExporter GoogleCodeExporter commented Aug 8, 2015

Thanks!
My first and third example do work indeed :-)

Something else broke though, see the following example which I think used to work:

data _==_ {A : Set} (a : A) : A → Set where
  idp : a == a
{-# BUILTIN REWRITE _==_ #-}

ap : {A B : Set} (f : A  B) {x y : A} 
  x == y  f x == f y
ap f idp = idp

{- Circle -}
postulate
  Circle : Set
  base : Circle
  loop : base == base

module _ (P : Set) (base* : P) (loop* : base* == base*) where

  postulate
    Circle-rec : Circle  P
    Circle-base-recβ : Circle-rec base == base*
  {-# REWRITE Circle-base-recβ #-}


f : Circle  Circle
f = Circle-rec Circle base loop

postulate
  rewr : ap (λ z  f (f z)) loop == loop
{-# REWRITE rewr #-}

test : ap (λ z  f (f z)) loop == loop
test = idp  -- Does not work
{-
Agda does not manage to use [rewr] to rewrite the LHS. It works if
I unfold the two [f] by hand, but I’d prefer not to have to do that.
-}

Original comment by guillaum...@gmail.com on 20 Jun 2015 at 11:05

@GoogleCodeExporter

This comment has been minimized.

Copy link
Author

@GoogleCodeExporter GoogleCodeExporter commented Aug 8, 2015

I fixed the issue in b077aa2

I also added a new pattern for lambda-bound variables applied to arguments (5c42006), so now your second example should work as well. I'm hopeful that there's not actually a need for having pattern variables applied to arguments, because that would bring us to our necks in the swamp of higher-order unification.

Original comment by jesper.c...@gmail.com on 21 Jun 2015 at 11:00

@GoogleCodeExporter

This comment has been minimized.

Copy link
Author

@GoogleCodeExporter GoogleCodeExporter commented Aug 8, 2015

Oh, and fixed (hopefully).

Original comment by jesper.c...@gmail.com on 21 Jun 2015 at 11:02

  • Changed state: Fixed
@GoogleCodeExporter

This comment has been minimized.

Copy link
Author

@GoogleCodeExporter GoogleCodeExporter commented Aug 8, 2015

Thanks!

My second example works now but a slightly improved version of it (which I think should still work) fails with the error

ap-app is not a legal rewrite rule, since the following variables are not
bound by the left hand side: A
when checking the pragma REWRITE ap-app

Is that expected?

postulate
  _↦_ :  {i} {A : Set i}  A  A  Set i
  idr :  {i} {A : Set i} {a : A}  a ↦ a
{-# BUILTIN REWRITE _↦_ #-}

infix 3 _==_

data _==_ {A : Set} (a : A) : A → Set where
  idp : a == a

ap : {A B : Set} (f : A  B) {x y : A} 
  x == y  f x == f y
ap f idp = idp


{- Function extensionality -}

module _ {A B : Set} {f g : AB} where

  postulate
    funext : ((x : A)  f x == g x)  f == g

  app= : f == g  ({x y : A} (p : x == y)  f x == g y)
  app= p idp = ap (λ h  h _) p

app=idp : {A B : Set} {f : A  B} {x y : A} (p : x == y) 
  app= (idp {a = f}) p ↦ ap f p
app=idp idp = idr
{-# REWRITE app=idp #-}

ap-app : {A B : Set} (a : A) {f g : A  B} (p : f == g) 
  ap (λ f  f a) p ↦ app= p idp
ap-app a idp = idr
{-# REWRITE ap-app #-}

Original comment by guillaum...@gmail.com on 21 Jun 2015 at 11:59

  • Changed state: Accepted
@GoogleCodeExporter

This comment has been minimized.

Copy link
Author

@GoogleCodeExporter GoogleCodeExporter commented Aug 8, 2015

Slightly simplified version:

{- Function extensionality -}

module _ {A B : Set} {f g : AB} where

  postulate
    funext : ((x : A)  f x == g x)  f == g

ap-app : {A B : Set} (a : A) {f g : A  B} (p : f == g) 
  ap (λ f  f a) p ↦ ap (λ h  h a) p
ap-app a idp = idr
{-# REWRITE ap-app #-}

I don’t understand why Agda considers A bound in ap-app-funext (in my original second example) but not in ap-app here.

Also, having actual higher order matching (pattern variables applied to arguments) would be very useful. For instance it would be great to be able to rewrite PathOver (\ x -> f x == g x) p u v to Square u v (ap f p) (ap g p), but for that we need the pattern variables f and g to be applied to the variable x.

But I’ll see how far I can go without it for now.

Original comment by guillaum...@gmail.com on 21 Jun 2015 at 1:03

@GoogleCodeExporter

This comment has been minimized.

Copy link
Author

@GoogleCodeExporter GoogleCodeExporter commented Aug 8, 2015

Other issue: If you add the following before the {- Function extensionality -} module, it gives an internal error:

ap-idf : {A : Set} {x y : A} (p : x == y)  ap (λ x  x) p ↦ p
ap-idf idp = idr
{-# REWRITE ap-idf #-}
An internal error has occurred. Please report this as a bug.
Location of the error: src/full/Agda/TypeChecking/Rewriting/NonLinMatch.hs:210

Presumably, it tries rewriting ap (λ f → f a) p using ap-idf, or something like that.

Original comment by guillaum...@gmail.com on 21 Jun 2015 at 1:28

@GoogleCodeExporter

This comment has been minimized.

Copy link
Author

@GoogleCodeExporter GoogleCodeExporter commented Aug 8, 2015

Ok, I added function types to the pattern language, so the rewrite rules in 9 and 10 should now be accepted. However, I'm not sure what the point of having this rewrite rule is, as it just gets you into an infinite loop.

So the main question if you want to have pattern variables applied to arguments, is whether you want to speculate lambdas for the pattern variables. For example with your rewrite rule, would you expect PathOver (\ x -> f x == x) p u v to be rewritten to Square u v (ap f p) (ap (λ x → x) p)?

I'll take a look at the error in 11 next.

Original comment by jesper.c...@gmail.com on 21 Jun 2015 at 1:44

@GoogleCodeExporter

This comment has been minimized.

Copy link
Author

@GoogleCodeExporter GoogleCodeExporter commented Aug 8, 2015

However, I'm not sure what the point of having this rewrite rule is, as it just gets you into an infinite loop.

Actually in my original file I had app= as a postulate and then I noticed when writing the bug report that I could actually define it by path induction, but I didn’t notice that doing so made the rewrite rule useless.

So the main question if you want to have pattern variables applied to arguments, is whether you want to speculate lambdas for the pattern variables. For example with your rewrite rule, would you expect PathOver (\ x -> f x == x) p u v] to be rewritten to Square u v (ap f p) (ap (λ x → x) p)?

Yes, it seems like the only logical choice. I will have another rewrite rule rewriting ap (λ x → x) p to p anyway.

Original comment by guillaum...@gmail.com on 21 Jun 2015 at 2:28

@GoogleCodeExporter

This comment has been minimized.

Copy link
Author

@GoogleCodeExporter GoogleCodeExporter commented Aug 8, 2015

I fixed the issue in 11: 8da569d

Real higher-order matching seems worth thinking about in the future, but right now I think we have enough progress for one sunday :)

Original comment by jesper.c...@gmail.com on 21 Jun 2015 at 2:34

@GoogleCodeExporter

This comment has been minimized.

Copy link
Author

@GoogleCodeExporter GoogleCodeExporter commented Aug 8, 2015

Yes, we can keep real higher-order matching for later :-)

I have another internal error:

data _==_ {A : Set} (a : A) : A → Set where
  idp : a == a
{-# BUILTIN REWRITE _==_ #-}

ap : {A B : Set} (f : A  B) {x y : A}
   x == y  f x == f y
ap f idp = idp

postulate
  Circle : Set
  base : Circle
  loop : base == base

module _ (A : Set) (base* : A) (loop* : base* == base*) where
  postulate
    Circle-rec : Circle  A
    Circle-base-β : Circle-rec base == base*
  {-# REWRITE Circle-base-β #-}
  postulate
    Circle-loop-β : ap Circle-rec loop == loop*
  {-# REWRITE Circle-loop-β #-}


{- Internal error when doing C-u C-u C-c C-t in the hole -}
test : (x : Circle)  ap (Circle-rec (Circle  Circle) (λ y  y) idp x) 
loop == idp
test = {!!}

{-
An internal error has occurred. Please report this as a bug.
Location of the error: src/full/Agda/TypeChecking/Rewriting/NonLinMatch.hs:178
-}

Original comment by guillaum...@gmail.com on 21 Jun 2015 at 3:56

@GoogleCodeExporter

This comment has been minimized.

Copy link
Author

@GoogleCodeExporter GoogleCodeExporter commented Aug 8, 2015

Hmm, it seems we cannot count on the fact two argument lists have the same length. Fixed (hopefully): 531c5ad

Original comment by jesper.c...@gmail.com on 21 Jun 2015 at 6:00

@andreasabel

This comment has been minimized.

Copy link
Contributor

@andreasabel andreasabel commented Aug 26, 2015

This issue report lead to many fixes, and it is not easy to see what remains to be fixed. I am closing this issue, please open a fresh issue with the left-over enhancement request.

nad added a commit that referenced this issue Sep 19, 2015
@asr asr added the has-attachments label Dec 4, 2015
@asr asr added the rewrite label Jan 13, 2016
@asr asr added rewriting and removed rewrite labels Apr 14, 2016
@jespercockx jespercockx self-assigned this Jun 21, 2019
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
4 participants
You can’t perform that action at this time.