从各个角度看Monad - 数学,图解和程序化

Question

我正在尝试将Monad的分类定义与我在其他一些教程/书籍中看到的其他一般表示/定义进行协调.

下面,我(也许是有力的)试图将两个定义关闭,请指出错误并提供更正,如果需要的话

所以从Monads的定义开始

Monads只是endofunctors类别中的幺半群.

并且对endofunctors有一点了解,我假设一个Monad可以写成

((a->b)->Ma->Mb)->((b->c)->Mb->Mc) 

TypeLHS(左手边)的' ' Mb和RHS的类型是Mc,所以我想我可以写如下

Mb-> (b->c)-> Mc, **which is how we define bind**

这里是我看到Monads在endofuctors类别中的方式(它们本身在CategoryC中,而types'as as objects)

.

这有什么意义吗？

Answer 1

嗯,我觉得你有点不对劲.monad是一个endofunctor,它在Hask(Haskell类型的类别)中F :: * -> *具有一些功能,它知道如何将态射(函数)注入到Hask的子类中,其中Fs作为态射,Fs作为对象fmap.你在那里拥有的东西似乎是哈斯克的自然变革.

例如:Maybe,Either a,(,) a等.

现在monad也必须有2个自然变换(Functor F, Functor g => F a -> G a在hask中).

n : Identity -> M
u : M^2 -> M

或者在haskell代码中

n :: Identity a -> M a -- Identity a == a
u :: M (M a) -> M a

分别对应于return和join.

现在我们必须去>>=.你有什么绑定实际上只是fmap,我们真正想要的是m a -> (a -> m b) -> m b.这很容易定义为

 m >>= f = join $ f `fmap` m

田田!我们有单子.现在为这个幺半群的endofunctors.

在endofunctors上的monoid将有一个仿函数作为对象和自然变换作为态射.有趣的是,两个endofunctor的产品是它们的组成.这是我们新的monoid的Haskell代码

type (f <+> g) a = f (g a)
class Functor m => Monoid' m where
    midentity' :: Identity a -> m a
    mappend' :: (m <+> m) a -> m a

这令人厌恶

 midentity' :: a -> m a
 mappend' :: m (m a) -> m a

看起来熟悉？

Answer 2

定义"Monads只是endofunctors类别中的幺半群.",虽然这是一个不好的起点.这是一篇博客文章,主要是为了开个玩笑.但是如果你对这些函数感兴趣,它可以在Haskell中演示:

类别的外行描述是对象之间的对象和态射的抽象集合.类别之间的映射称为仿函数,将对象映射到对象,将态射映射到态射,并保留身份.endofunctor是一个类别到自身的仿函数.

{-# LANGUAGE MultiParamTypeClasses, 
             ConstraintKinds,
             FlexibleInstances,
             FlexibleContexts #-}

class Category c where
  id  :: c x x
  (.) :: c y z -> c x y -> c x z

class (Category c, Category d) => Functor c d t where
  fmap :: c a b -> d (t a) (t b)

type Endofunctor c f = Functor c c f

满足所谓自然条件的仿函数之间的映射称为自然变换.在Haskell中,这些是类型的多态函数:(Functor f, Functor g) => forall a. f a -> g a.

一个单子上一类C是三件事(T,?,?),T是endofunctor并且1是对身份的仿函数C.Mu和eta是两个满足三角形身份和相关性身份的自然变换,定义如下:

• ? : 1 ? T
• ? : T^2 ? T

在Haskell ?是join和?是return

• return :: Monad m => a -> m a
• join :: Monad m => m (m a) -> m a

可以写出Haskell中Monad的分类定义:

class (Endofunctor c t) => Monad c t where
  eta :: c a (t a)
  mu :: c (t (t a)) (t a)

bind运算符可以从这些派生出来.

(>>=) :: (Monad c t) => c a (t b) -> c (t a) (t b)
(>>=) f = mu . fmap f

这是一个完整的定义,但同样地,您也可以证明Monad定律可以表示为具有仿函数类别的 Monoid定律.我们可以构造这个仿函数类别,它是一个带有对象作为仿函数(即类别之间的映射)和自然变换(即仿函数之间的映射)作为态射的类别.在endofunctors类别中,所有仿函数都是同一类别之间的仿函数.

newtype CatFunctor c t a b = CatFunctor (c (t a) (t b))

我们可以证明这产生了一个带有函子组成的类别作为态射组成:

-- Note needs UndecidableInstances to typecheck
instance (Endofunctor c t) => Category (CatFunctor c t) where
  id = CatFunctor id
  (CatFunctor g) . (CatFunctor f) = CatFunctor (g . f)

幺半群有通常的定义:

class Monoid m where
  unit :: m
  mult :: m -> m -> m

关于一类仿函数的幺半群具有自然变换作为身份a和乘法运算,其结合了自然变换.可以定义Kleisli组成以满足乘法定律.

(<=<) :: (Monad c t) => c y (t z) -> c x (t y) -> c x (t z)
f <=< g = mu . fmap f . g 

所以你有它"Monads只是endofunctors类别中的幺半群",它只是来自endofunctors和(mu,eta)的monad的正常定义的"无点"版本.

instance (Monad c t) => Monoid (c a (t a)) where
  unit = eta
  mult = (<=<)

通过一点替换,我们可以证明(<=<)三角形的等值线性和monad自然变换的相关性图的等值线性质.

f <=< unit == f
unit <=< f == f

f <=< (g <=< h) == (f <=< g) <=< h

如果您对图解表示感兴趣,我已经写了一些关于用字符串图表示它们的内容.