[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