延续作为有意义的理解

Mus*_*ssy 9 monads continuations haskell

Monads可以被解释为容器的形式:

  • list:给定类型的项目的聚合
  • bag:无序聚合
  • set:忽略多重性的无序聚合
  • 也许:最多一个项目的聚合
  • 读者e:基数的汇总| e |

我想知道如何在这个视图中以一种有意义的方式将continuation解释为包/容器的形式.谢谢!

jto*_*bin 8

我喜欢将延续视为带有漏洞的程序.我想我最初从Tekmo的博客中收集了这些见解.

看看这个小延续:

import Control.Monad.Trans.Cont

program :: ContT () IO Char
program = ContT $ \doThing -> do
  c <- getChar
  doThing c
Run Code Online (Sandbox Code Playgroud)

这是一个"缺少一块"的程序 - 即如何处理从中Char检索到的getChar.我们可以通过填充缺失的部分来运行它putChar; 评估continuation via runContT program putChar将得到一个字符,然后将其打印到stdout.

如果您对通过抽象语法树表示程序感到满意,那么容器类比可能是直观的.

为了更清楚,你可以建立一个包含一个DoThing代表一个需要填充的洞的术语的AST :

{-# LANGUAGE DeriveFunctor #-}

import Control.Monad.Free

data ExprF a =
    GetChar (Char -> a)
  | DoThing Char a
  deriving Functor

type Expr = Free ExprF

getChar' :: Expr Char
getChar' = liftF (GetChar id)

doThing' :: Char -> Expr ()
doThing' c = liftF (DoThing c ())

program' :: Expr ()
program' = do
  c <- getChar'
  doThing' c
Run Code Online (Sandbox Code Playgroud)

program'希望更清楚一个容器; 要运行它,我们需要以与任何其他递归容器类似的方式处理AST:

eval :: Expr () -> (Char -> IO ()) -> IO ()
eval prog f = iterM alg prog where
  alg (GetChar k)   = getChar >>= k
  alg (DoThing c k) = f c >> k
Run Code Online (Sandbox Code Playgroud)

评估program'via eval program' putChar类似于运行programvia runContT program putChar.


Cir*_*dec 6

理解monad的真正关键是停止尝试说

monad是X.

而是开始说

X是monad

如果它具有某种结构并遵守某些定律,那么它就是monad .出于在Haskell中编程的目的,Monad如果它具有正确的类型和类型并遵守Monad法则,那就是一个东西.

 return a >>= f ? f a
 m >>= return   ? m
(m >>= f) >>= g ? m >>= (\x -> f x >>= g)
Run Code Online (Sandbox Code Playgroud)

Gabriel Gonzales指出,monad法律是"伪装的范畴法".我们可以使用>=>,定义如下,而不是>>=.

(f >=> g) = \x -> f x >>= g
Run Code Online (Sandbox Code Playgroud)

当我们这样做时,monad法则成为具有同一性和联想构成的范畴法.return>=>

return >=> f    ? f
f >=> return    ? f
f >=> (g >=> h) ? (f >=> g) >=> h
Run Code Online (Sandbox Code Playgroud)

在你的例子中,你已经讨论了monad的两个不同的东西:一个扁平的聚合和一个修剪的聚合.我们不会试图说monad是这两件事,而是说这两件事都是monad.为了发展关于什么是monad的直觉,让我们来谈谈所有monad中最大的东西.

树木与嫁接

这是最大的一类Monads为与嫁接树和简化.这个类是如此之大,Monad以至于我在Haskell中所知道的每一个都是一棵嫁接的树.这些monad中的每一个都包括一个return构造一个树的树,一个树在叶子上保存值,一个绑定>>=做两件事.Bind用新树替换每个叶子,将新树移植到叶子所在的树上,并简化得到的树.您提到的示例在简化树的方式上有所不同.允许哪些简化受Monad法律管辖.

如果我们有一个简单的树在其叶子上保持值,那么它就是一个monad.

data Tree a = Branch [Tree a] | Leaf a
Run Code Online (Sandbox Code Playgroud)

它的return构造单一Leaf.这是return 1:

          1
Run Code Online (Sandbox Code Playgroud)

它的绑定用整棵树代替树叶.我们从以下树开始:

          *
         / \
        0   1
Run Code Online (Sandbox Code Playgroud)

并绑定它\x -> Branch [x*2, x*2 + 1].我们用新计算的树替换每个叶子.

        __*__
       /     \
      *       *
     / \     / \
    0   1   2   3
Run Code Online (Sandbox Code Playgroud)

对于普通树木,嫁接步骤不进行任何简化.在检查这些操作是否符合我们可以说的monad定律之后

嫁接树和没有简化的树是monad

弄平

列出,包装,设置,Maybe并将Identity生成的树的所有级别展平为单个级别.在树上任何地方嫁接的所有东西都会在同一个列表或包中或集合中Just.集合还会从生成的单层树中删除任何重复项.

          *
         / \
       [0,  1]
Run Code Online (Sandbox Code Playgroud)

如果我们绑定它,\x -> [x*2, x*2 + 1]我们用新树替换每个叶子

        __*__
       /     \
      *       *
     / \     / \
   [0,  1] [2,  3]
Run Code Online (Sandbox Code Playgroud)

然后压平中间层

      ____*____
     /  |   |  \
   [0,  1,  2,  3]
Run Code Online (Sandbox Code Playgroud)

我们可以这么说

平坦化的聚合是具有嫁接和简化的树

并且,在检查了monad法则之后我们可以这么说

扁平化的聚合是monad

修剪

Reader e和双方一样data Pair a = Pair a a有点不同.它们不能将所有结果压平成单个层,或者至少不能立即这样做.相反,他们修剪不与父母分支相同方向的分支.

如果我们从一对开始

          *
         / \
       <0,  1>
Run Code Online (Sandbox Code Playgroud)

当我们绑定它时,\x -> <x*2, x*2 + 1>我们用新树替换每个叶子

        __*__
       /     \
      *       *
     / \     / \
   <0,  1> <2,  3>
Run Code Online (Sandbox Code Playgroud)

我们修剪那些没有分支同一方向的分支

        __*__
       /     \
      *       *
     /         \
   <0,          3>
Run Code Online (Sandbox Code Playgroud)

然后可以通过展平图层来进一步简化这一过程

          *
         / \
       <0,  3>
Run Code Online (Sandbox Code Playgroud)

正如您所指出的,Reader e a分支的方向数等于可能值的数量e.

我们可以这么说

修剪和压平的聚合是具有嫁接和简化的树

并且,在检查了monad法则之后我们可以这么说

修剪和变平的聚合是monad

延续

在延续单子是对每个可能的分支树延续.我们将采用Philip JF建议的延续术语.在延续单子是整个(a -> r) -> r.的延续是a -> r通过在作为第一个参数功能

--                               continuation                                 
--                               |------|            
data Cont r a = Cont {runCont :: (a -> r) -> r}
--                               |-----------|
--                               continuation monad
Run Code Online (Sandbox Code Playgroud)

continuation monad有许多分支等于|r| ^ |a|,continuation的可能值的数量a -> r.每个分支都标有相应的功能.延续总是在每个叶子中保持相同的值,我们稍后会证明这一点.我们还将向树的内部节点添加标签r -> r,这是一个函数,稍后我将对此进行讨论.

我们将使用以下数据类型来编写示例树.

data Tri = A | B | C
Run Code Online (Sandbox Code Playgroud)

我们的示例树将用于return A :: Cont Bool Tri.树中保存的值的类型Tri有三个构造函数,而控制monad的结果Bool有两个构造函数.有2 ^ 3 = 8可能的功能Tri -> Bool,每个功能构成树的一个分支.

                               id *
      ____________________________|____________________________
false |     a |     b |     c |  aOrB |  aOrC |  bOrC |  true |
      A       A       A       A       A       A       A       A
Run Code Online (Sandbox Code Playgroud)

"通往Monad的心脏的方式是通过它的Kleisli箭头".Kleisli箭头是你可以传递到第二个参数的东西>>=; 他们有类型a -> m b.我们将研究Kleisli箭头Cont的类型a -> Cont r b,或者,当我们浏览Cont构造函数时

a -> (b -> r) -> r
Run Code Online (Sandbox Code Playgroud)

我们可以将契约monad的Kleisli箭头a -> (b -> r) -> r分成两部分.第一部分是决定b传递给延续的内容的函数b -> r.它唯一需要处理的是a参数,因此它必须是其中一个函数 g :: a -> b.第二部分是结合结果的功能.它可以看到参数a和传递g a到延续的结果.我们将称之为第二个功能r :: a -> r -> r.所有类型的函数a -> (b -> r) -> r都可以写在表单中

a  -> (b -> r) -> r
\x -> \f       -> r x (f (g x))
Run Code Online (Sandbox Code Playgroud)

一些g :: a -> b和r :: a -> r -> r.

类似地,每个延续monad (a -> r) -> r都可以写在表单中

(a -> r) -> r
\f       -> r (f a)
Run Code Online (Sandbox Code Playgroud)

一些a :: a和r :: r -> r.这些组合起来构成了一个继续monad总是在每一片叶子中保持相同价值的理由.

当我们将一个函数绑定\x -> \f -> r x (f (g x))到一个continuation monad树时,我们将记录g x为新的叶子并记录(r x, g x)为新的中间节点的标签.树木真的很大,但我们将使用只有两个构造函数的\x -> \f -> r x (f (g x)) :: Tri -> (Bit -> Bool) -> Bool地方绘制另一个完整示例的角落Bit.由此产生的延续monad应该只有|Bool| ^ |Bit| = 4分支,但我们还没有简化它.

                                            id *  
                _______________________________|_...
          false |                         a |
            r A *                       r A *
       _________|____________          _____|_...
bfalse |  b0 |  b1 |  btrue |   bfalse |  b0 |  
      g A   g A   g A      g A        g A   g A
Run Code Online (Sandbox Code Playgroud)

由于每个叶子保持相同的值,因此通过树的路径之间的唯一差异是标记每个分支的函数.我们将从分支中删除标签,只绘制一个分支.我们的第一个例子return a现在将被绘制为

        id *
           |
           A
Run Code Online (Sandbox Code Playgroud)

并且绑定\x -> \f -> r x (f (g x))到的示例return A将被绘制为

        id *
           |
       r A *
           |
          g A
Run Code Online (Sandbox Code Playgroud)

任何延续单子书面形式\f -> r (f a)对一些a :: a并r :: r -> r会由树表示

         r *
           |
           a
Run Code Online (Sandbox Code Playgroud)

绑定时\x -> \f' -> r' x (f' (g' x)),它将由以下树表示(这只是嫁接)

           r *
             |
        r' a *
             |
           g' a
