monad-ideals: Ideal Monads and coproduct of them

[ bsd3, control, library ] [ Propose Tags ]

Type class to represent ideal monads in terms of the "ideal part" of ideal monads. See README for more.


[Skip to Readme]

Downloads

Maintainer's Corner

Package maintainers

For package maintainers and hackage trustees

Candidates

  • No Candidates
Versions [RSS] 0.1.0.0
Change log CHANGELOG.md
Dependencies base (>=4.14 && <4.21), bifunctor-classes-compat (>=0.1 && <1), comonad (>=5.0.8 && <5.1), semigroupoids (>=6.0.0 && <6.1) [details]
License BSD-3-Clause
Copyright Copyright (C) 2008 Edward A. Kmett, Copyright (C) 2004--2008 Dave Menendez, Copyright (C) 2007 Iavor Diatchki, Copyright (C) 2024 Koji Miyazato
Author Koji Miyazato
Maintainer viercc@gmail.com
Category Control
Home page https://github.com/viercc/monad-ideals
Source repo head: git clone https://github.com/viercc/monad-ideals.git -b main
Uploaded by viercc at 2024-05-01T14:24:23Z
Distributions NixOS:0.1.0.0
Downloads 20 total (7 in the last 30 days)
Rating (no votes yet) [estimated by Bayesian average]
Your Rating
  • λ
  • λ
  • λ
Status Docs available [build log]
Last success reported on 2024-05-01 [all 1 reports]

Readme for monad-ideals-0.1.0.0

[back to package description]

monad-ideals: Ideal Monads and coproduct of Monads

Revives Control.Monad.Ideal from old versions of category-extras.

Ideal Monads

Ideal monads1 are certain kind of monads. Informally, an ideal monad M is a Monad which can be written as a disjoint union of "pure" values and "impure" values, and its join operation on "impure" values never produces "pure" values.

data M a = Pure a | Impure (...)

pure :: a -> M a
pure = Pure

join :: M (M a) -> M a
join (Pure ma) = ma
join (Impure ...) = Impure (...)
  -- Impure values of @M a@ never becomes pure again 

Formally, an ideal monad m is a Monad equipped with

  • Functor m₀, called the ideal part of m
  • Natural isomorphism iso :: ∀a. Either a (m₀ a) -> m a (and its inverse iso⁻¹ :: ∀a. m a -> Either a (m₀ a))
  • Natural transformation idealize :: ∀a. m₀ (m a) -> m₀ a

satisfying these two properties.

  • iso . Left === pure :: ∀a. a -> m a
  • either id (iso . Right . idealize) . iso⁻¹ === join :: m (m a) -> m a

This package provides MonadIdeal, a type class to represent ideal monads in terms of its ideal part m₀ (instead of a subclass of Monad to represent ideal monad itself.)

class (Isolated m0, Bind m0) => MonadIdeal m0 where
  idealBind :: m0 a -> (a -> Ideal m0 b) -> m0 b

type Ideal m0 a

-- | Constructor of @Ideal@
ideal :: Either a (m0 a) -> Ideal m0 a

-- | Deconstructor of @Ideal@
runIdeal :: Ideal m0 a -> Either a (m0 a)

Here, Ideal m0 corresponds to the ideal monad which would have m0 as its ideal part.

Isolated class

There is a generalization to ideal monads, which are almost ideal monads, but lack a condition that says "an impure value does not become a pure value by the join operation".

A monad m in this class has natural isomorphism Either a (m₀ a) -> m a with some functor m₀, and pure is the part of m which is not m₀. Formally, the defining data of this class are:

  • Functor m₀, called the impure part of m
  • Natural isomorphism iso :: ∀a. Either a (m₀ a) -> m a (and its inverse iso⁻¹ :: ∀a. m a -> Either a (m₀ a))
  • iso . Left === pure :: ∀a. a -> m a

Combined with the monad laws of m, join :: ∀a. m (m a) -> m a must be equal to the following natural transformation with some impureJoin.

join :: ∀a. m (m a) -> m a
join mma = case iso⁻¹ mma of
  Left ma -> ma
  Right m₀ma -> impureJoin m₀ma
  where
    impureJoin :: ∀a. m₀ (m a) -> m a

The Isolated class is a type class for a functor which can be thought of as an impure part of some monad.

newtype Unite f a = Unite { runUnite :: Either a (f a) }

class Functor m0 => Isolated m0 where
  impureBind :: m0 a -> (a -> Unite m0 b) -> Unite m0 b

Coproduct of monads

Coproduct m ⊕ n of two monads2 m, n is the coproduct (category-theoretic sum) in the category of monad and monad morphisms. 3

In basic terms, m ⊕ n is a monad with the following functions and properties.

  • Monad morphism inject1 :: ∀a. m a -> (m ⊕ n) a

  • Monad morphism inject2 :: ∀a. n a -> (m ⊕ n) a

  • Function eitherMonad which takes two monad morphisms and return a monad morphism.

    eitherMonad :: (∀a. m a -> t a) -> (∀a. n a -> t a) -> (∀a. (m ⊕ n) a -> t a)
    
  • Given arbitrary monads m, n, t,

    • For all monad morphisms f1 and f2,

      • eitherMonad f1 f2 . inject1 = f1
      • eitherMonad f1 f2 . inject2 = f2
    • For any monad morphism f :: ∀a. (m ⊕ n) a -> t a, f equals to eitherMonad f1 f2 for some unique f1, f2. Or, equvalently, f = eitherMonad (f . inject1) (f . inject2).

Coproduct of two monads does not always exist, but for ideal monads or monads with Isolated impure parts, their coproducts exist. This package provides a type constructor (:+) below.

-- Control.Monad.Coproduct
data (:+) (m :: Type -> Type) (n :: Type -> Type) (a :: Type)

Using this type constructor, coproduct of monad can be constructed in two ways.

  • If m0, n0 are Isolated i.e. the impure part of monads Unite m0, Unite n0 respectively, m0 :+ n0 is also Isolated and Unite (m0 :+ n0) is the coproduct of monads Unite m0 ⊕ Unite n0.

  • If m0, n0 are MonadIdeal i.e. the ideal part of ideal monads Ideal m0, Ideal n0 respectively, m0 :+ n0 is also MonadIdeal and Ideal (m0 :+ n0) is the coproduct of monads Ideal m0 ⊕ Ideal n0.

Duals

This package also provides the duals of ideal monads and coproducts of them: Coideal comonads and products of them.

--------

1

N. Ghani and T. Uustalu, “Coproducts of ideal monads,” Theoret. Inform. and Appl., vol. 38, pp. 321–342, 2004.

2

Jiří Adámek, Nathan Bowler, Paul B. Levy and Stefan Milius, "Coproducts of Monads on Set." (https://doi.org/10.48550/arXiv.1409.3804)

3

To name the same concept to monad morphism, the term "monad transformation" is used in transformers package (Control.Monad.Trans.Class.)