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

[Andreas Abel]

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

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>> 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> 
>> https://lists.chalmers.se/mailman/listinfo/agda
> 
> 
> 
> 
> _______________________________________________ Agda mailing list 
> 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/

iEYEARECAAYFAlNZZjEACgkQPMHaDxpUpLOH9gCgrDh/4lzQd5RoULL+frfn9tN2
PJgAoMJXuuiB5KDlnjxcyyLECLJ0210F
=CibP
-----END PGP SIGNATURE-----