Run Code Online (Sandbox Code Playgroud)

我们将从for的定义中>>=Cont弄清楚简化步骤是什么.

m >>= k = Cont $ \ c -> runCont m (\x -> runCont (k x) c)

(\f -> r (f a)) >>= (\x' -> \f' -> r' x' (f' (g' x')))
= \c -> (\f -> r (f a)) (\x -> (\x' -> \f' -> r' x' (f' (g' x'))) x c) -- by definition
= \c -> (\f -> r (f a)) (\x -> (       \f' -> r' x  (f' (g' x )))   c) -- beta reduction
= \c -> (\f -> r (f a)) (\x ->                r' x  (c  (g' x ))     ) -- beta reduction
= \c ->        r ((\x -> r' x  (c  (g' x))) a) -- beta reduction
= \c ->        r (       r' a  (c  (g' a))   ) -- beta reduction
= \c ->       (r .       r' a) (c  (g' a))     -- f (g x) = (f . g) x
= \c -> (r . r' a) (c (g' a))                  -- whitespace
Run Code Online (Sandbox Code Playgroud)

这是形式\f -> r (f a).我们的树将简化为

    r . r' a *
             |
           g' a
Run Code Online (Sandbox Code Playgroud)

continuation monad是一个树,其内部节点用函数标记.它的绑定操作是树移植,然后是简化步骤.简化步骤组成内部节点上的功能.我们可以这么说

延续monad是一棵嫁接和简化的树

并且,在检查了monad法则之后我们可以这么说

延续monad是monad