[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