[Agda] Partiality/delay monad [was: proofs for (NON)TERMINATING]

[Sandro Stucki]

I have a follow-up question about the partiality/delay monad.

A while ago, I wrote some code using the Partiality monad from the
standard library (Category.Monad.Partiality). But that module uses old
coinduction, which seems deprecated now:

  https://agda.readthedocs.io/en/v2.5.3/language/coinduction.html#old-coinduction

If I want to future-proof my code, what is the recommended way to go?

NAD says

> The standard library contains an implementation in
> Category.Monad.Partiality. I would not recommend that you use this
> implementation. I have another implementation that uses sized types, and
> which is therefore in my opinion easier to use (the delay-monad library,
> available from http://www.cse.chalmers.se/~nad/software.html). However,
> this implementation depends on a different library, which is set up in a
> somewhat roundabout way in order to cater to a certain experiment. I
> believe others have also implemented the delay monad using sized types.

So that is definitely an alternative, but as NAD points out, it adds
some extra dependencies, which I'd like to avoid. Are there any plans
to "upgrade" Category.Monad.Partiality to use coinductive records
and/or sized types?

> Here's an example of how one can implement an interpreter for the
> untyped λ-calculus using the delay monad:
>
> http://www.cse.chalmers.se/~nad/listings/partiality-monad/Lambda.Simplified.Delay-monad.Interpreter.html

I get a 404 error following that link.

/Sandro


On Wed, Jan 24, 2018 at 9:43 AM, Nils Anders Danielsson <nad at cse.gu.se> wrote:
> On 2018-01-23 19:54, Sergei Meshveliani wrote:
>>
>> Please, where it is described the delay monad ?
>
>
> Venanzio Capretta
> General Recursion via Coinductive Types
> https://doi.org/10.2168/LMCS-1(2:1)2005
>
> The standard library contains an implementation in
> Category.Monad.Partiality. I would not recommend that you use this
> implementation. I have another implementation that uses sized types, and
> which is therefore in my opinion easier to use (the delay-monad library,
> available from http://www.cse.chalmers.se/~nad/software.html). However,
> this implementation depends on a different library, which is set up in a
> somewhat roundabout way in order to cater to a certain experiment. I
> believe others have also implemented the delay monad using sized types.
>
> Here's an example of how one can implement an interpreter for the
> untyped λ-calculus using the delay monad:
>
>
> http://www.cse.chalmers.se/~nad/listings/partiality-monad/Lambda.Simplified.Delay-monad.Interpreter.html
>
> --
> /NAD
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda