Export `return` from `IO.Primitive`

[andreasabel]

Trying to check my development Type-preserving compilation via dependently typed syntax (SPLS March 2023) with the current standard library, I get a failure for a trivial reason:

The module IO.Primitive doesn't export the following:
  return
when scope checking the declaration
  open import IO.Primitive public using (return; _>>=_)

In this state, I see no easy way to make my development work with both std-lib 1.7.1/2 and 2.0.

An easy fix would be to restore return to this module with the alias return = pure which could maybe be coming with a deprecation warning.
(Though in my view there is no consensus in the FP community that return is a bad word and pure the good word. Esp. when the return statement is the last of my function, it makes perfectly sense to say return result rather than pure result).

Ref: https://github.com/agda/agda-stdlib/blame/master/src/IO/Primitive.agda

[gallais]

The issue is that return clashes with case_return_of_.

[andreasabel]

@gallais Please have a look at #2125 which adds the backwards-compatibility with v1.7 that I need for an IO-monadic Agda development (the one mentioned in the OP).

[jamesmckinna]

[UPDATED] Suggest instead:

• add the alias pure = return to v1.7.2 IO.Primitive (and, if necessary, any hiding (pure) directives in client modules where this might be a problem)
• adding 'stub' versions of Effect.Functor and Effect.Applicative (and Effect.Monad?) to v1.7.2 which provide the Raw* functionality, but otherwise publicly re-export from Category.*; how much of the Category.* tree do you actually require for your development?
• import in a both-versions-compatible way (in your talk-related client module(s)) open import IO.Primitive public using (_>>=_) renaming (pure to return)

Does that work?
TL;DR: patch/retrofit v1.7.2 (and if necessary, a minor version bump) so that it is forwards compatible with v2.0, not the other way round.

[jamesmckinna]

The discussion on #2129 seems to be asking for a v1.7.3 (or back-patching v1.7.2). Suggest we lift this out as a separate issue, and collect a number of issues which might be solved by such a thing (such as these two, but what else?), together with some discussion/agreement about what (minimal) patches might be necessary? But I do worry that this would be opening a door...

[MatthewDaggitt]

Given how widely return is used, maybe it should be case_return_of_ whose name should be changed? Thought I don't have any particular suggestions. Just throwing it out there @gallais ?

[gallais]

Yeah of course but as you said, there are no alternative name proposals (#356).
And on the other hand, should we pollute the namespace with an alias for pure just because
Haskell does so? Should we add fmap as an alias for _<$>_ because people may reach for
it out of habit?

[andreasabel]

Yeah of course but as you said, there are no alternative name proposals (#356).

case_yield_of_ would use a synonym of "return".
In other PLs (except maybe Coq), neither return nor yield is used for the return type, but always for the return value.

Also case_return:_of_ is thinkable with the : emphasizing a return type.

[JacquesCarette]

On Zulip, @jamesmckinna suggested case_returning_of_. I happen to also like your 'thinkable' suggestion. (i.e. either returning or return: would feel like an improvement). I don't feel that yield is much of an improvement for the very reason you mention: it still feels value-level rather than type-level.