[Agda] another possible without-K problem

Wed Jul 10 17:45:22 CEST 2013

On 10.07.2013 17:28, drl at cs.cmu.edu wrote:
> If you make S1 and base abstract, then the example is not accepted.
>
> However, the current implementation of HITs uses private, not abstract,
> and in this case the example is accepted (private is what gives you the
> definitional behavior).  Unless you use the unit->unit
> trick, so that base is no longer a constructor applied to variables.
>
> What would happen if without-K restricted matching to only distinct
> variables, not constructors applied to variables?  This would seem to
> rule out the examples below, including disjointness.
>
> However, what I'd really like is:
>
> - parameters can be anything

The question is what counts as a parameter.  In the current darcs 
--without-K, anything that shares variables with an index in a 
constructor target type is not a parameter.  In particular, in

   data _==_ {A : Set}(a : A) : A -> Set where
     refl : a == a

the (a : A) is not a parameter.  But then, after we thus ruled out 
information flow from parameters to indices, parameters can be anything.

> - indices must be distinct variables

So this means they cannot be constructors applied to distinct variables?

> - unless the index type is an hset, in which case indices can be
>    anything

Do you have a syntactic analysis for hset we could build into Agda?

> Assuming the identity type is defined in the Paulin-Mohring style, this
> would allow Paulin-Mohring pattern matching (e.g. you can split on
> M == x for any term M), and let you mix in the usual with-K
> Agda programming.
>
> I remember an issue with parameters from the bug you noticed a while
> ago.  Would my proposal above run afoul of that?

In the new analysis, the two definitions of equality are treated the same.

Cheers,
Andreas

> On Jul10, 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?

-- 
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/