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

[vlad]

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