[Agda] Re: Yet another way Agda --without-K is incompatible with
univalence
Jesper Cockx
Jesper at sikanda.be
Fri Jan 17 16:42:51 CET 2014
A little more analysis from my part. The injectivity rule in the EDPM paper
has the following form (somewhat simplified):
m : s ≃ t -> P ⊢ injectivity m : c s ≃ c t -> P
where ≃ is Conor's heterogeneous equality. As we all know, the elimination
rule for heterogeneous equality is equivalent with K, so we should use the
homogeneous equality instead:
m : s ≡ t -> P ⊢ injectivity m : c s ≡ c t -> P
Unfortunately, this turns out to be insufficient for pattern matching. What
we need instead is a version of injectivity where P is dependent on the
proof of c s ≡ c t:
m : (e : s ≡ t) -> P (cong c e) ⊢ injectivity m : (e : c s ≡ c t) -> P e
This works fine as long as the type of c is just a simple data type. When
we consider indexed data types, we can no longer be sure that the equation
c s ≡ c t is homogeneous. So an additional equation on the indices is
introduced, and P is made dependent on it as well. So suppose for
simplicity "D : U -> Set" is a data type with a single constructor "c : (x
: A) -> D (u x)" and define "us := u s" and "ut := u t". We need this
auxiliary function:
conf : (e : s ≡ t) → subst D (cong u e) (c s) ≡ c t
conf e = J (λ t e → subst D (cong u e) (c s) ≡ c t) e refl
Then we get the correct version of injectivity:
m : (e : s ≡ t) -> P (cong u e) (conf e) ⊢ injectivity m : (eu : us ≡ ut)
(e : subst D eu (c s) ≡ c t) -> P eu e
This rule can be defined using only the standard eliminators for D and ≡,
without K (ask me if you want to see the construction, I have it but it's
quite long).
However, this is not the form of injectivity that is used in the pattern
matching algorithm. Rather, it needs a version of injectivity where us and
ut are *definitionally* equal. Ok, you say, in that case we can just fill
in refl to get this:
m : (e : s ≡ t) -> P (cong u e) (conf e) ⊢ injectivity m : (e : c s ≡ c t)
-> P refl e
The problem arises when we want to apply this rule to construct a function
"? : (e : c s ≡ c t) -> P' e". Now in order to apply this rule, we need to
find P such that P refl e = P' e (definitionally). In other words, to
construct P we need to eliminate the first argument "eu : u ≡ u", which is
generally speaking not possible without K.
In my example, I exploit this behaviour by choosing "P' : foo ≡ foo -> Set"
to be defined by "P' e = e ≡ refl". You can see that we cannot construct a
"P : (e : refl ≡ refl) -> subst Foo e foo ≡ foo -> Set" such that "P refl e
≡ P' refl" without using K. So we should not be able to apply injectivity
in this situation, yet that is exactly what Agda is doing.
Best,
Jesper
On Fri, Jan 17, 2014 at 3:34 PM, Jesper Cockx <Jesper at sikanda.be> wrote:
> Andreas: my own version of --without-K has the same problem. However, I'm
> trying to fix it by doing something like parameter reconstruction for the
> indices: when applying the injectivity rule to the problem "foo ≡ foo", we
> should first solve the equation "refl ≡ refl" on the indices (here, both
> refl's have type "myPoint ≡ myPoint"). But this equation is already
> rejected by the current --without-K, thus excluding the problematic pattern
> matching on "foo ≡ foo". I'm still testing whether this doesn't introduce
> any other problems or excludes any good examples.
>
> Matteo: the problem with allowing no pattern matching at all is that in
> Agda, we depend on pattern matching to define eliminators for data types.
> Another possibility would be to introduce an even more restrictive version
> of --without-K that requires all indices (and parameters too possibly?) to
> be *distinct* variables (so no constructors allowed). This would at least
> allow us to define the eliminator for each data type, but hopefully be
> simple enough to avoid any problems like this one.
>
> Mattieu: The equation that's being eliminated is "foo ≡ foo", which is
> indeed the same as "refl ≡ refl" under the equivalence Foo-equiv. However
> unlike refl, the constructor foo has no parameters and no arguments, so a
> naive interpretation of injectivity would tell you that the only term of
> type "foo ≡ foo" is refl. However, this is ignoring the index of the type
> Foo. So in fact, we first need to solve the equation "refl ≡ refl" on the
> indices, which is impossible without K.
>
> Best,
> Jesper
>
>
> On Fri, Jan 17, 2014 at 3:02 PM, Matteo Acerbi <matteo.acerbi at gmail.com>wrote:
>
>> Hello,
>>
>> I noticed that if the two postulates are replaced by
>>
>> module _ (mySpace : Set)(myPoint : mySpace) where
>>
>> (indent the rest)
>>
>> the problem seems to not appear (an error is reported).
>>
>> Maybe this gives some hints (I do not know).
>>
>> That said, I have a small proposal.
>>
>> Most of the times I use Agda for its *wonderful* dependent pattern
>> matching facility, but every now and then I would like to forbid
>> myself to use pattern matching at all, at least from inside a single
>> file.
>>
>> I would like to have the possibility to get back to that file and make
>> sure that I never used pattern matching in that code just by looking
>> at the OPTIONS header.
>>
>> I think I would find a --no-pattern-matching option, which simply
>> applied this restriction, but still allowed for importing modules
>> whatever their options are, very convenient.
>>
>> For now I am just curious as to whether others are interested: would
>> anyone else like such a --no-pattern-matching option?
>>
>> Cheers,
>> Matteo
>>
>> On Fri, Jan 17, 2014 at 2:43 PM, Jesper Cockx <Jesper at sikanda.be> wrote:
>> > I'm not relieved. The problem is still there.
>> >
>> >
>> > On Fri, Jan 17, 2014 at 2:38 PM, Andreas Abel <andreas.abel at ifi.lmu.de>
>> > wrote:
>> >>
>> >> Can you explain, please?
>> >>
>> >> You say you did not expect to be able to prove 'problem' from
>> >> 'equiv-to-id' which you thought was univalence. Martin tells you that
>> >> 'equiv-to-id' is a consequence of univalence. Now you are relieved.
>> But
>> >> still 'problem' follows from univalence. Why are you relieved now?
>> >>
>> >> Sorry, I am a bit confused now...
>> >> Andreas
>> >>
>> >>
>> >> On 17.01.2014 13:39, Jesper Cockx wrote:
>> >>>
>> >>> As Martin pointed out to me, my definition of equiv-to-id is not the
>> >>> univalence axiom, but merely a (much weaker) consequence of it. Thank
>> >>> you.
>> >>>
>> >>> Best,
>> >>> Jesper
>> >>>
>> >>>
>> >>> On Fri, Jan 17, 2014 at 12:19 PM, Jesper Cockx <Jesper at sikanda.be
>> >>> <mailto:Jesper at sikanda.be>> wrote:
>> >>>
>> >>> Dear all,
>> >>>
>> >>> Much to my own surprise, I encountered another problem with the
>> >>> --without-K option. This is on the latest darcs version of Agda
>> and
>> >>> is unrelated to the termination checker. As far as I understand,
>> the
>> >>> unification algorithm is applying the injectivity rule too
>> liberally
>> >>> for data types indexed over indexed data. But maybe someone else
>> can
>> >>> give a better explanation?
>> >>>
>> >>> === BEGIN CODE ===
>> >>>
>> >>> {-# OPTIONS --without-K #-}
>> >>>
>> >>> module YetAnotherWithoutKProblem where
>> >>>
>> >>> -- First, some preliminaries to make this file self-contained.
>> >>> data _≡_ {a} {A : Set a} (x : A) : A → Set where
>> >>> refl : x ≡ x
>> >>>
>> >>> subst : ∀ {a b} {A : Set a} {x : A} (B : (y : A) → Set b) →
>> >>> {y : A} → x ≡ y → B x → B y
>> >>> subst B refl b = b
>> >>>
>> >>> record _≃_ (A B : Set) : Set where
>> >>> constructor equiv
>> >>> field
>> >>> f : A → B
>> >>> g : B → A
>> >>> i : (x : A) → g (f x) ≡ x
>> >>> j : (y : B) → f (g y) ≡ y
>> >>>
>> >>> -- The univalence axiom.
>> >>> postulate equiv-to-id : {A B : Set} → A ≃ B → A ≡ B
>> >>>
>> >>> -- Now consider any concrete space 'mySpace' with a point
>> 'myPoint'.
>> >>> -- We will show that mySpace has no structure above dimension 2.
>> >>> postulate mySpace : Set
>> >>> postulate myPoint : mySpace
>> >>>
>> >>> -- We define Foo in a way such that 'Foo e' is equivalent with
>> 'refl
>> >>> ≡ e'.
>> >>> data Foo : myPoint ≡ myPoint → Set where
>> >>> foo : Foo refl
>> >>>
>> >>> Foo-equiv : {e : myPoint ≡ myPoint} → Foo e ≃ (refl ≡ e)
>> >>> Foo-equiv = equiv f g i j
>> >>> where
>> >>> f : {e : myPoint ≡ myPoint} → Foo e → refl ≡ e
>> >>> f foo = refl
>> >>>
>> >>> g : {e : myPoint ≡ myPoint} → refl ≡ e → Foo e
>> >>> g refl = foo
>> >>>
>> >>> i : {e : myPoint ≡ myPoint} (m : Foo e) → g (f m) ≡ m
>> >>> i foo = refl
>> >>>
>> >>> j : {e : myPoint ≡ myPoint} (i : refl ≡ e) → f (g i) ≡ i
>> >>> j refl = refl
>> >>>
>> >>> -- Here comes the real problem: by injectivity, 'Foo e' is a set
>> ...
>> >>> test : {e : myPoint ≡ myPoint} → (a : Foo e) → (i : a ≡ a) → i ≡
>> refl
>> >>> test foo refl = refl
>> >>>
>> >>> -- ... hence by univalence, so is 'refl ≡ e'.
>> >>> problem : {e : myPoint ≡ myPoint} → (a : refl ≡ e) → (i : a ≡ a)
>> → i
>> >>> ≡ refl
>> >>> problem = subst (λ X → (x : X) → (i : x ≡ x) → i ≡ refl)
>> >>> (equiv-to-id Foo-equiv)
>> >>> test
>> >>>
>> >>> === END CODE ===
>> >>>
>> >>> All the best,
>> >>> Jesper
>> >>>
>> >>>
>> >>>
>> >>>
>> >>> _______________________________________________
>> >>> Agda mailing list
>> >>> Agda at lists.chalmers.se
>> >>> https://lists.chalmers.se/mailman/listinfo/agda
>> >>>
>> >>
>> >>
>> >> --
>> >> Andreas Abel <>< Du bist der geliebte Mensch.
>> >>
>> >> Theoretical Computer Science, University of Munich
>> >> Oettingenstr. 67, D-80538 Munich, GERMANY
>> >>
>> >> andreas.abel at ifi.lmu.de
>> >> http://www2.tcs.ifi.lmu.de/~abel/
>> >
>> >
>> >
>> > _______________________________________________
>> > Agda mailing list
>> > Agda at lists.chalmers.se
>> > https://lists.chalmers.se/mailman/listinfo/agda
>> >
>>
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20140117/4e08cae4/attachment-0001.html
More information about the Agda
mailing list