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

The unification machinery does not respect η-equality #473

Closed
GoogleCodeExporter opened this Issue Aug 8, 2015 · 27 comments

Comments

Projects
None yet
2 participants
@GoogleCodeExporter
Copy link

GoogleCodeExporter commented Aug 8, 2015

module Bug where

data I : Set where
  i : I

record Box (A B : Set) : Set where
  constructor [_]
  field contents : A

data D : Set → Set₁ where
  d₁ : (R : Set) → D R
  d₂ : (i : I) (R : I → Set) → D (R i) → D (Box I (R i))

data S : (R : Set) → R → D R → Set₁ where
  s : (i : I) (R : I → Set) (p : D (R i)) →
      S (Box I (R i)) [ i ] (d₂ i R p)

postulate
  P : I → Set

-- The unification machinery doesn't respect η-equality:

Fails : (e : Box I (P i)) → S (Box I (P i)) e (d₂ i P (d₁ (P i))) → 
Set₁
Fails .([ i ]) (s .i .P .(d₁ (P i))) = Set

-- Refuse to solve heterogeneous constraint p : D (P (Box.contents e))
-- =?= d₁ (P i) : D (P i)
-- when checking that the pattern s .i .P .(d₁ (P i)) has type
-- S e (d₂ i P (d₁ (P i)))

-- One can avoid this problem by explicitly pattern matching on record
-- constructors:

Works : (e : Box I (P i)) → S (Box I (P i)) e (d₂ i P (d₁ (P i))) → 
Set₁
Works [ .i ] (s .i .P .(d₁ (P i))) = Set

-- However, this seems like a hack.

Original issue reported on code.google.com by nils.anders.danielsson on 23 Sep 2011 at 3:40

@GoogleCodeExporter

This comment has been minimized.

Copy link

GoogleCodeExporter commented Aug 8, 2015

I'm not sure I'd classify this as not respecting eta. In the working case the 
only thing you've changed is that you're supplying more hints to the unifier, 
it isn't an eta contracted/expanded version of the failing case. Here's another 
example where providing a record constructor makes a difference:

works : Box ⊥ I → I
works [ () ]  -- also a hack?

fails : Box ⊥ I → I
fails ()

Original comment by ulf.nor...@gmail.com on 23 Sep 2011 at 6:25

@GoogleCodeExporter

This comment has been minimized.

Copy link

GoogleCodeExporter commented Aug 8, 2015

Your example is somewhat different, in that the use of () is essential. In my 
case I would want to avoid the e argument altogether (by making it implicit).

Andreas, do you have an opinion on this?

Original comment by nils.anders.danielsson on 24 Sep 2011 at 5:34

@GoogleCodeExporter

This comment has been minimized.

Copy link

GoogleCodeExporter commented Aug 8, 2015

Clearly, eta-equality is not always respected, since currently the test, 
whether we can go back from a heterogeneous situation to a homogeneous one uses 
a syntactic equality test on the types.

In this particular case, however, the setting

  i := Box.contents e

has already be made, but it is not propagated properly somehow, this is a bug.

Original comment by andreas....@gmail.com on 26 Sep 2011 at 7:41

  • Changed state: Accepted
  • Added labels: Priority-High
@GoogleCodeExporter

This comment has been minimized.

Copy link

GoogleCodeExporter commented Aug 8, 2015

Ulf, I do not understand why ureduce does not propagate the substitution 
everywhere.

The postponed constraint is

  unifyAtom Box I (R i) =?= Box I (P i) : Set

Then, after the assignment, it gets awaken
i := Box.contents e
unifyHH (Box I (R (Box.contents e))) (Box I (P i)) : Set
unifyAtom Box I (R (Box.contents e)) =?= Box I (P i) : Set

Why has i only be substituted on the left hand side??  Is there some problems 
with variable indices?

Original comment by andreas....@gmail.com on 26 Sep 2011 at 8:01

Attachments:

@GoogleCodeExporter

This comment has been minimized.

Copy link

GoogleCodeExporter commented Aug 8, 2015

I think you're confusing i and i. If you change the definition of S to

data S : (R : Set) → R → D R → Set₁ where
  s : (j : I) (R : I → Set) (p : D (R j)) →
      S (Box I (R j)) [ j ] (d₂ j R p)

it's easier to debug. The problem is that unification picks the solution

  j := Box.contents e

instead of

  e := [ j ]

and then it unify Box.contents e with i.

Anyway, here's a simpler example:

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

open _×_

data Nat : Set where
  zero : Nat
  suc  : Nat → Nat

data Zero : Nat → Set where
  zero : Zero zero

data Zero₂ : Nat → Nat → Set where
  zero : Zero₂ zero zero

f₁ : (p : Nat × Nat) → Zero₂ (fst p) (snd p) → Set
f₁ (.zero , .zero) zero = Nat    -- works
-- f₁ .(zero , zero) zero = Nat  -- fails

