[Agda] A different implementation of --without-K
Andreas Abel
andreas.abel at ifi.lmu.de
Fri Apr 25 17:37:47 CEST 2014
-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA1
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: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>> 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>>> 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>>
>>> https://lists.chalmers.se/mailman/listinfo/agda
>
>
>
>
>> _______________________________________________ Agda mailing
>> list 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/
iEYEARECAAYFAlNagUsACgkQPMHaDxpUpLOnCgCg1iNurGDcak0oxfdX++ijVkVv
NF8Anj1XmAaZoRRmGlr3B1+EaNWNHO4x
=4ejk
-----END PGP SIGNATURE-----
More information about the Agda
mailing list