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

Rewrite rules in parametrized modules #1652

Closed
guillaumebrunerie opened this issue Sep 17, 2015 · 18 comments
Assignees

Comments

@guillaumebrunerie
Copy link
Contributor

@guillaumebrunerie guillaumebrunerie commented Sep 17, 2015

Rewrite rules do not work as I expect in parametrized modules:

{-# OPTIONS --rewriting #-}

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

postulate
  A B : Set
  f g : A  B

module M (x : A) where

  postulate
    rx : f x == g x
  {-# REWRITE rx #-}

  -- Works, but I don’t think it should
  test : (y : A)  f y == g y
  test y = idp
@andreasabel

This comment has been minimized.

Copy link
Contributor

@andreasabel andreasabel commented Sep 17, 2015

The REWRITE pragma gets to see the lambda-lifted type-signature (x : A) -> f x == g x and does not respect the module free vars (getModuleFreeVars) of the current module, here (x : A).

It is easy to make test not work anymore, but do you expect f x to rewrite to g x or simply to refuse the REWIRTE pragma for a signature with free vars?

@andreasabel

This comment has been minimized.

Copy link
Contributor

@andreasabel andreasabel commented Sep 18, 2015

Possibly it is likewise surprising that the following is rejected?

module _ (A : Set) where

  postulate
    plus0p :  {x}  (x + zero) ≡ x

  {-# REWRITE plus0p #-}
plus0p  is not a legal rewrite rule, 
since the following variables are not bound by the left hand side:  A
when checking the pragma REWRITE plus0p
@guillaumebrunerie

This comment has been minimized.

Copy link
Contributor Author

@guillaumebrunerie guillaumebrunerie commented Sep 18, 2015

I would expect f x to rewrite to g x.

My use case is the following: I want to construct some r : (n : Nat) -> f n == g n and register it as a rewrite rule, but the construction of r is by induction on n and for the successor case I need to use the fact that the previous case holds as a rewrite rule.

The scheme I’ve been using so far is the following, which looks reasonable:

r : (n : Nat) -> f n == g n
r O = …
r (S n) =where
  rn : f n == g n
  rn = r n
  {-# REWRITE rn #-}

but I’ve noticed now that this is not safe because of the issue here (the rewrite rule rn works for every n instead of just for this particular n, so it also works for S n so I can just define r (S n) as idp which is obviously wrong).

If there is any relatively safe way to do this kind of "recursively defined rewrite rule", I’d be happy to hear about it.

@andreasabel

This comment has been minimized.

Copy link
Contributor

@andreasabel andreasabel commented Sep 18, 2015

Looks like you want a local rewrite rule.

@guillaumebrunerie

This comment has been minimized.

Copy link
Contributor Author

@guillaumebrunerie guillaumebrunerie commented Sep 18, 2015

Yes :-)
Is it easy to add?

@andreasabel

This comment has been minimized.

Copy link
Contributor

@andreasabel andreasabel commented Sep 18, 2015

Maybe you want some kind of scoped rewrite rules. Maybe the problem is a bit similar to scoped instances.

@guillaumebrunerie

This comment has been minimized.

Copy link
Contributor Author

@guillaumebrunerie guillaumebrunerie commented Sep 18, 2015

Would that ensure that I can use the rewrite rule rn only for this value of n?

Maybe what I want is a kind of termination checked rewrite rule:

r : (n : Nat) -> f n == g n
{-# REWRITE r #-}
r O = …
r (S n) =-- only `r n` can be used there, otherwise it wouldn’t pass the termination checker
@jespercockx

This comment has been minimized.

Copy link
Member

@jespercockx jespercockx commented Oct 5, 2015

"Termination checked rewrite rules" seem really tough to implement, since you need some way to get information about which rewrite rules were used with which parameters in typechecking a term. Otherwise there is no way to accurately check termination of a function with multiple arguments. This would lead us quite far in the direction of extensional type theory, since rewrite rules would basically become some kind of heuristic to insert ephemereal subst's at appropriate places. I'm not sure if this a direction we want Agda to go.

Scoped rewrite rules (and scoped instances for that matter) on the other hand seem like they could be a very sensible addition. What needs to be done is, instead of lambda-lifting the type of the rewrite rule (or instance declaration), it should be applied to free variables and be stored together with its context (as a a kind of closure). Then when the typechecker wants to apply the rewrite rule it has to check that we're still in (an extension of) the stored context. Andreas, does Agda have something internally that could be used to do this?

@UlfNorell

This comment has been minimized.

Copy link
Member

@UlfNorell UlfNorell commented Oct 6, 2015

@jespercockx

This comment has been minimized.

Copy link
Member

@jespercockx jespercockx commented Oct 14, 2015

The similarity of this problem for rewrite rules and for instance arguments has made me think: wouldn't it be better if we used the instance search mechanism for rewrite rules? Instead of defining an element of the rewrite relation and then marking it as a rewrite rule, you could just mark the definition as an instance. I think this would fit quite nicely and reduce the cost of implementing new features for instance arguments/rewriting by a lot.

@jespercockx

This comment has been minimized.

Copy link
Member

@jespercockx jespercockx commented Oct 14, 2015

I fixed this by no longer lifting rewrite rules to the top-level and using Ulf's suggestion instead: e5b647b. This means the original example is rejected, and the example by Andreas is accepted. This also means it matters now whether a {-# REWRITE ... #-} pragma is given inside or outside of a module (see https://github.com/agda/agda/blob/e5b647be9462b4457846306c10703f28a9502ef0/test/succeed/RewritingRuleInParametrizedModule.agda).

Please check whether your use case works now (with the {-# REWRITE rn #-} in a where block) and add it to the test suite if it does.

@jespercockx

This comment has been minimized.

Copy link
Member

@jespercockx jespercockx commented Oct 15, 2015

Never mind, I added two more test cases myself (see eff0638). In https://github.com/agda/agda/blob/eff0638cd71601369545035e5441da576cbce35d/test/succeed/RewritingRuleInWhereBlock.agda, I noticed something funny: if you put a hole in the place of refl in the second clause, the normalized goal type is f n ≡ g n even though f n should be rewritten to g n. But then if you give refl, it is accepted. I wonder what's going on there.

@jespercockx

This comment has been minimized.

Copy link
Member

@jespercockx jespercockx commented Oct 29, 2015

I guess my current fix is somewhat too restrictive. If you open a module, all rewrite rules declared in that module should be generalized over the module telescope (and/or applied to the module arguments, if there are any). However, currently no information is kept about what rewrite rules are declared in a given module. I'm trying to find out where best to put this information now...

@jespercockx

This comment has been minimized.

Copy link
Member

@jespercockx jespercockx commented Oct 30, 2015

Generalizing rewrite rules from a parametrized module isn't as easy as I first thought. In fact, it's not even always possible:

{-# OPTIONS --rewriting #-}
postulate
  _↦_ : ∀ {ℓ} {A : Set ℓ} → A → A → Set ℓ
  foo : Set
{-# BUILTIN REWRITE _↦_ #-}

module _ (bar : Set) where
  postulate r : foo ↦ bar
  {-# REWRITE r #-}

Having the rewrite rule inside the module is ok, but giving it outside of the module (rightfully) gives the following error: r is not a legal rewrite rule, since the following variables are not bound by the left hand side: bar. We could maybe try to check whether the rewrite rule makes sense in the more general context and only generalize it if it does.

@jespercockx

This comment has been minimized.

Copy link
Member

@jespercockx jespercockx commented Nov 12, 2015

I finally thought of a way to automatically generalize the rewrite rules to the correct context (and not further) without having to edit all rewrite rules at the end of each (parametrized) module. Here you go: 5297d70
Of course, this means that un-generalizable rewrite rules like in the last post are no longer allowed, but I'm not sure they would have been very useful anyway. I'm going ahead and close this issue now, but please let me know if there's anything else.

@andreasabel

This comment has been minimized.

Copy link
Contributor

@andreasabel andreasabel commented Nov 17, 2015

LGTM (but I have not tested anything).

@guillaumebrunerie

This comment has been minimized.

Copy link
Contributor Author

@guillaumebrunerie guillaumebrunerie commented Nov 17, 2015

The following does not seem to work:

{-# OPTIONS --rewriting --without-K #-}

open import Agda.Primitive

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

infixr 3 _==_

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

PathOver :  {i j} {A : Set i} (B : A  Set j)
  {x y : A} (p : x == y) (u : B x) (v : B y)  Set j
PathOver B idp u v = (u == v)

syntax PathOver B p u v =
  u == v [ B ↓ p ]

postulate
  PathOver-rewr :  {i j} {A : Set i} {B : Set j} {x y : A} (p : x == y) (u v : B) 
    (PathOver (λ _  B) p u v) ↦ (u == v)
  {-# REWRITE PathOver-rewr #-}

ap :  {i j} {A : Set i} {B : A  Set j} (f : (a : A)  B a) {x y : A}
   (p : x == y)  PathOver B p (f x) (f y)
ap f idp = idp


module _ {i j k} {A : Set i} {B : Set j} {C : Set k} (g : BC) (f : AB) where

  ∘ap : {x y : A} (p : x == y) 
    ap g (ap f p) ↦ ap (λ x  g (f x)) p
  ∘ap idp = idr
  {-# REWRITE ∘ap #-}

  ap∘ : {x y : A} (p : x == y) 
    ap (λ x  g (f x)) p ↦ ap g (ap f p)
  ap∘ p = {!idr!}

It works if ap∘ is put in a different module and it also works if ap is the normal one (with a non-dependent function and no PathOver).

@jespercockx

This comment has been minimized.

Copy link
Member

@jespercockx jespercockx commented Nov 17, 2015

I made a mistake when adding an equality with a module parameter, fixed now: f1282fb

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.