f₂ : (p : Nat × Nat) → Zero (fst p) → Set
f₂ (.zero , y) zero = Nat  -- works
-- foo .?? zero             -- fails (nothing to write in place of ??)

f₁ is the same as the original example. Both fields are instantiated by
unification, but if we try to make the pair unify it doesn't work. f₂ shows
why it doesn't work (without some special magic). It's really hard to
distinguish the case where all fields can be instantiated from the case
where only some of them can be.

Original comment by ulf.nor...@gmail.com on 26 Sep 2011 at 9:10

  • Added labels: Priority-Low
  • Removed labels: Priority-High
@GoogleCodeExporter

This comment has been minimized.

Copy link

GoogleCodeExporter commented Aug 8, 2015

"and then it unify Box.contents e with i." should be
"and then it fails to unify Box.contents e with i."

Original comment by ulf.nor...@gmail.com on 26 Sep 2011 at 9:11

@GoogleCodeExporter

This comment has been minimized.

Copy link

GoogleCodeExporter commented Aug 8, 2015

I suppose something we could to is always eta expand implicit arguments of 
record type before type checking the left hand side. At the moment, if we make 
p implicit in f₁, the left hand side

  f₁ zero

expands into

  f₁ ?p zero

where the ? indicates that the pattern could be dotted if necessary. We then 
type check this getting
either f₁ p zero, f₁ .v zero, or as in this case, a type error.

It shouldn't be that hard to change the implicit expansion to produce

  f₁ (?x , ?y) zero

which would make it type check. It would also solve the original example 
provided you make e implicit.
It would also take care of f₂ with implicit p which is a nice bonus.

Original comment by ulf.nor...@gmail.com on 26 Sep 2011 at 9:27

  • Added labels: Priority-Medium
  • Removed labels: Priority-Low
@GoogleCodeExporter

This comment has been minimized.

Copy link

GoogleCodeExporter commented Aug 8, 2015

I implemented that and it solves the problem. However, always expanding 
implicit record arguments leads to problems with issue 456. More metas will be 
applied to record values and thus won't be solved unless we fix issue 456.

Original comment by ulf.nor...@gmail.com on 26 Sep 2011 at 12:36

@GoogleCodeExporter

This comment has been minimized.

Copy link

GoogleCodeExporter commented Aug 8, 2015

Blocked on issue 456

Original comment by ulf.nor...@gmail.com on 26 Sep 2011 at 12:39

  • Changed state: Blocked
@GoogleCodeExporter

This comment has been minimized.

Copy link

GoogleCodeExporter commented Aug 8, 2015

Original comment by ulf.nor...@gmail.com on 26 Sep 2011 at 12:40

@GoogleCodeExporter

This comment has been minimized.

Copy link

GoogleCodeExporter commented Aug 8, 2015

Original comment by andreas....@gmail.com on 26 Mar 2012 at 2:39

  • Added labels: Eta, Meta, Pattern-Matching
@GoogleCodeExporter

This comment has been minimized.

Copy link

GoogleCodeExporter commented Aug 8, 2015

Since 456 is solved, Ulf, you could try to integrate your fix again...

Original comment by andreas....@gmail.com on 29 Mar 2012 at 8:37

  • Changed state: Accepted
@GoogleCodeExporter

This comment has been minimized.

Copy link

GoogleCodeExporter commented Aug 8, 2015

I have "rolled forward" Ulf's fix. The test suite doesn't complain.

Can someone describe this change in the release notes (if necessary)?

Original comment by nils.anders.danielsson on 29 Mar 2012 at 9:59

@GoogleCodeExporter

This comment has been minimized.

Copy link

GoogleCodeExporter commented Aug 8, 2015

I would not know what to write.  Something broken works now.  Maybe Ulf can 
write something, since he fixed this.

Does this have a negative impact on runtime?

Original comment by andreas....@gmail.com on 30 Mar 2012 at 1:33

@GoogleCodeExporter

This comment has been minimized.

Copy link

GoogleCodeExporter commented Aug 8, 2015

No visible runtime impact. I'm not sure what to write that's not going into 
implementation specifics. Maybe "Unification now preserves (more) eta 
equalities", but I agree with Andreas that this isn't something that a user 
would notice unless they ran into exactly this problem.

Original comment by ulf.nor...@gmail.com on 30 Mar 2012 at 2:02

  • Changed state: Fixed
@GoogleCodeExporter

This comment has been minimized.

Copy link

GoogleCodeExporter commented Aug 8, 2015

Original comment by andreas....@gmail.com on 19 Oct 2012 at 8:06

  • Added labels: PatternMatching
  • Removed labels: Pattern-Matching
@GoogleCodeExporter

This comment has been minimized.

