[Agda] Re: Yet another way Agda --without-K is incompatible with univalence

Matteo Acerbi matteo.acerbi at gmail.com
Fri Jan 17 17:11:51 CET 2014


To be even more clear: I really like that many Agda developers are
working on fixing --without-K.

I simply asked a question about a related possible option in the same thread.

I apologise if that confused anyone.

Cheers,
Matteo

PS. I still do not understand why by using a parameterised module the
file is not accepted, as that is the way I most often assume
"postulates" and I thought the outcome would be the same. However, I
admit I do *not* understand the details of the problem.

On Fri, Jan 17, 2014 at 3:51 PM, Matteo Acerbi <matteo.acerbi at gmail.com> wrote:
> I am aware that in Agda eliminators can only be defined by pattern
> matching (or assumed).
>
> If I am not wrong, only LEGO and Epigram had built-in eliminators for
> every type.
>
> As I wrote in the other message, I would still like to disallow myself
> to use pattern matching in the current file, but be free to use any
> definition from imported files.
>
> Those definitions might include "eliminators", to be more clear.
>
> Would anyone find this useful as well?
>
> Cheers,
> Matteo
>
> 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
>>> >
>>
>>


More information about the Agda mailing list