<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>