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

[Joey Eremondi]

>
> But our enthusiasm for sized types in Agda was severely dampened when we
> learned later that in current versions they allow one to prove that true
> equals false :-( — see <https://github.com/agda/agda/issues/3026>.


Oh... well that definitely ruins what I was trying to do. Does --sized make
Agda inconsistent even with --safe enabled?

Looks like I'll have to either use Nat fuel or guardedness-based
coinduction.

Thanks!

On Fri, Apr 24, 2020 at 3:21 AM Andrew M. Pitts <amp12 at cam.ac.uk> wrote:

>
>
> > On 24 Apr 2020, at 10:41, Nils Anders Danielsson <nad at cse.gu.se> wrote:
> >
> > 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.
> >
> > Two data points:
> >
> > * I have found it practical to use sized coinductive types, together
> >  with explicit definitions of (strong or weak) bisimilarity.
> >
> > * I have found it less practical to use sized inductive types with
> >  /relevant/ size arguments together with propositional equality.
>
> I and my co-authors can’t seem to do without sized inductive types in the
> recent paper <https://www.cl.cam.ac.uk/~amp12/papers/coniqi/coniqi.pdf>
>
> But our enthusiasm for sized types in Agda was severely dampened when we
> learned later that in current versions they allow one to prove that true
> equals false :-( — see <https://github.com/agda/agda/issues/3026>.
>
> Andy Pitts
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20200424/7fb935e7/attachment.html>