[Agda] no longer type checks
Martin Escardo
m.escardo at cs.bham.ac.uk
Fri Dec 14 20:00:50 CET 2012
Thanks, Andreas. This is a helpful explanation.
I think that maybe it is an open research question what kind of pattern
matching corresponds to (intensional) MLTT (without the K axiom). That
should be interesting to know for sure. But I am glad that there is some
preliminary experimental work in Agda going on.
Best,
Martin
On 14/12/12 10:42, Andreas Abel wrote:
> For background on the new implementation of --without-K, see the thread
>
> without-K problem
>
> on this list. Thorsten had observed that with Agda 2.3.0, a weak
> version of K was provable for the identity type given by
>
> data Id1 (X : Set)(x : X) : X -> Set where
> refl : Id1 X x x
>
> Guillaume Brunerie observed that this is not possible for the version
>
> data Id2 (X : Set) : X -> X -> Set where
> refl : (x : X) -> Id2 X x x
>
> The difference between Id1 and Id2 is that for Id2, there is only one
> index (x) and two parameters (X,x), but Id2 has one parameter (X) and
> two indices (x,x). The old --without-K check was that during matching,
> the indices should not have common free variables, because by the
> non-linearity one could get K. For Id1, the non-linear nature of
> indices is hidden by the fact that only the second argument of type X is
> declared as an index. For Id2, the non-linearity is obvious.
>
> Nisse's rectification of the situation was to treat *all* parameters as
> indices, to reveal hidden non-linearity situations. I think he went one
> step to far, as your example shows. Your lemma gets rejected because it
> uses two constructors of the disjoint sum type which naturally share the
> type parameters of the disjoint sum type.
>
> I think in the calculation of the "critical variables", i.e., those that
> need to be all distinct, only those parameters of a constructor should
> be taken into account that have common variables with one of the
> indices. To state that in the mentioned examples,
>
> - for the disjoint sum type, no parameter should be counted as index
>
> - for the type Id1, only x, but not X should be counted as index
>
> Might be worth to add this to the bug tracker...
>
> Cheers,
> Andreas
>
>
> On 13.12.12 10:16 PM, Martin Escardo wrote:
>> This
>>
>> lemma : in₀ x ≡ in₁ y → ⊥
>> lemma ()
>>
>> used to compile, where "in" are the injections into X + Y.
>>
>> Now I get, in 2.3.2,
>>
>> "The variables
>> .X₁
>> .Y₁
>> x₁
>> .X₁
>> .Y₁
>> y₁
>> in the indices
>> in₀ x₁
>> in₁ y₁
>> are not distinct (note that parameters count as constructor
>> arguments)
>> when checking that the clause lemma () has type in₀ x ≡ in₁ y → ⊥"
>>
>> Is that intended behaviour?
>>
>> What would be the easiest solution to make this lemma work?
>>
>> Thanks,
>> Martin
>>
>
--
Martin Escardo
http://www.cs.bham.ac.uk/~mhe
More information about the Agda
mailing list