Copy link

GoogleCodeExporter commented Aug 8, 2015

Fix is probable cause of issue 635.

Original comment by andreas....@gmail.com on 29 Oct 2012 at 6:13

@GoogleCodeExporter

This comment has been minimized.

Copy link

GoogleCodeExporter commented Aug 8, 2015

Issue 635 is fixed if we only eta-expand implicit patterns of record type which 
has a constructor.  I restrict the fix for 473 to this case.

Original comment by andreas....@gmail.com on 21 Mar 2013 at 9:51

@GoogleCodeExporter

This comment has been minimized.

Copy link

GoogleCodeExporter commented Aug 8, 2015

Added the following explanation to the release notes:

* Implicit patterns of record type are now only eta-expanded if there
  is a record constructor. [Issues 473, 635]

    data D : Set where
      d : D

    data P : D → Set where
      p : P d

    record Rc : Set where
      constructor c
      field f : D

    works : {r : Rc} → P (Rc.f r) → Set
    works p = D

  This works since the implicit pattern {r} is eta-expanded to
  {c x} which allows the type of p to reduce to P x and x to be
  unified with d.  The corresponding explicit version is:

    works' : (r : Rc) → P (Rc.f r) → Set
    works' (c .d) p = D

  However, if the record constructor is removed, the same example will
  fail:

    record R : Set where
      field f : D

    fails : {r : R} → P (R.f r) → Set
    fails p = D

    -- d != R.f r of type D
    -- when checking that the pattern p has type P (R.f r)

  The error is justified since there is no pattern we could write down
  for r.  It would have to look like

    record { f = .d }

  but anonymous record patterns are not part of the language.

Original comment by andreas....@gmail.com on 22 Mar 2013 at 9:26

@GoogleCodeExporter

This comment has been minimized.

Copy link

GoogleCodeExporter commented Aug 8, 2015

> anonymous record patterns are not part of the language.

I think they should be.

Original comment by nils.anders.danielsson on 22 Mar 2013 at 9:54

@GoogleCodeExporter

This comment has been minimized.

Copy link

GoogleCodeExporter commented Aug 8, 2015

Is there a reason why they are not?  Has there been a discussion about this?

Original comment by andreas....@gmail.com on 22 Mar 2013 at 10:17

@GoogleCodeExporter

This comment has been minimized.

Copy link

GoogleCodeExporter commented Aug 8, 2015

No one has implemented it yet. Furthermore it doesn't seem extremely
useful (ignoring issues like the one discussed here), because the
"obvious" syntax is rather heavy-weight:

  uncurry f (record { proj₁ = x; proj₂ = y }) = f x y

Original comment by nils.anders.danielsson on 22 Mar 2013 at 12:25

@GoogleCodeExporter

This comment has been minimized.

Copy link

GoogleCodeExporter commented Aug 8, 2015

The syntax could be made more lightweight by allowing puns and the omission of 
fields, as in Haskell.

  uncurry f (record { proj1; proj2 }) = f proj1 proj2

Original comment by andreas....@gmail.com on 22 Mar 2013 at 3:00

@GoogleCodeExporter

This comment has been minimized.

Copy link

GoogleCodeExporter commented Aug 8, 2015

Unfixed by 
https://github.com/agda/agda/commit/217c98406217f8224fd50603d483791658b029f8

Original comment by andreas....@gmail.com on 10 Jun 2015 at 12:20

  • Changed state: Accepted
@GoogleCodeExporter

This comment has been minimized.

Copy link

GoogleCodeExporter commented Aug 8, 2015

The prefix fix has serious performance problems for large records as hidden 
function arguments:

open import Common.Prelude
open import Common.Product

T : Nat → Set
T zero = ⊤
T (suc n) = T n × T n

test : {r : T 9} → Bool → Set
test true = Nat
test false = Bool

takes >90 s (Andreas' Dell E7440)
T 7: 2s
T 8: 13 s

Agda.Utils.Permutation.topoSort is implemented naively, has quadratic best case 
behavior.

Original comment by andreas....@gmail.com on 10 Jun 2015 at 12:29

@GoogleCodeExporter

This comment has been minimized.

Copy link

GoogleCodeExporter commented Aug 8, 2015

Issue 1575 has been merged into this issue.

Original comment by nils.anders.danielsson on 25 Jun 2015 at 4:48

@GoogleCodeExporter

This comment has been minimized.

Copy link

GoogleCodeExporter commented Aug 8, 2015

Unfix reverted by 
https://github.com/agda/agda/commit/6cfd5b56d57fc67dfe30d1b75475e14b97e13c25

For backwards compatibility (see issue 1575), this issue has to stay fixed, 
even if the fix has to be improved.

Original comment by andreas....@gmail.com on 10 Jul 2015 at 10:22

  • Changed state: Fixed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment