From 804bf6f1e67325500076bb89a7245b18935bd80a Mon Sep 17 00:00:00 2001 From: Andreas Abel Date: Fri, 6 Oct 2023 09:51:05 +0200 Subject: [PATCH 1/3] Fix #2124: `IO.Primitive.return` (alias for `pure`) for backwards compat --- src/IO/Primitive.agda | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/src/IO/Primitive.agda b/src/IO/Primitive.agda index 220e862fb4..cdfe4dddc4 100644 --- a/src/IO/Primitive.agda +++ b/src/IO/Primitive.agda @@ -23,6 +23,11 @@ postulate pure : ∀ {a} {A : Set a} → A → IO A _>>=_ : ∀ {a b} {A : Set a} {B : Set b} → IO A → (A → IO B) → IO B +-- Alias 'return' for backwards compatibility. + +return : ∀ {a} {A : Set a} → A → IO A +return = pure + {-# COMPILE GHC pure = \_ _ -> return #-} {-# COMPILE GHC _>>=_ = \_ _ _ _ -> (>>=) #-} {-# COMPILE UHC pure = \_ _ x -> UHC.Agda.Builtins.primReturn x #-} From ac1dba79191733d49bc765f5c51487a3a5aa03d1 Mon Sep 17 00:00:00 2001 From: Andreas Abel Date: Fri, 6 Oct 2023 11:10:05 +0200 Subject: [PATCH 2/3] Restore Category/* tree of v1.7 as deprected module aliases For backwards compatibility. This allows Agda developments that use monads to be made to work with both v1.7 and v2.0 of the standard library. --- src/Category/Applicative.agda | 17 +++++++++++++++++ src/Category/Applicative/Indexed.agda | 17 +++++++++++++++++ src/Category/Applicative/Predicate.agda | 17 +++++++++++++++++ src/Category/Comonad.agda | 17 +++++++++++++++++ src/Category/Functor.agda | 17 +++++++++++++++++ src/Category/Functor/Indexed.agda | 17 +++++++++++++++++ src/Category/Functor/Predicate.agda | 17 +++++++++++++++++ src/Category/Monad.agda | 17 +++++++++++++++++ src/Category/Monad/Continuation.agda | 17 +++++++++++++++++ src/Category/Monad/Indexed.agda | 17 +++++++++++++++++ src/Category/Monad/Partiality.agda | 17 +++++++++++++++++ src/Category/Monad/Partiality/All.agda | 17 +++++++++++++++++ src/Category/Monad/Partiality/Instances.agda | 17 +++++++++++++++++ src/Category/Monad/Predicate.agda | 17 +++++++++++++++++ src/Category/Monad/Reader.agda | 17 +++++++++++++++++ src/Category/Monad/State.agda | 17 +++++++++++++++++ 16 files changed, 272 insertions(+) create mode 100644 src/Category/Applicative.agda create mode 100644 src/Category/Applicative/Indexed.agda create mode 100644 src/Category/Applicative/Predicate.agda create mode 100644 src/Category/Comonad.agda create mode 100644 src/Category/Functor.agda create mode 100644 src/Category/Functor/Indexed.agda create mode 100644 src/Category/Functor/Predicate.agda create mode 100644 src/Category/Monad.agda create mode 100644 src/Category/Monad/Continuation.agda create mode 100644 src/Category/Monad/Indexed.agda create mode 100644 src/Category/Monad/Partiality.agda create mode 100644 src/Category/Monad/Partiality/All.agda create mode 100644 src/Category/Monad/Partiality/Instances.agda create mode 100644 src/Category/Monad/Predicate.agda create mode 100644 src/Category/Monad/Reader.agda create mode 100644 src/Category/Monad/State.agda diff --git a/src/Category/Applicative.agda b/src/Category/Applicative.agda new file mode 100644 index 0000000000..370a91a8fa --- /dev/null +++ b/src/Category/Applicative.agda @@ -0,0 +1,17 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- This module is DEPRECATED. Please use +-- `Effect.Applicative` instead. +------------------------------------------------------------------------ + +{-# OPTIONS --cubical-compatible --safe #-} + +module Category.Applicative where + +open import Effect.Applicative public + +{-# WARNING_ON_IMPORT +"Category.Applicative was deprecated in v2.0. +Use Effect.Applicative instead." +#-} diff --git a/src/Category/Applicative/Indexed.agda b/src/Category/Applicative/Indexed.agda new file mode 100644 index 0000000000..a09e2fb8cd --- /dev/null +++ b/src/Category/Applicative/Indexed.agda @@ -0,0 +1,17 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- This module is DEPRECATED. Please use +-- `Effect.Applicative.Indexed` instead. +------------------------------------------------------------------------ + +{-# OPTIONS --cubical-compatible --safe #-} + +module Category.Applicative.Indexed where + +open import Effect.Applicative.Indexed public + +{-# WARNING_ON_IMPORT +"Category.Applicative.Indexed was deprecated in v2.0. +Use Effect.Applicative.Indexed instead." +#-} diff --git a/src/Category/Applicative/Predicate.agda b/src/Category/Applicative/Predicate.agda new file mode 100644 index 0000000000..2f69be1f05 --- /dev/null +++ b/src/Category/Applicative/Predicate.agda @@ -0,0 +1,17 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- This module is DEPRECATED. Please use +-- `Effect.Applicative.Predicate` instead. +------------------------------------------------------------------------ + +{-# OPTIONS --cubical-compatible --safe #-} + +module Category.Applicative.Predicate where + +open import Effect.Applicative.Predicate public + +{-# WARNING_ON_IMPORT +"Category.Applicative.Predicate was deprecated in v2.0. +Use Effect.Applicative.Predicate instead." +#-} diff --git a/src/Category/Comonad.agda b/src/Category/Comonad.agda new file mode 100644 index 0000000000..7a5be7e0da --- /dev/null +++ b/src/Category/Comonad.agda @@ -0,0 +1,17 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- This module is DEPRECATED. Please use +-- `Effect.Comonad` instead. +------------------------------------------------------------------------ + +{-# OPTIONS --cubical-compatible --safe #-} + +module Category.Comonad where + +open import Effect.Comonad public + +{-# WARNING_ON_IMPORT +"Category.Comonad was deprecated in v2.0. +Use Effect.Comonad instead." +#-} diff --git a/src/Category/Functor.agda b/src/Category/Functor.agda new file mode 100644 index 0000000000..4c5b6ec450 --- /dev/null +++ b/src/Category/Functor.agda @@ -0,0 +1,17 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- This module is DEPRECATED. Please use +-- `Effect.Functor` instead. +------------------------------------------------------------------------ + +{-# OPTIONS --cubical-compatible --safe #-} + +module Category.Functor where + +open import Effect.Functor public + +{-# WARNING_ON_IMPORT +"Category.Functor was deprecated in v2.0. +Use Effect.Functor instead." +#-} diff --git a/src/Category/Functor/Indexed.agda b/src/Category/Functor/Indexed.agda new file mode 100644 index 0000000000..6f02824566 --- /dev/null +++ b/src/Category/Functor/Indexed.agda @@ -0,0 +1,17 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- This module is DEPRECATED. Please use +-- `Effect.Functor.Indexed` instead. +------------------------------------------------------------------------ + +{-# OPTIONS --cubical-compatible --safe #-} + +module Category.Functor.Indexed where + +open import Effect.Functor.Indexed public + +{-# WARNING_ON_IMPORT +"Category.Functor.Indexed was deprecated in v2.0. +Use Effect.Functor.Indexed instead." +#-} diff --git a/src/Category/Functor/Predicate.agda b/src/Category/Functor/Predicate.agda new file mode 100644 index 0000000000..f0d065bea7 --- /dev/null +++ b/src/Category/Functor/Predicate.agda @@ -0,0 +1,17 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- This module is DEPRECATED. Please use +-- `Effect.Functor.Predicate` instead. +------------------------------------------------------------------------ + +{-# OPTIONS --cubical-compatible --safe #-} + +module Category.Functor.Predicate where + +open import Effect.Functor.Predicate public + +{-# WARNING_ON_IMPORT +"Category.Functor.Predicate was deprecated in v2.0. +Use Effect.Functor.Predicate instead." +#-} diff --git a/src/Category/Monad.agda b/src/Category/Monad.agda new file mode 100644 index 0000000000..01143536a4 --- /dev/null +++ b/src/Category/Monad.agda @@ -0,0 +1,17 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- This module is DEPRECATED. Please use +-- `Effect.Monad` instead. +------------------------------------------------------------------------ + +{-# OPTIONS --cubical-compatible --safe #-} + +module Category.Monad where + +open import Effect.Monad public + +{-# WARNING_ON_IMPORT +"Category.Monad was deprecated in v2.0. +Use Effect.Monad instead." +#-} diff --git a/src/Category/Monad/Continuation.agda b/src/Category/Monad/Continuation.agda new file mode 100644 index 0000000000..7f0bb177ec --- /dev/null +++ b/src/Category/Monad/Continuation.agda @@ -0,0 +1,17 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- This module is DEPRECATED. Please use +-- `Effect.Monad.Continuation` instead. +------------------------------------------------------------------------ + +{-# OPTIONS --cubical-compatible --safe #-} + +module Category.Monad.Continuation where + +open import Effect.Monad.Continuation public + +{-# WARNING_ON_IMPORT +"Category.Monad.Continuation was deprecated in v2.0. +Use Effect.Monad.Continuation instead." +#-} diff --git a/src/Category/Monad/Indexed.agda b/src/Category/Monad/Indexed.agda new file mode 100644 index 0000000000..d5eaa29462 --- /dev/null +++ b/src/Category/Monad/Indexed.agda @@ -0,0 +1,17 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- This module is DEPRECATED. Please use +-- `Effect.Monad.Indexed` instead. +------------------------------------------------------------------------ + +{-# OPTIONS --cubical-compatible --safe #-} + +module Category.Monad.Indexed where + +open import Effect.Monad.Indexed public + +{-# WARNING_ON_IMPORT +"Category.Monad.Indexed was deprecated in v2.0. +Use Effect.Monad.Indexed instead." +#-} diff --git a/src/Category/Monad/Partiality.agda b/src/Category/Monad/Partiality.agda new file mode 100644 index 0000000000..c580eb274e --- /dev/null +++ b/src/Category/Monad/Partiality.agda @@ -0,0 +1,17 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- This module is DEPRECATED. Please use +-- `Effect.Monad.Partiality` instead. +------------------------------------------------------------------------ + +{-# OPTIONS --cubical-compatible --safe #-} + +module Category.Monad.Partiality where + +open import Effect.Monad.Partiality public + +{-# WARNING_ON_IMPORT +"Category.Monad.Partiality was deprecated in v2.0. +Use Effect.Monad.Partiality instead." +#-} diff --git a/src/Category/Monad/Partiality/All.agda b/src/Category/Monad/Partiality/All.agda new file mode 100644 index 0000000000..216c28e04d --- /dev/null +++ b/src/Category/Monad/Partiality/All.agda @@ -0,0 +1,17 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- This module is DEPRECATED. Please use +-- `Effect.Monad.Partiality.All` instead. +------------------------------------------------------------------------ + +{-# OPTIONS --cubical-compatible --safe #-} + +module Category.Monad.Partiality.All where + +open import Effect.Monad.Partiality.All public + +{-# WARNING_ON_IMPORT +"Category.Monad.Partiality.All was deprecated in v2.0. +Use Effect.Monad.Partiality.All instead." +#-} diff --git a/src/Category/Monad/Partiality/Instances.agda b/src/Category/Monad/Partiality/Instances.agda new file mode 100644 index 0000000000..7917c17d99 --- /dev/null +++ b/src/Category/Monad/Partiality/Instances.agda @@ -0,0 +1,17 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- This module is DEPRECATED. Please use +-- `Effect.Monad.Partiality.Instances` instead. +------------------------------------------------------------------------ + +{-# OPTIONS --cubical-compatible --safe #-} + +module Category.Monad.Partiality.Instances where + +open import Effect.Monad.Partiality.Instances public + +{-# WARNING_ON_IMPORT +"Category.Monad.Partiality.Instances was deprecated in v2.0. +Use Effect.Monad.Partiality.Instances instead." +#-} diff --git a/src/Category/Monad/Predicate.agda b/src/Category/Monad/Predicate.agda new file mode 100644 index 0000000000..df6f29c12a --- /dev/null +++ b/src/Category/Monad/Predicate.agda @@ -0,0 +1,17 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- This module is DEPRECATED. Please use +-- `Effect.Monad.Predicate` instead. +------------------------------------------------------------------------ + +{-# OPTIONS --cubical-compatible --safe #-} + +module Category.Monad.Predicate where + +open import Effect.Monad.Predicate public + +{-# WARNING_ON_IMPORT +"Category.Monad.Predicate was deprecated in v2.0. +Use Effect.Monad.Predicate instead." +#-} diff --git a/src/Category/Monad/Reader.agda b/src/Category/Monad/Reader.agda new file mode 100644 index 0000000000..217e033d8b --- /dev/null +++ b/src/Category/Monad/Reader.agda @@ -0,0 +1,17 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- This module is DEPRECATED. Please use +-- `Effect.Monad.Reader` instead. +------------------------------------------------------------------------ + +{-# OPTIONS --cubical-compatible --safe #-} + +module Category.Monad.Reader where + +open import Effect.Monad.Reader public + +{-# WARNING_ON_IMPORT +"Category.Monad.Reader was deprecated in v2.0. +Use Effect.Monad.Reader instead." +#-} diff --git a/src/Category/Monad/State.agda b/src/Category/Monad/State.agda new file mode 100644 index 0000000000..24007b3516 --- /dev/null +++ b/src/Category/Monad/State.agda @@ -0,0 +1,17 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- This module is DEPRECATED. Please use +-- `Effect.Monad.State` instead. +------------------------------------------------------------------------ + +{-# OPTIONS --cubical-compatible --safe #-} + +module Category.Monad.State where + +open import Effect.Monad.State public + +{-# WARNING_ON_IMPORT +"Category.Monad.State was deprecated in v2.0. +Use Effect.Monad.State instead." +#-} From 4a760fb6064ea16e28d59784208e9edf5e57c6b9 Mon Sep 17 00:00:00 2001 From: Andreas Abel Date: Fri, 6 Oct 2023 11:50:27 +0200 Subject: [PATCH 3/3] Deprecation warning for `IO.Primitive.return` --- src/IO/Primitive.agda | 20 +++++++++++++++----- 1 file changed, 15 insertions(+), 5 deletions(-) diff --git a/src/IO/Primitive.agda b/src/IO/Primitive.agda index cdfe4dddc4..6a44c79e39 100644 --- a/src/IO/Primitive.agda +++ b/src/IO/Primitive.agda @@ -23,12 +23,22 @@ postulate pure : ∀ {a} {A : Set a} → A → IO A _>>=_ : ∀ {a b} {A : Set a} {B : Set b} → IO A → (A → IO B) → IO B --- Alias 'return' for backwards compatibility. - -return : ∀ {a} {A : Set a} → A → IO A -return = pure - {-# COMPILE GHC pure = \_ _ -> return #-} {-# COMPILE GHC _>>=_ = \_ _ _ _ -> (>>=) #-} {-# COMPILE UHC pure = \_ _ x -> UHC.Agda.Builtins.primReturn x #-} {-# COMPILE UHC _>>=_ = \_ _ _ _ x y -> UHC.Agda.Builtins.primBind x y #-} + +------------------------------------------------------------------------ +-- DEPRECATED NAMES +------------------------------------------------------------------------ +-- Please use the new names as continuing support for the old names is +-- not guaranteed. + +-- Version 2.0 + +return : ∀ {a} {A : Set a} → A → IO A +return = pure +{-# WARNING_ON_USAGE return +"Warning: return was deprecated in v2.0. +Please use pure instead." +#-}