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

[Conor McBride]

On 2 Dec 2013, at 10:46, Nils Anders Danielsson <nad at cse.gu.se> wrote:

> On 2013-11-30 10:34, Andreas Abel wrote:
>> On 29.11.2013 20:40, Jason Gross wrote:
>>> Is there a computable/decidable/syntactic (and also complete)
>>> characterization of what's provable with J but not K?  (Alternatively,
>>> is there an algorithm for transforming proofs using K into proofs using
>>> only J whenever they exist?)
>> 
>> Not that I know of.  [Maybe there is one in one of the drawers of
>> Conor's desk...]  I guess this is what Jesper Cockx and Pierre
>> Boutillier are working on.
> 
> I would like to know if Conor's translation of pattern matching, which
> relies on K, could be modified so that it supports fewer patterns but
> doesn't require K.

Of course it could.

Rather than using the '99 translation, based on JMeq, we could use the
'98 translation, which explicitly used substitution by earlier equations
to keep later equations homogeneous.

The general method gives you patterns of equations like

  (q1 : Eq T1 a1 b1) ->
  (q2 : Eq (T2 b1) (subst1 q1 T2 a2) b2) ->
  (q3 : Eq (T3 b1 b2) (subst2 q1 q2 T3 a3) b3) ->
  ...

which can be simplified by unification: when constructors clash, you
win; when (injective) constructors coincide, one equation splits into
several; when a variable meets a term which does not depend on it,
use J to substitute, and all the substs simplify. (substn is J
iterated n times). The trouble bites when a1 and b1 coincide. In general,
q1 is used in later substs, so you need to use dependent elimination on
it, which means using K to deal with apparently trivial unification
problems. Of course, in HoTT world, they really aren't trivial
unification problems.

So what you can do is a finer dependency analysis, minimizing the
extent to which the formation of later equations depends on the proofs
of earlier equations. Any such analysis is likely to be quite syntactic
and miss some subtle forms of non-dependency. But at least it's easy to
be sure that you're K-less.

A more general question we might ask is "what are the unification problems
we can solve in the absence of K and the presence of higher inductive
types?" It is already clear that the notion of "most general unifer"
needs a proof relevant refinement.

All the best

Conor