[Agda] another possible without-K problem
Dan Licata
drl at cs.cmu.edu
Wed Jul 10 21:38:28 CEST 2013
On Jul10, Dan Doel wrote:
> (If I'm not mistaken) way back in Eliminating Dependent Pattern Matching
> (at least), it is remarked that the translation relies on both K (or, an
> appropriate heterogeneous equality) and disjointness and injectivity of
> constructors. So it would not be a surprise that removing K does not remove
> disjointness of constructors.
At least for simple types like the natural numbers and booleans, I am
pretty sure that injectivity and disjointness can be proved from J and
large elims. So I agree that, in a theory with J + large elims but
without K, one can prove disjointness and injectivity. The question is
whether we want this to be part of pattern matching on identity types in
general, though.
> Getting rid of this is a big deal, though. If you just throw it away, then
> I don't think definitions like the following work:
>
> zip : {A B : Set} {n : ℕ} -> Vec A n -> Vec B n -> Vec (A × B) n
> zip [] [] = []
> zip (x :: xs) (y :: ys) = (x , y) :: zip xs ys
>
> The ability to elide the two other cases relies on the fact that they cause
> unification errors, zero ≠ suc n. But, this presumes disjointness of the
> natural numbers. If we aren't allowed that, then we must write these cases,
> and explicitly appeal to disjointness proofs. Except, Agda (for instance)
> isn't equipped for such a thing; we have no way of accessing a
> propositional 'zero = suc n' in those cases to hand off to a lemma.
>
> Also, you presumably lose the ability to write things like:
>
> foo : ∀ n -> Fin n -> ...
> foo zero () ...
> ...
>
> and similarly have no real recourse for that case in Agda.
I think these examples are OK under my stipulation that
dependent pattern matching works as-is for hset indices.
Nats are an hset, so code with Fin/Vec would be the same as it is in
Agda currently. Does that seem right? There totally could be holes in
it. This was more a stray thought than a well-thought-out proposal.
-Dan
More information about the Agda
mailing list