[ bsd3, control, library ] [ Propose Tags ]

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

## Modules

[Index] [Quick Jump]

• Control
• Data

#### Maintainer's Corner

Package maintainers

For package maintainers and hackage trustees

Candidates

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

[back to package description]

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

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 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.

--------

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

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

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