search

agda / agda-stdlib

The Agda standard library
https://wiki.portal.chalmers.se/agda/Libraries/StandardLibrary
Other
575 stars 237 forks source link

Add `_>>_` for `IO.Primitive.Core` #2374

Closed ncfavier closed 5 months ago

ncfavier commented 5 months ago

This has to be in scope for desugaring do blocks that don't bind intermediate results.

JacquesCarette commented 5 months ago

Please all add CHANGELOG entry - but otherwise looks good.

jamesmckinna commented 5 months ago

[Comment deleted after rereading the PR name in the light of the actual commit: but it seems a bad idea in general to mention deprecated module names in PRs?]

gallais commented 5 months ago

What is your use case? In theory you're not supposed to use IO.Primitive and instead rely on IO.Base which does have everything you need to desugar do blocks.

ncfavier commented 5 months ago

Just making a simple demonstration program that does not need the fancy coinductive IO, so I thought I'd use the primitive one. Doesn't really make a difference either way.

ncfavier commented 5 months ago

Oh, I guess a better answer would be: I want to do IO and I don't want to enable --guardedness.

jamesmckinna commented 5 months ago

Oh, I guess a better answer would be: I want to do IO and I don't want to enable --guardedness.

But is that sufficient grounds for us extending such functionality to all clients of stdlib? I'm not clear whether we should...

ncfavier commented 5 months ago

Is there a cost?

jamesmckinna commented 5 months ago

Is there a cost?

So I realise that I am out of my depth here; I had imagined (at a minimum) that moving the definition of _>>_ would at least incur a deprecation cost, but digging a bit deeper I now see that this isn't 'moving' that definition at all...

... But there remains the question of how/whether the library should support your use case... and for that, I'll throw the question back to you and @gallais ... but perhaps in this instance it's 'harmless' (although slavishly offering a 'shallow' emulation of haskell IO, and exposing that as part of the library API, seems maybe something we don't want?)...

... but then: what's the cost (to you) of working with --guardedness?

ncfavier commented 5 months ago

But there remains the question of how/whether the library should support your use case

It already does. I'm just making a minor quality-of-life improvement for when someone imports the already existing IO.Primitive.Core module.