Free 与 Freer Monad,将 Monad 放回柜橱

译自 Free and Freer Monads: Put Monad Back into Closet 简介 编写 Monad(现在还包括 Applicative 和 Functor)的实例,并确保实例符合 Monad 定律不但是定义 Monad 的重要部分,同时也是数量正在以指数级膨胀的「Monad 教程」的重要部分。而本文认为所有这些实例都不过是 boilerplate--可以避免的 boilerplate!或许是因为听起来像拉丁语的名字和其引起的人们对顶尖数学的兴趣,这些琐碎的 boilerplate,琐碎的 Monad 定律,毫无新意的「管道」吸引了过多的关注。如果我们能直接思考副作用本身而非这些管道的工作原理,难道不让人耳目一新吗? Free Monad,以及我们正要提到的 Freer Monad 将把我们从 boilerplate 中解放出来,从而专注于副作用的本质。有了它,我们就可以将解释器这一在编程语言研究和实践中的大杀器引入到副作用编程中--为副作用定义解释器。 目前,已经有了许多关于 Free Monad 的精彩解释,这些解释往往援引了幺半群、普适代数和范畴论的观点。但最近流行的 Freer Monad 却给我们带来了困境:它的定位是什么?它能让我们更清晰地思考副作用吗?它也是『自由』的吗?如果是,为什么这些数学上的解释都没有预言 Freer Monad 的存在呢?本文接下来将解决这些问题,但唯独最后一个问题,我只能说,人们几次发现 Free Monad 都不是通过范畴论。(事后来看,范畴论上的联系确实存在,而且确实有洞见性)。与许多已有的解释不同,本文采取了通俗的方法,通过具体的例子而非抽象的代数解释 Free Monad(有关范畴论的内容将仅在括号中提及)。 经典 Monad 我们用耳熟能详的 State Monad 举例,该 Monad 代表『访问或更新一个可变状态』的副作用。常见的实现将这个可变状态作为返回值和参数沿着程序传递,然后通过 get 和 put 两个原语来获取/更新变量。 newtype State s a = State{unState :: s -> (a,s)} get :: State s s get = State $ \s -> (s,s) put :: s -> State s () put s = State $ \_ -> ((),s) runState :: State s a -> s -> (a,s) runState = unState get 和 put 操作,State s 蕴涵的定律以及解释器 runState,没有这三者,State s 就不能够作为真正的可变状态副作用计算使用。然而,为了在 Haskell 程序中方便地使用这些操作,我们要编写以下代码。...

February 29, 2024 · 阅卜录 · Public Domain

Monadic的作用管理

大多数情况下,effect都是用Hoare逻辑来描述的。一个Hoare三元组$\{p\}\;S\;\{q\} $, $S$ 是一段程序, $p $ 是执行这段程序的前提条件(状态), $q$ 是执行完这段程序后的条件(状态)。然后使用这个三元组的一些规则表示语句的一些性质: 空语句: $\frac {} {\{p\}\;skip\;\{p\}}$ 赋值语句: $\frac {} {\{p[u :=t]\}\;u:=t\;\{p\}}$ 顺序语句: $\frac {\{p\}\;S_1\;\{q\}, \{q\}\;S_2\;\{r\}} {\{p\}\;S_1;\,S_2\;\{r\}}$ 等等。这其实恰好是个幺半群——空语句是幺元,顺序语句是乘法。总之,用幺半群来描述作用(语句)是十分合适的。 于是用Monad来描述作用也是很自然的——Monad是自函子范畴上的幺半群。(这句话我就不解释了) 比如用m a表示带作用类型为m的程序,而m (m (m ... m a))表示一系列的作用,对应作用(语句)序列 $S_1, S_2, S_3, S_4 \dots S_n$ : stms :: Monad m => m (m (m (m ... m a))) -- ^ ^ ^ ^ ^ -- | | | | ... | -- S1 S2 S3 S4... Sn stms = ....

February 27, 2021 · 脚趾头 · 转自知乎