Mus*_*ssy 9 monads continuations haskell
Monads可以被解释为容器的形式:
我想知道如何在这个视图中以一种有意义的方式将continuation解释为包/容器的形式.谢谢!
我喜欢将延续视为带有漏洞的程序.我想我最初从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.
理解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
| 归档时间: |
|
| 查看次数: |
159 次 |
| 最近记录: |