[Agda] without-K problem
Nils Anders Danielsson
nad at chalmers.se
Fri Jun 22 00:43:09 CEST 2012
On 2012-06-20 14:00, Andreas Abel wrote:
> On 20.06.2012 12:32, Altenkirch Thorsten wrote:
>> On 20/06/2012 08:39, "Andreas Abel"<andreas.abel at ifi.lmu.de> wrote:
>>> On 18.06.12 9:18 PM, Guillaume Brunerie wrote:
>>>> For what it’s worth, I cannot reproduce the bug using the following
>>>> definition of the identity types:
>>>>
>>>> data _≡_ {A : Set} : A → A → Set where
>>>> refl : {x : A} → x ≡ x
>>>>
>>>> But I can reproduce it using the following definition (which is the one
>>>> used in the standard library):
>>>>
>>>> data _≡_ {A : Set} (x : A) : A → Set where
>>>> refl : x ≡ x
>>>
>>> Yes, it seems --without-K should also forbid data definitions where a
>>> parameter variable ("x") is free in a index position.
>>>
>>> Otherwise, index variables can be "hidden" in parameter positions and
>>> are not spotted by --without-K when it checks whether a split is legal.
Yes, the problem is that constructors are not applied to their
parameters. We can fix the problem in several ways:
* Don't allow any constructors: force the indices to be distinct
variables that are not free in the parameters. I tried this once, and
found it rather crippling.
* Only allow constructors from parameter-free data types (natural
numbers but not lists). This is easy to implement, but also quite
annoying.
* Reconstruct the parameters when applying the check. This sounds like
the way to go. Is there some kind of parameter-reconstructing function
somewhere in the code base?
> (That Nisse uses Guillaumes version of equality of course hints that he
> finds the std-lib definition is problematic...)
I don't.
--
/NAD
More information about the Agda
mailing list