<html>
<head>
<meta http-equiv="Content-Type" content="text/html; charset=UTF-8">
</head>
<body>
<p>Hi.</p>
<p>Where can I find the definitions of Size and Size<?
<a class="moz-txt-link-freetext" href="https://github.com/agda/agda-stdlib/blob/master/src/Size.agda">https://github.com/agda/agda-stdlib/blob/master/src/Size.agda</a>
imports <span class="pl-k"></span><span class="pl-en">Agda.Builtin.Size
but I don't know where to find this module. (Sorry, I am not
familiar with Agda.)</span></p>
<p><span class="pl-en">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?<br>
</span></p>
<p><span class="pl-en">However,
<a class="moz-txt-link-freetext" href="https://agda.readthedocs.io/en/v2.6.1.1/language/built-ins.html#sized-types">https://agda.readthedocs.io/en/v2.6.1.1/language/built-ins.html#sized-types</a>
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.</span></p>
<p><span class="pl-en">Thanks for your help.</span></p>
<p><span class="pl-en">Frédéric.</span></p>
<div class="moz-cite-prefix">Le 20/10/2020 à 11:09, vlad a écrit :<br>
</div>
<blockquote type="cite"
cite="mid:0aea0a29-2721-ee22-e76d-e13a8406598a@inria.fr">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.
<br>
<br>
On 20/10/2020 10:37, Andrea Vezzosi wrote:
<br>
<blockquote type="cite">Using sizes as freely as Agda allows, the
distinction between data and
<br>
codata gets quite blurred, but that does not necessarily lead to
an
<br>
unsound system.
<br>
<br>
The fact that _<_ is not well-founded on sizes is what is
unsound, and
<br>
I argue also agda refuting cycles in your ℕ {∞}.
<br>
<br>
Regarding Acc, It's true that for any specific size "Acc s"
<br>
corresponds to "s" being accessible. But then well-foundedness
of _<_
<br>
implies `Acc s` is equivalent to the unit type for any `s`, so
any two
<br>
elements you define in it are going to be equal.
<br>
<br>
Regarding how your `ℕ` can be the (sized) conatural numbers, my
point
<br>
is that for the functor F
<br>
<br>
F : (Size -> Set) -> Size -> Set
<br>
F X i = Maybe ((j : Size< i) -> X j)
<br>
<br>
the least and greatest fixed points coincide, so whether you
construct
<br>
it with "data" or a coinductive record it does not make a
difference.
<br>
You'll get a `ℕ : Size -> Set` which can be shown to be
antitone in
<br>
the size.
<br>
<br>
I would agree that it's a bit of an obscure interaction though,
and
<br>
might deserve a warning.
<br>
<br>
On Mon, Oct 19, 2020 at 6:22 PM vlad <a class="moz-txt-link-rfc2396E" href="mailto:Vlad.Rusu@inria.fr"><Vlad.Rusu@inria.fr></a>
wrote:
<br>
<blockquote type="cite">Thank you for the reply. Hmm, there are
some things I don't understand.
<br>
<br>
On 19/10/2020 17:05, Andrea Vezzosi wrote:
<br>
<blockquote type="cite">The issue here is only incidentally
about sized types. but rather an
<br>
issue with the check for when an absurd pattern (i.e. "()")
is
<br>
allowed:
<br>
<br>
<a class="moz-txt-link-freetext" href="https://github.com/agda/agda/issues/4995">https://github.com/agda/agda/issues/4995</a>
<br>
</blockquote>
Unlike that issue I do not use a postulate but I am using
sized types,
<br>
so how can my issue only incidentally be about sized types?
<br>
<blockquote type="cite">Btw, the type you defined is more like
co-natural numbers, i.e. with
<br>
an extra point at infinity, so it's quite natural to have a
fix-point
<br>
for `suc`.
<br>
</blockquote>
Ok, perhaps the notation is confusing. If I syntactically
rewrite the
<br>
definition
<br>
<br>
data ℕ {s : Size} : Set where
<br>
zero : ℕ
<br>
suc : ({s' : Size< s} → ℕ {s'}) → ℕ {s}
<br>
<br>
as follows, with Acc instead of ℕ, acc instead of suc, with
explicit
<br>
instead of implicit sizes, and forgetting the zero
constructor, which
<br>
was there just to make the above look like a definition of
natural
<br>
numbers anyway:
<br>
<br>
data Acc (s : Size) : Set where
<br>
<br>
acc : ((s' : Size< s) → Acc s') → Acc s
<br>
<br>
then Acc reads as the accessibility predicate for the relation
_<_ on
<br>
Size such that i < j iff i : Size< j. The issue I raised
can of course
<br>
be rephrased by proving that the accessible part of the
relation _<_
<br>
coincides with the whole relation, in particular, Acc ∞, and
since _<_
<br>
is not well-founded (∞<∞) one gets a proof of False. Or one
can use ℕ
<br>
instead of Acc for that purpose, they're interchangeable here.
<br>
<br>
Now, Acc is an inductive definition, and so is ℕ. I don't see
how the
<br>
latter can denote co-natural numbers, which AFAIK require a
coinductive
<br>
definition?
<br>
<br>
Mind, I'm not saying that ℕ above is the appropriate way of
defining
<br>
sized natural numbers. But Agda accepts it - and it shouldn't,
because
<br>
after a few steps one gets a proof of False in safe mode...
<br>
<br>
<br>
<blockquote type="cite">On Mon, Oct 19, 2020 at 1:44 PM vlad
<a class="moz-txt-link-rfc2396E" href="mailto:Vlad.Rusu@inria.fr"><Vlad.Rusu@inria.fr></a> wrote:
<br>
<blockquote type="cite">Thanks for finding this. I guess
this is in a longer tradition of
<br>
problems with the sized types implementation, see e.g.
<br>
<a class="moz-txt-link-freetext" href="https://github.com/agda/agda/issues/2820">https://github.com/agda/agda/issues/2820</a>,
<br>
<a class="moz-txt-link-freetext" href="https://github.com/agda/agda/issues/3026">https://github.com/agda/agda/issues/3026</a>,
<br>
<a class="moz-txt-link-freetext" href="https://github.com/agda/agda/issues/1428">https://github.com/agda/agda/issues/1428</a>.
<br>
<br>
I don't understand whether it has overlap with existing
issues. You
<br>
don't use the infinity size, nor equality. So maybe it's a
new kind of
<br>
issue, coming from interaction of sizes with inductive
types?
<br>
<br>
It is an elaboration on the bug about well-founded
induction and sized types
(<a class="moz-txt-link-freetext" href="https://github.com/agda/agda/issues/3026">https://github.com/agda/agda/issues/3026</a>). 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 :
<br>
<br>
data ℕ {s : Size} : Set where
<br>
zero : ℕ
<br>
suc : ({s' : Size< s} → ℕ {s'}) → ℕ {s}
<br>
<br>
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:
<a class="moz-txt-link-freetext" href="https://github.com/agda/agda/issues/2820#issuecomment-339969286">https://github.com/agda/agda/issues/2820#issuecomment-339969286</a>)
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"
<br>
<br>
foo : ℕ
<br>
foo = size-elimproved (λ s → ℕ{s}) (λ _ H → suc λ { {j} →
H j } ) _
<br>
<br>
is easily shown to be a successor of itself, which the
definition of "natural numbers" forbids, hence the proof
of False.
<br>
<br>
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.
<br>
<br>
_______________________________________________
<br>
Agda mailing list
<br>
<a class="moz-txt-link-abbreviated" href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a>
<br>
<a class="moz-txt-link-freetext" href="https://lists.chalmers.se/mailman/listinfo/agda">https://lists.chalmers.se/mailman/listinfo/agda</a>
<br>
</blockquote>
</blockquote>
</blockquote>
</blockquote>
_______________________________________________
<br>
Agda mailing list
<br>
<a class="moz-txt-link-abbreviated" href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a>
<br>
<a class="moz-txt-link-freetext" href="https://lists.chalmers.se/mailman/listinfo/agda">https://lists.chalmers.se/mailman/listinfo/agda</a>
<br>
</blockquote>
</body>
</html>