Backward compatibility with v1.7.1/2 for the IO Monad

[andreasabel]

• Fix Export return from IO.Primitive #2124: IO.Primitive.return (alias for pure) for backwards compat
• Restore Category/* tree of v1.7 as deprected module aliases

These patches allow me to port an Agda development using v1.7.1 to v2.0 (current master).

The code I want to have working with both version uses do for the IO monad and mapM.

foo = do
   ...
   _ <- mapM f xs
   ...
   return _
   where
   open IOMonad
   open TraversableM record{ IOMonad }

So I am using the module based technique to bring >>= into scope for the do notation.

Previously (v1.7), I defined IOMonad like this:

module IOMonad where
  open import IO.Primitive public using (return; _>>=_)

  infixl 1 _>>_

  _>>_  : ∀ {b} {B : Set b} → IO ⊤ → IO B → IO B
  _>>_ = λ m m' → m >>= λ _ → m'

  infixr 1 _=<<_

  _=<<_  : ∀ {a b} {A : Set a} {B : Set b} → (A → IO B) → IO A → IO B
  k =<< m = m >>= k

This definition was good enough to form record {IOMonad} for the instantiation of TraversableM.

With v2.0, forming a RawMonad also needs embedded instances of RawFunctor and RawApplicative.
I managed to make the definition of IOMonad compatible with v2.0 by changing it to be the following:

open import Category.Functor     using (RawFunctor)
open import Category.Applicative using (RawApplicative)

module IOFunctor where
  open import IO.Primitive public using (return; _>>=_)

  infixl 1 _>>_

  _>>_  : ∀ {b} {B : Set b} → IO ⊤ → IO B → IO B
  _>>_ = λ m m' → m >>= λ _ → m'

  infixr 1 _=<<_

  _=<<_  : ∀ {a b} {A : Set a} {B : Set b} → (A → IO B) → IO A → IO B
  k =<< m = m >>= k

  -- The following definition is needed to create the RawFunctor instance.

  infixl 4 _<$>_

  _<$>_ :  ∀ {a b} {A : Set a} {B : Set b} → (A → B) → IO A → IO B
  f <$> m = m >>= λ a -> return (f a)

-- This module is needed to create the RawApplicative instance
-- in a way compatible with both std-lib v1.7.1/2 and v2.0.

module IOApplicative where
  open IOFunctor public

  rawFunctor : ∀{ℓ} → RawFunctor (IO {a = ℓ})
  rawFunctor = record { IOFunctor }

  pure : ∀{a} {A : Set a} → A → IO A
  pure = return

  infixl 4 _<*>_ _⊛_

  _<*>_ : ∀ {a b} {A : Set a} {B : Set b} → IO (A → B) → IO A → IO B
  mf <*> ma = mf >>= λ f → ma >>= λ a → return (f a)

  _⊛_ : ∀ {a b} {A : Set a} {B : Set b} → IO (A → B) → IO A → IO B
  _⊛_ = _<*>_

module IOMonad where
  open IOApplicative public

  -- Field rawApplicative is part of the RawMonad of std-lib v2.0
  -- Thus we have to construct the Applicative implementation
  -- even though we do not use it.
  --
  rawApplicative : ∀{ℓ} → RawApplicative (IO {a = ℓ})
  rawApplicative = record { IOApplicative }

This works with 1.7.1/2. To have it work with 2.0 as well, the present PR is needed, because:

• I need to be able to import return from IO.Primitive.
• I need to be able to import Raw* from Category.* (for * in {Functor, Applicative}).

[gallais]

I thought that the point of v2.0 was that we were happy to break backwards compatibility more aggressively?
Otherwise we may as well call it v1.8.

Also, if this does get in then IO.Primitive's return should definitely be deprecated
because of the name clash I mention in the related issue which was the motivation
behind getting rid of it in the first place.

[jamesmckinna]

And... the whole point of the breaking change to remove the top-level namespace entry Category.* altogether. The subsidiary *.Categorical modules were (eventually ;-)) retained for backwards compatibility, but this change would condemns us to another cycle of versions which can't make use of anything agda-categories to populate Category.*.

So I would be strongly against this merge, FWIW.

[jamesmckinna]

Can the definitions of rawFunctor and rawApplicative (not?) be inlined (without associated type declarations) in the definition of record{ IOMonad }?

[andreasabel]

@jamesmckinna wrote:

Can the definitions of rawFunctor and rawApplicative (not?) be inlined (without associated type declarations) in the definition of record{ IOMonad }?

The problem is that v1.7 does not expect such fields here in a RawMonad. The trick I am using here is that record{ M } will pick from M the fields it needs and ignores the rest of M.

@jamesmckinna wrote:

but this change would condemns us to another cycle of versions which can't make use of anything agda-categories to populate Catgeory.*.

Ah, sorry, I was not aware of such plans. Currently, Category.* is unused, and agda-categories uses Categories.*.

@gallais wrote:

Also, if this does get in then IO.Primitive's return should definitely be deprecated

I added a deprecation warning.

[jamesmckinna]

@jamesmckinna wrote:

but this change would condemns us to another cycle of versions which can't make use of anything agda-categories to populate Category.*.

Ah, sorry, I was not aware of such plans. Currently, Category.* is unused, and agda-categories uses Categories.*.

Issue #1636 / PR #1735

[jamesmckinna]

@andreasabel wrote:

@jamesmckinna wrote:

Can the definitions of rawFunctor and rawApplicative (not?) be inlined (without associated type declarations) in the definition of record{ IOMonad }?

The problem is that v1.7 does not expect such fields here in a RawMonad. The trick I am using here is that record{ M } will pick from M the fields it needs and ignores the rest of M.

Yes, I see. But I think the suggestion might (?) still work, even with the module IOMonad if the definitions rawFunctor and rawApplicative are given without type signatures. There are examples of this in stdlib, with local naming of Algebra.Bundles.* objects without explicitly giving their signatures. It does actually cause problems #2112 in some cases, but here? I wonder...

[MatthewDaggitt]

This works with 1.7.1/2. To have it work with 2.0 as well, the present PR is needed, because:

Yes, as @gallais and @jamesmckinna have identified, this is the crux of the problem. We've taken the decision not to preserve backwards compatibility with the 2.0 release.

What reason do you need for working both with 1.7.2 and the unreleased 2.0 at the same time? Could you simply upgrade when 2.0 is released?

[andreasabel]

@jamesmckinna wrote:

I think the suggestion might (?) still work, even with the module IOMonad if the definitions rawFunctor and rawApplicative are given without type signatures.

Thanks for the hint. I tried it out. I got unsolved metas because these defs are polymorphic. But even if I could solve this problem, there would still be the problem that an alias foo = record{Bar} does not work as the elaboration of record{Bar} needs to know which fields you want to pick from module Bar. So you need the record type here.

[andreasabel]

On a more general note, my goal is to develop such that:

1. My code works with the latest release of std-lib.
2. My code also works with the master of std-lib.

Unfortunately, Agda does not natively understand CPP; that's the technique used in GHC Haskell to support different API versions. I also lacks good support for dependency versioning (like Cabal's MIN_VERSION_package macros).

So far, I have been relying on the backwards compatibility of the std-lib. Things have not been removed from one release to the next, but just deprecated. Then, after the release, one can fix the deprecation warnings to again get something that works with the latest release and the master.

In the current gap between v1.7 and master I have to either use CPP or fork my project.

I think you must have discussed this scenario; do you have some advise how to proceed here?

In the present situation, because Agda 2.6.4 also works with 1.7.1/2, I could postpone updating my project to the next std-lib, but in general, there could be a problem...

[andreasabel]

@jamesmckinna wrote:

And... the whole point of the breaking change to remove the top-level namespace entry Category.* altogether. The subsidiary *.Categorical modules were (eventually ;-)) retained for backwards compatibility, but this change would condemns us to another cycle of versions which can't make use of anything agda-categories to populate Catgeory.*.

It seems like if v2.0 does not aim to populate the Category.* module tree, it should be possible to remove the aliases I propose here directly after the release of v2.0 and so they would be free for use in v2.1. Or maybe there is a policy of having names unused for one release before rededication? (Like phone numbers should rest for a couple of years before recycling...)

[jamesmckinna]

Have you tried the suggestion proposed in #2124 (comment)?

[andreasabel]

Have you tried the suggestion proposed in #2124 (comment)?

Making 1.7 forward compatible is of course another alternative, that would mean adding Effect.* modules in there reflecting the new organization in 2.0.
Forward compatibility releases would of course be a new path we have not walked so far.

Btw, I just released Agda 2.6.4!

[jamesmckinna]

Have you tried the suggestion proposed in #2124 (comment)?

Making 1.7 forward compatible is of course another alternative, that would mean adding Effect.* modules in there reflecting the new organization in 2.0. Forward compatibility releases would of course be a new path we have not walked so far.

Btw, I just released Agda 2.6.4!

Ah... there really seems to be no good solution without, in some way, interpolating @gallais 's hypothetical "v1.8" or "v1.7.3". Maddening! Or else, craving your indulgence to accept a breaking change, this one time. I understand the desire to maintain a 'smooth'/'progressive' upgrade/deprecation path (and v2.0 incorporates many such detours where it has been possible), but v2.0 has so many changes over v1.7.* that I think we would like users to accept... the break.

Shout-outs to @gallais and @MatthewDaggitt ... I am a still newcomer, albeit 'relatively' such.

[jamesmckinna]

Of course, we haven't consider forward compatibility before, I'm a drowning man clutching at anything that floats by, while trying to defend breaking changes that required quite some effort to achieve (and which I have already rolled back on once already, again on request from you).

If we were to consider it as policy, then I could imagine that would/might open a world of pain in respect of any particular development which some user or other wishes to maintain. Your situation in that regard is somewhat different... ;-)

I am not, nor I think could be, any (final) arbiter in this.

[shhyou]

So far, I have been relying on the backwards compatibility of the std-lib. Things have not been removed from one release to the next, but just deprecated. Then, after the release, one can fix the deprecation warnings to again get something that works with the latest release and the master.

FWIW, stdlib 2.0 is backwards-incompatible in many different ways in addition to declaring some definitions as deprecated. If I understand correctly, the hierarchy of quite some modules is reorganized with exports being moved around; some definitions change implicit arguments to explicit; some definitions have different implementation so their proofs have to change, etc.

[MatthewDaggitt]

Closing as superseded by #2141