[Agda] slightly wrong sized datatype definition leads to proof of False

[Frédéric Blanqui]

Hi.

Where can I find the definitions of Size and Size<? 
https://github.com/agda/agda-stdlib/blob/master/src/Size.agda imports 
Agda.Builtin.Size but I don't know where to find this module. (Sorry, I 
am not familiar with Agda.)

A comment in this page says that: SizeUniv is a sort, Size:SizeUniv and 
Size<:Size->SizeUniv. Is SizeUniv typable, and what is the type of 
Size->SizeUniv? In other words, what are the PTS axioms and rules for 
the sort SizeUniv?

However, 
https://agda.readthedocs.io/en/v2.6.1.1/language/built-ins.html#sized-types 
says that SizeUniv:SizeUniv, which doesn't seem like a good idea in a 
type system, and Size<:..Size->SizeUniv. I don't know what is ..Size.

Thanks for your help.

Frédéric.

Le 20/10/2020 à 11:09, vlad a écrit :
> Thanks again for the answer. All this is very informative. It does IMO 
> deserve to be properly documented, in papers and in the tool, since it 
> contradicts the usual discourse that  inductive types should be 
> defined using data, coinductive types should be defined using records, 
> and sizes are just a way to ensure termination/productivity. Hopefully 
> all this will be clarified (and the corresponding soundness bugs will 
> be fixed) in a future release. When this happens I'll be happy to use 
> Agda again.
>
> On 20/10/2020 10:37, Andrea Vezzosi wrote:
>> Using sizes as freely as Agda allows, the distinction between data and
>> codata gets quite blurred, but that does not necessarily lead to an
>> unsound system.
>>
>> The fact that _<_ is not well-founded on sizes is what is unsound, and
>> I argue also agda refuting cycles in your  ℕ {∞}.
>>
>> Regarding Acc,  It's true that for any specific size "Acc s"
>> corresponds to "s" being accessible. But then  well-foundedness of _<_
>> implies `Acc s` is equivalent to the unit type for any `s`, so any two
>> elements you define in it are going to be equal.
>>
>> Regarding how your `ℕ` can be the (sized) conatural numbers, my point
>> is that for the functor F
>>
>>   F : (Size -> Set) -> Size -> Set
>>   F X i = Maybe ((j : Size< i) -> X j)
>>
>> the least and greatest fixed points coincide, so whether you construct
>> it with "data" or a coinductive record it does not make a difference.
>> You'll get a `ℕ : Size -> Set` which can be shown to be antitone in
>> the size.
>>
>> I would agree that it's a bit of an obscure interaction though, and
>> might deserve a warning.
>>
>> On Mon, Oct 19, 2020 at 6:22 PM vlad <Vlad.Rusu at inria.fr> wrote:
>>> Thank you for the reply. Hmm, there are some things I don't understand.
>>>
>>> On 19/10/2020 17:05, Andrea Vezzosi wrote:
>>>> The issue here is only incidentally about sized types. but rather an
>>>> issue with the check for when an absurd pattern (i.e. "()") is
>>>> allowed:
>>>>
>>>> https://github.com/agda/agda/issues/4995
>>> Unlike that issue I do not use a postulate but I am using sized types,
>>> so how can my issue only incidentally be about sized types?
>>>> Btw, the type you defined is more like co-natural numbers, i.e. with
>>>> an extra point at infinity, so it's quite natural to have a fix-point
>>>> for `suc`.
>>> Ok, perhaps the notation is confusing. If I syntactically rewrite the
>>> definition
>>>
>>> data  ℕ {s : Size} :  Set where
>>>     zero :  ℕ
>>>     suc : ({s' : Size< s} → ℕ {s'}) → ℕ {s}
>>>
>>> as follows, with Acc instead of ℕ, acc instead of suc, with explicit
>>> instead of implicit sizes, and forgetting the zero constructor, which
>>> was there just to make the above look like a definition of natural
>>> numbers anyway:
>>>
>>> data Acc (s : Size) : Set where
>>>
>>>       acc : ((s' : Size< s)  → Acc s') → Acc s
>>>
>>> then Acc reads as the accessibility predicate for the relation _<_  on
>>> Size such that i < j iff i : Size< j. The issue I raised can of course
>>> be rephrased by proving that the accessible part of the relation _<_
>>> coincides with the whole relation, in particular, Acc ∞, and since _<_
>>> is not well-founded (∞<∞) one gets a proof of False. Or one can use ℕ
>>> instead of Acc for that purpose, they're interchangeable here.
>>>
>>> Now, Acc is an inductive definition, and so is ℕ. I don't see how the
>>> latter can denote co-natural numbers, which AFAIK require a coinductive
>>> definition?
>>>
>>> Mind, I'm not saying that ℕ above is the appropriate way of defining
>>> sized natural numbers. But Agda accepts it - and it shouldn't, because
>>> after a few steps one gets a proof of False in safe mode...
>>>
>>>
>>>> On Mon, Oct 19, 2020 at 1:44 PM vlad <Vlad.Rusu at inria.fr> wrote:
>>>>> Thanks for finding this. I guess this is in a longer tradition of
>>>>> problems with the sized types implementation, see e.g.
>>>>> https://github.com/agda/agda/issues/2820,
>>>>> https://github.com/agda/agda/issues/3026,
>>>>> https://github.com/agda/agda/issues/1428.
>>>>>
>>>>> I don't understand whether it has overlap with existing issues. You
>>>>> don't use the infinity size, nor equality. So maybe it's a new 
>>>>> kind of
>>>>> issue, coming from interaction of sizes with inductive types?
>>>>>
>>>>> It is an elaboration on the bug about well-founded induction and 
>>>>> sized types (https://github.com/agda/agda/issues/3026). The main 
>>>>> difference with the latter is that, instead of importing the 
>>>>> well-founded module of Agda's library, I am using an apparently 
>>>>> innocent definition of a sized inductive type :
>>>>>
>>>>> data ℕ  {s : Size} :  Set where
>>>>>     zero :  ℕ
>>>>>     suc : ({s' : Size< s} → ℕ {s'}) → ℕ {s}
>>>>>
>>>>> as an accessibility predicate for the relation between sized 
>>>>> induced by the construction Size<. By using the "size-elimproved" 
>>>>> construction (also an elaboration of code found here: 
>>>>> https://github.com/agda/agda/issues/2820#issuecomment-339969286) I 
>>>>> can then define a "natural number" for each size, including 
>>>>> infinity (note that sizes are implicit arguments, so infinity does 
>>>>> not show up in the code, but it's there all right). For size = 
>>>>> infinity, the "natural number"
>>>>>
>>>>> foo : ℕ
>>>>> foo = size-elimproved (λ s → ℕ{s}) (λ _ H → suc λ { {j} → H j } ) _
>>>>>
>>>>> is easily shown to be a successor of itself, which the definition 
>>>>> of "natural numbers" forbids, hence the proof of False.
>>>>>
>>>>> Overall, I'm not sure it's worth a new bug report, as it is an 
>>>>> elaboration of existing constructions. My main point in showing 
>>>>> this is that one may easily "believe" that one is defining natural 
>>>>> numbers with sizes e.g. for writing non-structural recursive 
>>>>> functions over them (like integer division), while in effect 
>>>>> writing something else, with unpleasant consequences.
>>>>>
>>>>> _______________________________________________
>>>>> 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
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20201020/e8157318/attachment.html>