Sandro Stucki

2018-03-08 08:02:20 UTC

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

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?

/Sandro

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

http://www.cse.chalmers.se/~nad/listings/partiality-monad/Lambda.Simplified.Delay-monad.Interpreter.html

--

/NAD

_______________________________________________

Agda mailing list

https://lists.chalmers.se/mailman/listinfo/agda

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

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

http://www.cse.chalmers.se/~nad/listings/partiality-monad/Lambda.Simplified.Delay-monad.Interpreter.html

I get a 404 error following that link.http://www.cse.chalmers.se/~nad/listings/partiality-monad/Lambda.Simplified.Delay-monad.Interpreter.html

/Sandro

Please, where it is described the delay monad ?

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

http://www.cse.chalmers.se/~nad/listings/partiality-monad/Lambda.Simplified.Delay-monad.Interpreter.html

--

/NAD

_______________________________________________

Agda mailing list

https://lists.chalmers.se/mailman/listinfo/agda