什么monad可以表示为free over some functor?

Pet*_*lák 26 monads haskell functor free-monad

对文件Free说:

许多常见的单子出现为免费单子,

  • 鉴于data Empty a,Free EmptyIdentitymonad 同构.
  • Free Maybe可用于建模偏好monad,其中每个图层表示运行计算的时间更长.

还有哪些monad可以使用Free

我只想到一个:我相信Free (Const e)是同构的Either e.

编辑:哪些monad 不能用于表达Free?为什么?

Phi*_* JF 29

几乎所有这些(直到涉及循环的问题mfix),但没有Cont.

考虑一下Statemonad

newtype State s a = State (s -> (a,s))
Run Code Online (Sandbox Code Playgroud)

不看任何东西像一个免费的单子......不过仔细想想State来讲你如何使用它

get :: m s --or equivalently (s -> m a) -> m a
set :: s -> m () --or (s,m a) -> m a
runState :: m a -> s -> (a,s)
Run Code Online (Sandbox Code Playgroud)

我们可以通过将操作列为构造函数来设计具有此接口的免费monad

data StateF s a
  = Get (s -> a) | Set s a deriving Functor
Run Code Online (Sandbox Code Playgroud)

然后我们有

type State s a = Free (StateF s) a
Run Code Online (Sandbox Code Playgroud)

