[Agda] another possible without-K problem

Wed Jul 10 17:52:30 CEST 2013

Ah, so how do you prove then that p and q are the same equality proof, 
with only J?

On 10.07.2013 17:01, Altenkirch Thorsten wrote:
>
>
> On 10/07/2013 15:52, "Dan Licata" <drl at cs.cmu.edu> wrote:
>
>> Is this a bug or a design decision?  It seems like this example is in
>> accord with the description of without-K in the release notes, but
>> that allowing matching when the indices are constructors has some
>> interesting consequences.
>
> You are right since in the example S1 is just an inductive type this isn't
> really a problem.
>
> Is this still possible if one "hides" the fact that S1 is inductively
> defined?
> I guess this is more the problem that the current implementation of HITs
> is a bit of a hack.
>
> Disjointness was always built into pattern matching and it is hard to see
> how to avoid this.
> One only needs a microscopic universe, Bool with T : Bool -> Type to
> justify this.
>
> Thorsten
>
>> In particular, it means that, in a core
>> theory without universes, without-K pattern matching cannot be
>> compiled to J, because you can prove disjointness (and injectivity) of
>> constructors, and that bool is an hset (code below), just using
>> pattern matching on the identity type.  As far as I know, disjointness
>> and the hset-ness of bool require a universe/large elims to prove.  Of
>> course, Agda has universes, and it is possible that without-K pattern
>> matching could be compiled to J + uses of large elims to code up these
>> constructions on constructors.  But I would personally prefer it if
>> without-K pattern matching did not build these things in, because it
>> means we need to use two hacks (rather than just one :) ) to implement
>> higher inductives.
>>
>> -Dan
>>
>> -- checks in Agda 2.3.2.1
>> {-# OPTIONS --without-K #-}
>>
>> module WithoutK where
>>
>>   data Nat : Set where
>>     Z : Nat
>>     S : Nat -> Nat
>>
>>   data Bool : Set where
>>     True : Bool
>>     False : Bool
>>
>>   data Void : Set where
>>
>>   data _==_ {A : Set} (x : A) : A -> Set where
>>     Refl : x == x
>>
>>   injective : {m n : Nat} -> S m == S n -> m == n
>>   injective Refl = Refl
>>
>>   disjoint : {m : Nat} -> S m == Z -> Void
>>   disjoint ()
>>
>>   bool-hset : (b : Bool) -> (p : b == b) -> p == Refl
>>   bool-hset True Refl = Refl
>>   bool-hset False Refl = Refl
>>
>>
>>
>> On Wed, Jul 10, 2013 at 5:56 AM, Altenkirch Thorsten
>> <psztxa at exmail.nottingham.ac.uk> wrote:
>>> This looks like a bug – please add it to the bug tracker.
>>>
>>> We really need to understand what we are doing when checking wether
>>> pattern
>>> satisfy the —without-K condition. It seems that Conor's work on
>>> translating
>>> pattern matching to eliminators (with J and K) would be a good starting
>>> point.
>>>
>>> At the same time we know that many types support UIP by structure.
>>> Michael
>>> Hedberg showed that all types with a decidable equality support UIP and
>>> it
>>> is not hard to see that this can be extended to stable equality (non-not
>>> closed). (Little puzzle: without extensionality – are there any types
>>> which
>>> have stable but not decidable equality ?)
>>>
>>> We also want to quantify over all HSets (I.e. types with UIP) and so on.
>>>
>>> Thorsten
>>>
>>> From: Jason Reed <jcreed at gmail.com>
>>> Date: Tue, 9 Jul 2013 16:31:22 +0100
>>> To: "agda at lists.chalmers.se" <agda at lists.chalmers.se>
>>> Subject: [Agda] another possible without-K problem
>>>
>>> I'm experiencing something that I think is a violation of the intent of
>>> the
>>> --without-K flag, similar to what Thorsten was talking about in
>>> https://lists.chalmers.se/pipermail/agda/2012/004104.html.
>>>
>>> The following file checks fine for me under current darcs Agda:
>>>
>>> <<<begin>>>
>>> {-# OPTIONS --without-K #-}
>>>
>>> module Test where
>>>
>>> data S1 : Set where
>>>      base : S1
>>>
>>> module test where
>>>     data _≡_ {A : Set} (a : A) : A → Set where
>>>      refl : a ≡ a
>>>
>>>     bad : (p q : base ≡ base) -> p ≡ q
>>>     bad refl refl = refl
>>>
>>> module test2 where
>>>     data _≡_ {A : Set} : A → A → Set where
>>>         refl : {x : A} → x ≡ x
>>>
>>>     bad : (p q : base ≡ base) -> p ≡ q
>>>     bad refl refl = refl
>>> <<<end>>>
>>>
>>> Note that this covers both the possible definitions of the identity type
>>> mentioned by Guillaume in
>>> https://lists.chalmers.se/pipermail/agda/2012/004105.html
>>>
>>> Any ideas what should be done here? Does the K-check need to be further
>>> strengthened when there aren't parameters around? Am I misunderstanding
>>> something trivial?
>>>
>>>
>>> This message and any attachment are intended solely for the addressee
>>> and
>>> may contain confidential information. If you have received this message
>>> in
>>> error, please send it back to me, and immediately delete it.   Please
>>> do not
>>> use, copy or disclose the information contained in this message or in
>>> any
>>> attachment.  Any views or opinions expressed by the author of this
>>> email do
>>> not necessarily reflect the views of the University of Nottingham.
>>>
>>> This message has been checked for viruses but the contents of an
>>> attachment
>>> may still contain software viruses which could damage your computer
>>> system,
>>> you are advised to perform your own checks. Email communications with
>>> the
>>> University of Nottingham may be monitored as permitted by UK
>>> legislation.
>>>
>>>
>>>
>>> _______________________________________________
>>> Agda mailing list
>>> Agda at lists.chalmers.se
>>> https://lists.chalmers.se/mailman/listinfo/agda
>>>
>
>
>
> _______________________________________________
> 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/