[Agda] Nat Fuel vs Sized Types (and other Sized Type questions)

[Andreas Abel]

 > * Is there a general guideline for when to use sizes vs nats? Do sized
 > types give us anything Nats don't, other than having a solver, ∞ and
 > some implicit niceness? Or do they make the type theory strictly more
 > powerful?

Sizes stand for ordinals in general, not just natural numbers.  You can 
use them with infinitely branching types, like W or Acc.

 > * How does unification work with sizes? Why do the above unifications
 > fail? Is ↑ not injective?

No, this does not work.

 > * How does the subtyping work with sizes? Is T i < T (i ⊔ˢ j)?
 > Or (T i) < (T j) when i : Size< j? Or do I need to write manual
 > "size-lifting" functions?

In theory, you should get both T i <= T (i ⊔ˢ j) and T i <= T j.

 > * Does --without-K or --cubical interact with sized types in a weird way?

I wouldn't think so.

 > * Is there a general way to write a fixed-point combinator in with sized
 > types? Something like:
 >    mu : (A : Size -> Set) -> ( (i : Size) -> A i -> A (↑ i) ) -> (j :
 > Size) -> A j

No.  A definition like

    mu A F (↑ i) = F i (mu A F i)

would be non-terminating, since we do not match (or block) on sizes.

 > * Likewise, is there any way to write a sized-version of a type-fixed
 > point combinator (Mu : (Set -> Set) -> Set)

No:

   Mu F i = Sigma (Size< i) \ { j -> Mu F j }

would suffer from the same problem (non-termination).

On 2020-04-22 05:56, Joey Eremondi wrote:
> I'm wondering if there are general guidelines as to when to use sized 
> types vs. just using natural numbers as fuel/index.
> 
> ** My Problem **
> I've tried adding sized types to a proof I'm working on to establish an 
> explicit termination argument. However, in case splits I'm getting stuck 
> on unification problems like this.
> ↑ sz ≟ ↑ sz'
> or ↑ sz ≟  sz'
> 
> ** My Questions **
> 
> * Is there a general guideline for when to use sizes vs nats? Do sized 
> types give us anything Nats don't, other than having a solver, ∞ and 
> some implicit niceness? Or do they make the type theory strictly more 
> powerful?
> 
> * How does unification work with sizes? Why do the above unifications 
> fail? Is ↑ not injective?
> 
> * How does the subtyping work with sizes? Is T i < T (i ⊔ˢ j)?
> Or (T i) < (T j) when i : Size< j? Or do I need to write manual 
> "size-lifting" functions?
> 
> * Does --without-K or --cubical interact with sized types in a weird way?
> 
> * Is there a general way to write a fixed-point combinator in with sized 
> types? Something like:
>    mu : (A : Size -> Set) -> ( (i : Size) -> A i -> A (↑ i) ) -> (j : 
> Size) -> A j
> 
> * Likewise, is there any way to write a sized-version of a type-fixed 
> point combinator (Mu : (Set -> Set) -> Set)
> 
> Thanks!
> 
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>