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

[Guillaume Allais]

Hi Sandro,

This pushed me to finally start the "codata" project on agda-stdlib
to make use of copattern-based sized codatatypes:
https://github.com/agda/agda-stdlib/projects/1

I have pushed a first few modules to the codata branch to start the
discussion one of which is Codata.Delay:
https://github.com/agda/agda-stdlib/blob/codata/src/Codata/Delay.agda

There is no guarantee whatsoever that this is the version that will
eventually land in the stdlib but it should hopefully give you an
idea of how these things work.

Best,
--
gallais

On 08/03/18 09:02, Sandro Stucki wrote:
> 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
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda


-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 833 bytes
Desc: OpenPGP digital signature
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20180308/d0d36750/attachment.sig>