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

[Dan Licata]

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