[Agda] A different implementation of --without-K

Andreas Abel andreas.abel at ifi.lmu.de
Mon Apr 28 21:55:27 CEST 2014


-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA1

Excellent!  Pushed your patch.

There is also the wiki pages,

  http://wiki.portal.chalmers.se/agda/pmwiki.php?n=ReferenceManual.Pragmas

but these should be updated only after the release, I guess.

Cheers,
Andreas

On 28.04.2014 11:16, Jesper Cockx wrote:
> Below is a proposal for the patch notes, including some examples.
> I'm also attaching the notes as a darcs patch.
> 
> * Changed the semantics of --without-K. [Issue 712, Issue 865,
> Issue 1025]
> 
> New specification of --without-K:
> 
> When --without-K is enabled, the unification of indices for pattern
> matching is restricted in two ways:
> 
> 1. Reflexive equations of the form x == x are no longer solved, 
> instead Agda gives an error when such an equation is encountered.
> 
> 2. When unifying two same-headed constructor forms 'c us' and 'c 
> vs' of type 'D pars ixs', the datatype indices ixs (but not the
> parameters) have to be *self-unifiable*, i.e. unification of ixs
> with itself should succeed positively. This is a nontrivial
> requirement because of point 1.
> 
> Examples:
> 
> * The J rule is accepted.
> 
> J : {A : Set} (P : {x y : A} → x ≡ y → Set) → (∀ x → P (refl x)) → 
> ∀ {x y} (x≡y : x ≡ y) → P x≡y J P p (refl x) = p x
> 
> This definition is accepted since unification of x with y doesn't
> require deletion or injectivity.
> 
> * The K rule is rejected.
> 
> K : {A : Set} (P : {x : A} → x ≡ x → Set) → (∀ x → P (refl {x =
> x})) → ∀ {x} (x≡x : x ≡ x) → P x≡x K P p refl = p _
> 
> Definition is rejected with the following error:
> 
> Cannot eliminate reflexive equation x = x of type A because K has 
> been disabled. when checking that the pattern refl has type x ≡ x
> 
> * Symmetry of the new criterion.
> 
> test₁ : {k l m : ℕ} → k + l ≡ m → ℕ test₁ refl = zero
> 
> test₂ : {k l m : ℕ} → k ≡ l + m → ℕ test₂ refl = zero
> 
> Both versions are now accepted (previously only the first one
> was).
> 
> * Handling of parameters.
> 
> cons-injective : {A : Set} (x y : A) → (x ∷ []) ≡ (y ∷ []) → x ≡ y 
> cons-injective x .x refl = refl
> 
> Parameters are not unified, so they are ignored by the new 
> criterion.
> 
> * A larger example: antisymmetry of ≤.
> 
> data _≤_ : ℕ → ℕ → Set where lz : (n : ℕ) → zero ≤ n ls : (m n : ℕ)
> → m ≤ n → suc m ≤ suc n
> 
> ≤-antisym : (m n : ℕ) → m ≤ n → n ≤ m → m ≡ n ≤-antisym .zero
> .zero    (lz .zero) (lz .zero)   = refl ≤-antisym .(suc m) .(suc n)
> (ls m n p) (ls .n .m q) = cong suc (≤-antisym m n p q)
> 
> * [ Issue 1025 ]
> 
> postulate mySpace : Set postulate myPoint : mySpace
> 
> data Foo : myPoint ≡ myPoint → Set where foo : Foo refl
> 
> test : (i : foo ≡ foo) → i ≡ refl test refl = {!!}
> 
> When applying injectivity to the equation "foo ≡ foo" of type "Foo
> refl", it is checked that the index refl of type "myPoint ≡
> myPoint" is self-unifiable. The equation "refl ≡ refl" again
> requires injectivity, so now the index myPoint is checked for
> self-unifiability, hence the error:
> 
> Cannot eliminate reflexive equation myPoint = myPoint of type 
> mySpace because K has been disabled. when checking that the pattern
> refl has type foo ≡ foo
> 
> 
> 
> 
> On Fri, Apr 25, 2014 at 5:37 PM, Andreas Abel
> <andreas.abel at ifi.lmu.de <mailto:andreas.abel at ifi.lmu.de>> wrote:
> 
> Thanks, Jesper, great!
> 
> The new patch applies cleanly (just compiling).
> 
> I just had to remove test/fail/Issue1023.agda (which no longer
> fails, but this is an issue of the termination checker).
> 
> I pushed your patch.
> 
> The release notes now still contain the explanation for my own 
> --without-K, which can now be deleted.  Can you replace them with
> a documentation of your implementation?  See
> 
> doc/release-notes/2-3-4.txt
> 
> A starting point could be your commit message, but it would be nice
> if it was more detailed, including some examples.
> 
> Cheers, Andreas
> 
> On 25.04.2014 11 <tel:25.04.2014%2011>:36, Jesper Cockx wrote:
>> Andreas,
> 
>> It's great to hear that you want to include my patch in 2.3.4!
>> I'm attaching a patch to the latest darcs version that replaces 
>> --without-K with my new semantics. I hope everything is in
>> order, but feel free to make any further changes if necessary.
> 
>> Best, Jesper
> 
> 
>> On Thu, Apr 24, 2014 at 9:29 PM, Andreas Abel 
>> <andreas.abel at ifi.lmu.de <mailto:andreas.abel at ifi.lmu.de>
> <mailto:andreas.abel at ifi.lmu.de <mailto:andreas.abel at ifi.lmu.de>>> 
> wrote:
> 
>> Jesper,
> 
>> we would like to replace the current --without-K implementation 
>> with yours for Agda-2.3.4.
> 
>> The email I am quoting has a patch attached, but that was Nov 
>> 2013. Before I try to apply it, I thought I ask if you have a
>> newer version.
> 
>> Cheers, Andreas
> 
>> On 28.11.2013 16:50, Jesper Cockx wrote:
>>> Dear all,
> 
>>> I added parameter reconstruction to my implementation, as 
>>> suggested by Nils. This rules out the examples WithoutK5.agda, 
>>> WithoutK6.agda and WithoutK9.agda in test/fail (i.e. all the 
>>> variants of weak-K). Some other examples (WithoutK4.agda, 
>>> WithoutK7.agda, WithoutK8.agda and WithoutK10.agda) are still 
>>> accepted, but it seems to me that these don't rely on K in an 
>>> essential way. At least, I am able to define them (in a more 
>>> complicated way) even when the normal --without-K is enabled.
>>> So it seems to be a feature of my flag that these examples are 
>>> accepted, not a bug.
> 
>>> However, I am not convinced that parameter reconstruction is
>>> the correct way to go, as it seriously hampers reasoning about
>>> many parametrized types. Here are two examples that fail when
>>> either --without-K or the new version of --new-without-K is
>>> enabled:
> 
>>> data Unit {l} : Set l where tt : Unit
> 
>>> test? : ? {l} ? _?_ {l} tt tt ? Set? test? refl = Set
> 
>>> data Box (A : Set) : Set where [_] : A ? Box A
> 
>>> test? : (x y : Bool) ? [ x ] ? [ y ] ? x ? y test? x .x refl = 
>>> refl
> 
>>> I wonder if there isn't a better way to handle parameters that 
>>> doesn't rule out natural-looking code like this.
> 
>>> @Dan: Thank you for the encouragement, I'll let you know when
>>> I have a version of the proof that I can show. I agree that we
>>> need a more principled solution for defining higher inductive
>>> types. The current implementation of --new-without-K doesn't 
>>> distinguish individual data types (yet), but I'll look into it 
>>> later.
> 
>>> Jesper Cockx
> 
> 
> 
> 
>>> On Fri, Nov 22, 2013 at 9:16 PM, Dan Licata <drl at cs.cmu.edu
> <mailto:drl at cs.cmu.edu>
>> <mailto:drl at cs.cmu.edu <mailto:drl at cs.cmu.edu>>
>>> <mailto:drl at cs.cmu.edu <mailto:drl at cs.cmu.edu>
> <mailto:drl at cs.cmu.edu <mailto:drl at cs.cmu.edu>>>> wrote:
> 
>>> Hi Jesper,
> 
>>> I think it's great that you're working out the theory of 
>>> without-K---it would be wonderful to know that it actually 
>>> works!
> 
>>> One comment about allowing injectivity and disjointness in 
>>> unification: it would be nice if there were a way to turn this 
>>> on or off for individual datatypes.  The reason is that we use 
>>> datatypes to implement higher inductives types, and the 
>>> constructors for those are not necessarily injective or 
>>> disjoint. Right now, there is a hack for preventing
>>> disjointness from "leaking" outside the implementation of the
>>> higher inductive type (make the constructor take an extra
>>> argument of type (unit -> unit)), but it would be nice if there
>>> were a more principled solution.  I just thought I'd comment,
>>> in case this fits into your new implementation.
> 
>>> -Dan
> 
>>> On Nov22, Jesper Cockx wrote:
>>>> Dear all,
>>>> 
>>>> Lately I have been working on a proof of correctness for the
>>> --without-K
>>>> flag in Agda (someone should do it, right?). The proof
>>>> itself is
>>> not quite
>>>> ready for prime time, but during my investigations I
>>>> actually
>>> discovered a
>>>> more general (and, in my eyes, simpler) formulation of
>>>> pattern
>>> matching
>>>> without K. In order to play around with this idea, I 
>>>> implemented a
>>> new flag
>>>> to Agda. Since a good number of people here seem interested
>>>> in this subject, I thought I'd share it.
>>>> 
>>>> The idea is as follows: Suppose we want to split on a
>>>> variable x
>>> of type "D
>>>> us" for some data type D with constructors "c_j : Delta_j ->
>>>> D vs_j". Instead of putting certain syntactic restrictions
>>>> on the indices
>>> "us" (as
>>>> in the current implementation of --without-K), we limit the
>>> algorithm for
>>>> unification of "us" with "vs_j". We do this by refusing to 
>>>> deleting reflexive equations of the form "x = x" where x is
>>>> a variable. All
>>> other
>>>> unification steps (solution, injectivity, disjointness, and
>>> acyclicity)
>>>> keep working as usual. So for example, we allow unifying
>>>> "suc x"
>>> with "suc
>>>> zero" or "suc x" with "suc y" (where y != x), but not "suc
>>>> x" with
>>> "suc x".
>>>> This should rule out any definitions that depend on K (if my 
>>>> proof is correct). It is also more general than the current 
>>>> implementation,
>>> since
>>>> the current implementation guarantees that we will never 
>>>> encounter
>>> "x = x"
>>>> during unification.
>>>> 
>>>> In the attachment, you can find a patch to darcs agda. At
>>>> the
>>> moment, it
>>>> adds a new flag called --new-without-K that restricts the 
>>>> unification algorithm as described above. Here is an example 
>>>> of the error message:
>>>> 
>>>> K : (A : Set) (x : A) ? (p : x ? x) ? p ? refl K A x refl = 
>>>> refl
>>>> 
>>>> Cannot eliminate reflexive equation x = x of type A because
>>>> K has been disabled. when checking that the pattern refl has
>>>> type x ? x
>>>> 
>>>> One advantage is that this solves the problem where you can 
>>>> split on a variable of type "something ? x", but not "x ? 
>>>> something" (see 
>>>> https://lists.chalmers.se/pipermail/agda/2013/005407.html
>>>> and 
>>>> https://lists.chalmers.se/pipermail/agda/2013/005428.html). 
>>>> For
>>> example,
>>>> the following examples typecheck with --new-without-K
>>>> enabled (but
>>> not with
>>>> the old --without-K):
>>>> 
>>>> foo : (k l m : ?) ? k ? l + m ? {!!} foo .(l + m) l m refl = 
>>>> {!!}
>>>> 
>>>> bar : (n : ?) ? n ? n ? {!!} bar .zero z?n = {!!} bar .(suc
>>>> m) (s?s {m} p) = {!!}
>>>> 
>>>> I also added two tests to /test/succeed and /test/fail.
>>>> 
>>>> What I'd like you to do, is: 1. Try out my modification on 
>>>> your favorite examples, 2. Tell me what you think, 3. If you 
>>>> think it's good, add it to the main Agda branch.
>>>> 
>>>> Best regards, Jesper Cockx
> 
> 
>>>> _______________________________________________ Agda mailing 
>>>> list Agda at lists.chalmers.se <mailto:Agda at lists.chalmers.se>
> <mailto:Agda at lists.chalmers.se <mailto:Agda at lists.chalmers.se>>
>> <mailto:Agda at lists.chalmers.se <mailto:Agda at lists.chalmers.se>
> <mailto:Agda at lists.chalmers.se <mailto:Agda at lists.chalmers.se>>>
>>>> https://lists.chalmers.se/mailman/listinfo/agda
> 
> 
> 
> 
>>> _______________________________________________ Agda mailing 
>>> list Agda at lists.chalmers.se <mailto:Agda at lists.chalmers.se>
> <mailto:Agda at lists.chalmers.se <mailto:Agda at lists.chalmers.se>>
>>> https://lists.chalmers.se/mailman/listinfo/agda
> 
> 
> 
> 
> 
> 
> 
> 

- -- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Department of Computer Science and Engineering
Chalmers and Gothenburg University, Sweden

andreas.abel at gu.se
http://www2.tcs.ifi.lmu.de/~abel/
-----BEGIN PGP SIGNATURE-----
Version: GnuPG v1.4.11 (GNU/Linux)
Comment: Using GnuPG with Thunderbird - http://www.enigmail.net/

iEYEARECAAYFAlNesi8ACgkQPMHaDxpUpLP6/ACfU5RKvcjaJQ5qQBJWxt9wirGC
6doAn26tiVaTz/SbR6rr4/vMg7L1Ukfy
=5+UW
-----END PGP SIGNATURE-----


More information about the Agda mailing list