get = Impure (Get Pure)
set x = Impure (Set x (Pure ())
Run Code Online (Sandbox Code Playgroud)

我们只需要一种方法来使用它

runState (Pure a) s = (a,s)
runState (Impure (Get f)) s = runState (f s) s
runState (Impure (Set s next)) _ = runState next s
Run Code Online (Sandbox Code Playgroud)

你可以用大多数monad做这个结构.就像may/partiality monad一样

stop :: m a
maybe :: b -> (a -> b) -> m a -> b
Run Code Online (Sandbox Code Playgroud)

规则是,我们对待每一个为此在功能m x对于一些x作为函子构造,以及其他功能都运行产生的游离单子的方式.在这种情况下

data StopF a = StopF deriving Functor

maybe _ f (Pure a)      = f a
maybe b _ (Impure Stop) = b
Run Code Online (Sandbox Code Playgroud)

为什么这很酷?好吧,有些事情

  1. 免费monad为您提供了一段数据,您可以将其视为monadic代码的AST.您可以编写对此数据进行操作的函数,这对DSL非常有用
  2. Functors组成,这意味着分解你的monad就像这样使它们半可组合.特别是,给定两个共享代数的函子(代数实际上只是函数f a -> a,af一个函数是函数时),组合也有代数.

Functor组合就是我们可以用几种方式组合仿函数,其中大部分都保留了代数.在这种情况下,我们不需要仿函数组合,(f (g (x)))而是仿函数副产品.函数添加

data f :+: g a = Inl (f a) | Inr (g a) 

instance (Functor f, Functor g) => Functor (f :+: g) where
  fmap f (Inl x) = Inl (fmap f x)
  fmap f (Inr x) = Inr (fmap f x)

compAlg :: (f a -> a) -> (g a -> a) -> f :+: g a -> a
compAlg f _ (Inl x) = f x
compAlf _ g (Inr x) = g x
Run Code Online (Sandbox Code Playgroud)

也免费monad保存代数

freeAlg :: (f a -> a) -> Free f a -> a
freeAlg _ (Pure a) = a
freeAlg f (Impure x) = f $ fmap (freeAlg f) x
Run Code Online (Sandbox Code Playgroud)

在Wouter Swierstra的着名论文数据类型A La Carte中,这被用于产生巨大的效果.该论文的一个简单例子是计算器.我们将对这篇文章采用monadic take new.鉴于代数

class Calculator f where
 eval :: f Integer -> Integer
Run Code Online (Sandbox Code Playgroud)

我们可以想到各种情况

data Mult a = Mult a a deriving Functor
instance Calculator Mult where
  eval (Mult a b) = a*b

data Add a = Add a a deriving Functor
instance Calculator Add where
  eval (Add a b) = a+b

data Neg a = Neg a deriving Functor
instance Calculator Neg where
  eval (Neg a) = negate a

instance Calculator (Const Integer) where
  eval (Const a) = a

data Signum a = Signum a deriving Functor
instance Calculator Signum where
  eval (Signum a) = signum a

data Abs a = Abs a deriving Functor
instance Calculator Abs where
  eval (Abs a) = abs a
Run Code Online (Sandbox Code Playgroud)

而且最重要的

instance (Calculator f, Calculator g) => Calculator (f :+: g) where
   eval = compAlg eval
Run Code Online (Sandbox Code Playgroud)

你可以定义数字monad

newtype Numerical a = Numerical (
        Free (Mult 
        :+: Add 
        :+: Neg 
        :+: Const Integer 
        :+: Signum
        :+: Abs) a deriving (Functor, Monad)
Run Code Online (Sandbox Code Playgroud)

然后你可以定义

 instance Num (Numerical a)
Run Code Online (Sandbox Code Playgroud)

这可能完全没用,但我觉得很酷.它确实让你定义其​​他东西

 class Pretty f where
    pretty :: f String -> String

 instance Pretty Mult where
    pretty (Mult a b) = a ++ "*" ++ b
Run Code Online (Sandbox Code Playgroud)

和其他所有人类似.

这是一个有用的设计策略:列出你希望monad做的事情==>为每个操作定义仿函数==>弄清楚它的一些代数应该==>为每个操作定义那些仿函数==> make it快速.

快速进行很难,但我们有一些技巧.诀窍1是将你的免费monad包裹起来Codensity("更快的按钮"),但是当这不起作用你想要摆脱自由表示.记得我们什么时候

runState (Pure a) s = (a,s)
runState (Impure (Get f)) s = runState (f s) s
runState (Impure (Set s next)) _ = runState next s
Run Code Online (Sandbox Code Playgroud)

好吧,这是一个函数Free StateF a,s -> (a,s)只是使用结果类型,因为我们对状态的定义似乎是合理的......但是我们如何定义操作呢?在这种情况下,你知道答案,但推导它的一种方法是根据Conal Elliott所谓的类型态射来考虑.你要

runState (return a) = return a
runState (x >>= f) = (runState x) >>= (runState f)
runState (set x) = set x
runState get = get
Run Code Online (Sandbox Code Playgroud)

这让它很容易

runState (return a) = (Pure a) = \s -> (a,s)

runState (set x) 
   = runState (Impure (Set x (Pure ()))) 
   = \_ -> runState (Pure ()) x
   = \_ -> (\s -> (a,s)) x
   = \_ -> (a,x)

runState get
  = runState (Impure (Get Pure))
  = \s -> runState (Pure s) s
  = \s -> (s,s)
Run Code Online (Sandbox Code Playgroud)

这非常有帮助.>>=以这种方式衍生可能很难,我不会在这里包括它,但其他的正是你期望的定义.

  • +1,但是`:.:`应该是`:+:` - 你所拥有的是functor coproduct,组合看起来像`newtype(f:.:g)x = C(f(gx))`. (8认同)
  • 我喜欢"Impure",因为它只不过是"它是其他构造函数不是'纯'." :) (4认同)

Rei*_*ton 8

要回答这个问题,你在问题中没有提到的大多数熟悉的单子都不是自由的单子.菲利普JF的回答暗示你如何将一个给定的monad与一个新的,自由的monad相关联,但是新monad将会"更大":它具有比原始monad更明显的价值.例如真正的State smonad满足get >>= put = return (),但免费monad on StateF不.作为一个自由的monad,它不能满足额外的方程式; 这就是自由的概念.

我将表明Reader r,Writer wState s单子都没有,除了在特殊条件下自由r/ w/ s.

我来介绍一些术语.如果m是monad,那么我们将类型m a的任何值称为(m- )动作.m如果它对return x某些人来说是平等的,我们称之为- 作用是微不足道的x; 否则我们称之为不平凡.

如果m = Free f是一个仿函数上的任何免费monad f,那么m承认monad同态Maybe.这是因为,Free是在它的参数函子fMaybe = Free (Const ())其中Const ()是在函子的类别相关的终端对象.具体地说,可以写出这种同态

toMaybe :: Free f a -> Maybe a
toMaybe (Pure a) = Just a
toMaybe (Impure _) = Nothing
Run Code Online (Sandbox Code Playgroud)

因为toMaybe是monad同态,它特别满足toMaybe (v >> w) = toMaybe v >> toMaybe w任何m- v和 - 和w.现在观察一下,toMaybe将琐碎的m行为发送到琐碎的Maybe行为和非m平凡的Maybe行动到非平凡的行动Nothing.现在Maybe有一个属性,即>>以任何顺序执行任何动作的非平凡动作都会产生一个非常重要的动作(Nothing >> w = v >> Nothing = Nothing); 所以同样如此m,因为toMaybe是monad同态,保留(非)平凡.

(如果您愿意,您也可以直接从公式中>>为免费monad 验证这一点.)

为了表明一个特定的monad m不与任何自由monad同构,那么,它就足以找到m- v并且w至少有一个v并且w不是微不足道的,而是v >> w微不足道的.

Reader r满足v >> w = w,所以我们只需要选择w = return ()和任何非常重要的行动v,只要r至少有两个值(然后ask是非常数,即非平凡)就存在.

因为Writer w,假设k :: w除了身份之外还有一个可逆元素.让它kinv :: w反过来.然后tell k >> tell kinv = return (),但是tell k并且tell kinv非常重要.任何非平凡的组(例如,加法中的整数)都有这样的元素k.我认为形式的自由单子Writer w只是幺半群w本身自由的那些,即w = [a],Writer w ~ Free ((,) a).

因为State s,类似地,如果s允许任何非平凡的自同构f :: s -> s与逆finv :: s -> s,那么modify f >> modify finv = return ().s具有至少两个元素和可判定的相等性的任何类型都具有这样的自同构.


Ing*_*idt 5

根据里德回答中的见解,我写了一份证明,证明列表 monad 在发布到 haskell-cafe 邮件列表时不是免费的:

回想一下,我们可以为任何函子 f 构造 f 上的自由单子:

data Free f a = Pure a | Roll (f (Free f a))
Run Code Online (Sandbox Code Playgroud)

直观上,Free fa 是一种叶子为 a 型的 f 型树。连接操作只是将树嫁接在一起,不执行任何进一步的计算。在此发布中,形式 (Roll _) 的值应称为“非平凡”。

一些常见的 monad 实际上是一些 functor 上的自由 monad:

  • 树单子是函子上的自由单子Pair,其中 data Pair a = MkPair a a。在这个例子中,对形树的直觉是最强烈的。每个父节点都有一对子节点。

  • Maybe monad 是 functor 之上的自由 monad Unit,其中 data Unit a = MkUnit. 在图形图片中父节点有一个 Unit孩子,所以根本没有孩子。因此正好有两种 Unit形状的树:仅由叶子组成的树(对应于Just _)和由无子父节点组成的三棵树(对应于Nothing)。

  • Identity单子是在函子自由单子Void,其中Void a是没有构造一个类型。

  • Partiality单子是在免费的单子Maybe

  • Writer [r]单子是在仿免费单子(r,)。在(r,)形状树中,父节点用类型值修饰,r并且正好有一个子节点。遍历这样的路径会产生一个r's的列表和一个 type 的叶值a,所以总共有一个 type 的值([r],a) = Writer r a

    (特别是,Free (r,) ()与 同构[r]。这个观察导致了列表 monad 是自由的断言。但是这个断言是错误的,并且确实不是从观察中得出的。为了证明一个单子m 是自由的,一个人必须展示一个单子forall a. m a -> Free f a 某些函子的同构f。相比之下,展示m awith 的同构Free (f a) ()既不充分也不必需。)

更多的单子是自由单子的商。例如,State s是 的商Free (StateF s),其中

data StateF s a = Put s a | Get (s -> a).
-- NB: This functor is itself a free functor over a type constructor
-- which is sometimes called StateI [1], rendering Free (StateF s) what
-- Oleg and Hiromi Ishii call a "freer monad" [2].
Run Code Online (Sandbox Code Playgroud)

商由以下 monad 态射展示,它为自由 monad 的纯句法值提供语义。

run :: Free (StateF s) a -> State s a
run (Pure x)         = return x
run (Roll (Put s m)) = put s >> run m
run (Roll (Get k))   = get >>= run . k
Run Code Online (Sandbox Code Playgroud)

这个观点是 apfelmus [1] 的操作包的基础,在 StackOverflow 线程 [3] 中也有谈到。这是免费 monad 在编程环境中有用的主要原因。

那么,列表 monad 是一个免费的 monad 吗?直觉上,事实并非如此,因为列表 monad(连接)的连接操作不仅将表达式嫁接在一起,而且将它们扁平化 [4]。

这里证明了列表 monad 不是免费的。我正在记录它,因为我对证明感兴趣已经有一段时间了,但是搜索它没有产生任何结果。不过,线程 [3] 和 [5] 很接近。

在任意函子上的自由 monad 中,将非平凡动作与任何函数绑定的结果总是非平凡的,即

(Roll _ >>= _) = Roll _
Run Code Online (Sandbox Code Playgroud)

这可以直接从(>>=)for the free monad的定义中检查,或者使用 Reid Barton 的利用 monad 态射到 Maybe 的技巧进行检查,参见 [3]。

如果列表 monad 与某个函子上的自由 monad 同构为单子,则同构只会将单例列表映射[x]到形式的值,(Pure _)而将所有其他列表映射到非平凡的值。这是因为单子同构来来回回与“回报”,并return x[x]在列表单子,并Pure x在免费的单子。

这两个事实相互矛盾,如以下示例所示:

do
    b <- [False,True]  -- not of the form (return _)
    if b
        then return 47
        else []
-- The result is the singleton list [47], so of the form (return _).
Run Code Online (Sandbox Code Playgroud)

在对某个函子上的自由 monad 应用一个假设的同构之后,我们将得到一个非平凡值([False,True]同构下的的图像)与某个函数的绑定导致一个平凡的值( 的图像[47],即return 47)。

干杯,英戈

[1] http://projects.haskell.org/operational/Documentation.html

[2] http://okmij.org/ftp/Haskell/extensible/more.pdf

[3]哪些 monad 可以在某些函子上表示为 Free?

[4] https://hackage.haskell.org/package/free-4.12.4/docs/Control-Monad-Free.html

[5] https://www.reddit.com/r/haskell/comments/50zvyb/why_is_liststate_not_a_free_monad/