thoughts of hsfzxjy

二月十一日杂感

学生时代的我很怕父亲检查我的作文。四年级以前还没有真正意义的作文一说,因此这大概是从四年级开始的,一直持续到高中。父亲是学文的,在单位也常有写报告的工作。修改作文可以说是比较拿手。现在回想起来,父亲指导作文时还算温和,遇到写得不好的地方也不会破口大骂,只是表情比较严肃。但每当这个时候,我都会感到莫名的畏惧,就像是手无寸铁地撞上一个巨人。为此我会努力减少这种机会,时不时谎称没有布置作文作业,或是隐瞒语文测验。

我是慑于父亲的威严吗?不完全是。我更多地是不想将自己的不完美暴露在父亲面前。在写作这方面,我一直都无法超越父亲。当然这是一种很正常的心理,父亲也不会因为我的不完美而对我不利。尽管如此,我还是对这种事十分敏感。仔细想想,这样的情况还出现在我生活的其它方面。我会因此刻意隐瞒病情,压制心中的迷茫。除非是再三确认过交流过程不会暴露自己的缺陷,我不会轻易和父亲谈话。

我不知是自己天生性格使然,还是因小时候某个「导火索」事件所致。在其他人面前,我也或多或少会有类似的倾向,但这也有可能是因与父亲的关系而起的。小时候父亲总是很忙,有时甚至会长时间到另一个城市去工作。若要追究这种现象背后的原因,我想,这段经历要承担大部分的责任。

当然这不是父亲的错,为了生存,面对两难作出的选择,总会留下一些遗憾的。

一月二十六日杂感

小姑躺在床上,脸色苍白。一根管子从胸口伸出来,随着呼吸剧烈起伏着。长长的管子在床下绕了一圈,接上了一个白色塑料桶,里面尽是浑浊的黄色液体。病床对面坐着阿伯,一脸忧愁的样子。

我顿时感到有些难过——但也仅此而已。这感觉像是一种怜悯,却不是因为血缘,而是来自本性深处,对病危的同物种的怜悯。换句话说,如果躺在面前的是一个素未谋面的人,我的怜悯不会因此减少半分。这么说很残忍,但确实是我内心的真实写照。这种想法当然没有向任何人透露过,可在自己的博客我不想隐瞒这一点。

我身后有一个庞大的家族,但我时刻都想着和他们切断联系。这种想法来源已久了,或许是受到母亲的影响。母亲时常叨念家乡的事,这个人的小心眼,那个人的不作为。但由于外婆依旧健在,母亲还是保持着较高的探亲频率。说是探亲,不过也是周末偶尔回去住个两天,便匆匆回来了。四百公里的路,火车跑起来快得很。

我所不喜欢的,是老家那种到处是熟人的氛围。在那个小镇子上生活的人们从几代以前就互相认识了,出门走几步遇到的人大都能叫出你的名字。熟人社会有着他们自己认为的优点,办事方便,有困难时可以相互扶持。但在我看来这种关系状态是一种束缚。「熟人」们的指指点点会限制你的行为,即使你的行为并没有什么问题。如果将熟人社会看做一个整体,这个庞然大物的思想进步是非常缓慢的。社会中的人相互牵制,根深蒂固的观念不断同化着想要脱离的人。封闭而保守,也许有人喜欢那种状态,反正我是不喜欢的。

亲人又怎么样呢?如果不是经常见面,相互没有过印象深刻的经历,不过也是「熟人」罢了。血缘这种东西,粗暴地将一个人与另一个人捆绑在一起,物质上或许有一些牵连,但精神关系的认同仍然得看彼此的共同经历。自小我便和父母在另一个城市生活,除了曾经照顾过我的,家族中的许多人,同辈或是不同辈的,对于我都只是「熟人」。但遗憾的是,我常常需要回到这些「熟人」当中,有时甚至需要过多地流露一些感情,让我感到如坐针毡。而这一切,只因为我们有「血缘关系」。

有人说,计划生育和网络的崛起让我们这一代变得孤独而冷酷。但我觉得,如果孤独和冷酷不影响我们在现代社会生活的话,倒也无可厚非。熟人的相互关心也罢,沉迷于网络中的光怪陆离也罢,都是为了使精神不空虚,这是一个人活下去的必要条件。过去的人们没有过多的方式解决这个问题,但现在有了,我们应该有权利依自己的意志去选择。我们已经过了几千年的熟人/家族式社会,但不意味着这是常态。二三十年前的文学作品描绘了一个个乡土社会,它们透着幸福的气息,却不能使我产生憧憬。科技在瓦解旧的人际关系和社会结构,在此之前生活的人或许会感到痛惜,但在此之后的人只会无感甚至欣喜。我想,之前许多时代的接口处都会有这样的阵痛。

我盼望着,能尽早告别这一切。

TaPL Notes -- Chapter 3 Untyped Arithmetic Expressions

This chapter develop a small language of numbers and booleans, serving as a straightforward vehicle for the introduction of serveral fundamental concepts like, abstract syntax tree, evaluation and runtime errors.

Syntax

BNF-like Definition

Terms of this language are defined as below:

1
2
3
4
5
6
7
8
t ::=
true
false
if t then t else t
0
succ t
pred t
iszero t

where t is called meta-variable. At every point where the symbol t appears, we may substitute any terms.

Inductive Definition

The set of terms is the smallest set $T$ s.t.

  1. $\{0, true, false\} \subseteq T$
  2. if $t_1 \in T$, then ${succ\ t_1, pred\ t_1, iszero\ t_1} \subseteq T$
  3. if $t_1, t_2, t_3 \in T$, then $if\ t_1\ then\ t_2\ else\ t_3 \in T$

Concrete Definition

For each natural number $i$, define a set $S_i$ as follows:

  • $S_0 = \phi$
  • $S_{i+1} = \{0, true, false\} \cup \{succ\ t_1, pred\ t_1, iszero\ t_1 | t_1 \in S_i\} \cup \{if\ t_1\ then\ t_2\ else\ t_3 | t_j \in S_i\}$
  • $S = \cup_i S_i$

Three definition above are equivalent.

Semantics

The semantics of an language is how its terms are evaluated. Three approaches had been proposed to formalize semantics:

  • Operational Semantics (used here) specifies the behavior of a programming language by defining a simple abstract machine for it. This machine is “abstract” in the sense that it uses the terms of the language as its machine code, rather than some low-level microprocessor instruction set. For simple languages, a state of the machine is just a term, and the machine’s behavior is defined by a straition function that for each state, either gives the next state, or declares that the machine has halted. (字节码语义,Compare with languages like Python or Java)
  • Denotational Semantics. The meaning of a term is taken to be some mathematical object, instead of a sequence of machine states. Giving denotational semantics for a language consists of finding a collection of semantic domains and then defining an interpretation function mapping terms into elements of these domains.
  • Axiomatic semantics (omitted)

Semantics with only Booleans

Firstly we consider a simpler situation where only booleans get involved.

The evaluation process can be summarized as three rules:

1
2
3
if true then t2 else t3 -> t2 [E-IFTRUE]
if false then t2 else t3 -> t3 [E-IFFALSE]
t1 -> t1' || if t1 then t2 else t3 -> if t1' else t2 then t3 [E-IF]

A rule consists of one conclusion and zero or more premises. For example, in rule E-IF, t1 -> t1' is the premise and if t1 then t2 else t3 -> if t1' else t2 then t3 the conclusion.

Note that in textbook premises are written above conclusion with a horizontal line in the middle, but here I use a notation that is more convenient to type in.

A subset of terms should be defined as possible final results of evaluation, which are called values. Here they are just the constants true, false, 0.

Note that $\rightarrow$ can be viewed as a binary relation over $T$, i.e., a subset of $T \times T$.

The third rule E-IF specifies the evaluation order of an expression, i.e., clauses are always evaluated after their guards.

DEFINITION instance of an inference rule An instance of an inference rule is obtained by consistently replacing each metavariable by the same term in the rule’s conclusion and all its premises (if any). e.g., if true then true else (if false then false else false) -> true is an instance if E-IFTRUE.

DEFINITION satisfy A rule is satisfied by a relation if, for each instance of the rule, either the conclusion is in the relation or one of the premises is not (to ensure evaluation can proceed).

DEFINITION one-step evaluation relation denoted as $\rightarrow$, is the smallest binary relation on terms satisfying the three rules. When the pair (t, t') is in the relation, we say that t -> t' is derivable. (“smallest” implies that t -> t' is derivable iff it is justified by the rules).

DEFINITION normal form A term $t$ is in normal form if no evaluation rule applies to it.

Facts:

  • Every value is in normal form.
  • When only booleans involved, every term in normal form is a value.
  • Every term can be evaluated in values.

Semantics with Booleans and Numbers

Now we let numbers in. Several new rules should be added:

1
2
3
4
5
6
7
t1 -> t1' || succ t1 -> succ t1' [E-SUCC]
pred 0 -> 0 [E-PREDZERO]
pred (succ nv1) -> nv1 [E_PREDSUCC]
t1 -> t1' || pred t1 -> pred t1' [E-PRED]
iszero 0 -> true [E-ISZERO]
iszero (succ nv1) -> false [E-ISZEROSUCC]
t1 -> t1' || iszero t1 -> iszero t1'[E-ISZERO]

and new values:

1
2
3
4
5
6
7
v ::=
...
nv
nv ::=
0
succ nv # positive integer

DEFINITION stuck term A closed term is stuck if it is in normal form but not a value. e.g. if 0 then true else true or iszero false.

Stuckness gives us a simple notion of run-time error for this simple machine. Intuitively, it characterizes the situation where the operational semantics does not know what to do because the program has reached a “meaningless state”.

Stuckness can be prevented by introducing a new term called $wrong$ and augment the opereational semantics with rules that explicitly generate $wrong$ ain all the situations where the present semantics gets stuck.

Evaluation Theorems

If $t \rightarrow t1$ and $t \rightarrow t2$, then $t1 = t2$. (Can be proved by performing induction on the structure of t)

Other Forms of Evaluation Relation

DEFINITION mutli-step evaluation $\rightarrow^*$ is the reflexive, transitive closure of one-step evaluation.

If $t \rightarrow^\star t1$ and $t \rightarrow^\star t2$, where $t1$ and $t2$ are in normal form, then $t1 = t2$.

For every term $t$ there is some normal form $t’$ s.t. $t \rightarrow^\star t’$.

DEFINITION big-step evaluation (omitted) formulates the notion of “this term evaluates to that final value”.

SS Configuration

SS Client

1
$ [sudo] pip3 install shadowsocks

/etc/ss.json:

1
2
3
4
5
6
7
8
9
10
{
"server": "<server ip>",
"server_port": "<server port>", // must be Number
"password": "<password>",
"local_address":"127.0.0.1",
"local_port":1081,
"timeout":300,
"method":"aes-256-cfb",
"fast_open":false
}
1
$ [sudo] sslocal -c /etc/ss.json -d start

proxychains

clone repository from https://github.com/rofl0r/proxychains-ng, make && sudo make install.

Append following lines to /etc/proxychains.conf:

1
2
3
4
5
[ProxyList]
# add proxy here ...
# meanwile
# defaults set to "tor"
socks5 127.0.0.1 1081

Usage: proxychains [command].

Chrome Addons

SwitchyOmega.

一月七日杂感

前几天和阿三聚了一餐,这大概是一年到头来我们为数不多能好好聊天的时间。

我们谈了很多,从考试到动漫到未来。令人惊讶的是,他表现出了一种忧虑,对未来的忧虑。在我看来这是很少见的。忧虑的一方面是关于短期的未来,有CSST面试的压力,以及成堆的考试;另一方面是更遥远的未来,暑研或是升学或是就业。再往前两天的团队聚餐上大家的讨论,关于资本寒冬的,关于机器学习的逐渐饱和,都给我们留下了深刻的印象。

我问他不做金融吗。他说经过暑假的实习他也对这个行业失去了兴趣,量化交易不过也是机械性的脑力劳动(如有冒犯请见谅,这是我凭回忆归纳的,然而我对这个行业一窍不通)。现在他也开始迷茫将来要做什么。

他说有点羡慕我的状态,对周围的环境不care,沉浸在自己的小世界当中。这个学校没能让他满意,没有地缘优势,身边足够优秀的人还是少了些。但这些在我看来都不重要,甚至还是优点。

吃完饭后已经是九点半了。雾霾洇开了路灯的光晕,整个城市笼上了一种眩目的橘黄色。

在那之后,我又断断续续想了很多。机器学习真的是我喜欢的吗?钻研理论时我是开心的,但我没有记笔记的习惯;做实验有时会让我很头疼,冗长而累人,很多时候结果还并不好。让我快乐的其实是在概念间的思维游走,但真正深入细节却是有些乏味的。许多创意到了底层,无非也是各种指标的相互比较——除非你是一个子领域的开山鼻祖。但这需要热情和灵感,我认为我没有。我之所以处在这其中,是因为它热门——至少当时是的,而且不让我讨厌,无论是数学或是 CS。

我想我最纯粹的快乐就是写代码了,次之就是钻研各种新东西,数学上或程序上的。但这两者都不能让我活下去。逐利的代码是需要迎合市场的,但这很累,而且会包含许多我讨厌的东西。我从来不是一个好的产品经理,也不想成为。我只希望能依自由意志写代码,折腾各种东西,这些产出多是无用的或是无法迎合市场的,但又确实能让我感到快乐。这个愿望其实是奢侈的。如果把「写代码」替成「追番」、「玩手机」、「打机」,那就能契合到很多人身上。我还是需要一门手艺,支撑我活下去,而让我的纯粹爱好成为我的业余游戏。

既然如此,为什么不尝试将手艺的价值最大化呢?比如出国。在另一个环境凭这门手艺或许能活得更好。我觉得这其中有太多令我望而却步的东西,包括和很多人打交道,包括环境的切换。很多人觉得没什么,但我却十分在意。或许是刻在基因里的一种病吧。不想和人说话;一旦浸入了一个环境,出来时会痛苦万分。升学时也是,回家时也是。想改也改不了。

所以呢,依然没有结论,未来依旧是迷茫的。这两年多我错过了很多机会,实不相瞒是故意的。但也意外收获了一些好处,或许可以成为新的契机。很多问题要随着时间的流动才能找到答案,我也祈祷如此吧。

Sublime 配置 Rust 环境

rustup v.s. cargo

cargo 是 Rust 最底层的包管理器,类似 npm 或 pip。

rustup 是 Rust 的工具链管理器,允许开发者在多个不同版本的工具间切换。所谓工具不仅包括 rustc 和 cargo,还包括 rustfmt、racer 等一系列辅助开发的模块。类似于 Anaconda、Pipenv 之于 Python,或是 n 之于 Node.js。

Rust 的工具链默认存在于 ~/.cargo/bin 中,rustup 会用代理脚本覆盖其中的可执行文件,从而用户可以通过命令行标志方便地切换版本。

stable v.s. beta v.s. nightly

Rust 官方默认提供三个通道,稳定性依次递降,即时性依次递增。当然,还有众多的第三方版本。

Rust 工具链普遍有一个标志 +<channel> 用于注明通道版本,如:

1
2
3
4
$ rustc +nighly --version
rustc 1.33.0-nightly (68fe5182c 2019-01-05)
$ rustc +stable --version
rustc 1.31.1 (b6c32da9b 2018-12-18)

Sublime 配置

我们希望让 Sublime 支持如下功能:

  1. Auto Formatting
  2. Auto Completement
  3. Check on Save

为此需要两个插件:

  • Rust Enhanced(提供 3)
  • Anaconda Rust(提供 1 和 2)

Rust Enhanced

直接安装即可。

Anaconda Rust

官方版本停更了,rustfmt 相关功能有一些问题。为此需要使用我修改过的版本:https://github.com/hsfzxjy/anaconda_rust

依赖 rustfmtracer

racer

racer 需要 nightly 版本,用以下脚本安装:

1
$ cargo +nightly install racer

此方法需要本地编译,时间比较久。

自动补全的完成还需要一份 Rust 库的源码,可以从这个页面 下载。

解压完成后需要配置 Anaconda Rust 插件的 rust_src_path 选项。

rustfmt

rustfmt 支持使用 rustup 安装,更省时间:

1
$ rustup component add rustfmt-preview

四月·病

四月,我大病了一场。先是呼吸时胸口隐隐作痛,我以为是运动伤害,毕竟始发时刚剧烈地骑完车。后而逐渐变成呼吸困难,镜子里的自己嘴唇发紫,睡觉时也像是有人扼着喉咙。我开始在傍晚时发烧。

清明前后,春寒未散。宿舍已没有了暖气。清明节我在宿舍躺了两天,睡到饭点起来吃,吃完继续睡。两个舍友出去玩了,合肥一直在下雨,屋里甚是寒冷。

躺在床上,我不停查找着可能的病源。我是个不轻易上医院的人,但这突如其来的状况着实让我害怕。我想在相关疾病的列表中寻求安慰,希望只是一场小病。为什么不上医院呢?去医院一切就定下来了,无论结果是好是坏。但如果不去,就还有无数的可能。我总是这么想。

入夜时,我也会想,如果这真是糟糕的病又该怎么办呢?我在一个陌生的城市,一切都会变得麻烦;我的人生才刚刚开始,还有很多事没有做。诸如此类我想了很多很多,从黄昏到夜深,混杂着不安与飘忽不定的希冀入睡,再到早晨。

后来,病似乎开始好转。发烧渐渐没有了,但胸疼和窒息感却交替着。每当胸疼开始减轻时,就会有只无形的手慢慢握紧我的喉咙;手松开时,胸疼又开始发作。如此往复。我数次怀疑自己再也好不了了。四月在浑浑噩噩中度过了。

庆幸的是,期中考没有被耽误,我妈来看我时也没有发现异样。这话不知怎么的就脱口而出了,连我也觉得自己有些病态。明明可能是危及生命的事情,却要在众人面前尽力隐藏。我认为这种事不好,却一直在做,仿佛被周围人知道后天会塌下来一样。

接下来的五月,天气暖了起来,胸疼和窒息开始消退。当然我觉得不完全是温度的作用。持续的雨也渐渐停了。我似乎看到了希望。再到六月和炎热的七月,病终于完全好了。我可以自由地跑动,也可以大力地呼吸。这种没有不适感的感觉,客观上只过了三个月,主观上却长的像一生。

再后来,我没有和任何人提起过这段经历,如今病好了,也更不会了。我不知道这是什么病,现在也不想知道,以后也希望它不要再来了。这三个月里我想了很多很多。当自己恍惚看见时间的尽头时,才突然意识到曾经浪费了许多时间。多次感叹时间不够用,没能做成想做的事,我却把时间花在许多无关紧要的东西上。小时候我讨厌成为这样的人,但还是成为了这样的人。而如今,生活逐渐被紧要却无趣的事填满了。就算我改正这个毛病,乐趣也变少了。无奈。

而至于为什么又想起这件事,我也不清楚。只是单纯觉得岁末应该写点东西吧。

Haskell 笔记:State Monad

一个依赖于外部状态 s 的伪函数 f' :: a -> b,我们可以将其改写为 f :: a -> s -> (b, s) 使其良定。即,在输入输出中显式传递状态 s。现在,我们需要利用 Monad 将状态传递过程隐藏起来。

注意到,输出值 (b, s) 中的末状态 s 不仅依赖于输入状态,更依赖于之前更改过状态的一系列函数及其逻辑。因此我们不能简单地将 Monad 定义为 (a, s) 类似的形式,否则两个函数用 >=> 结合的结果将与函数逻辑无关,这与我们的期望不符。

考虑如下定义:

1
newtype State s a = { runState :: s -> (a, s) }

由于 -> 的右结合性,f :: a -> s -> (b, s)f :: a -> State s b 等价。固定 s,则 State s 可以成为一个 Monad。一个类型为 State s a 的值通常也被称为一个 state processor。

现在尝试定义 (>>=) :: State s a -> (a -> State s b) -> State s b。若 p >>= f,则 p 蕴含了在此之前所有的状态处理逻辑,我们希望将 pf 的逻辑融合在一起,成为一个新的 state processor,并作为返回值。

1
2
3
4
5
6
7
8
p >>= f =
(
State $ \s -> (b, s'')
where
(a, s') = (runState p) s
p2 = f a -- :: State s b
(b, s'') = (runState p2) s'
)

return 是平凡的:

1
return a = State $ (\s -> (a, s))

fmap 可以作如下定义:

1
2
3
4
5
6
7
8
9
fmap :: (a -> b) -> (State s a) -> (State s b)
fmap f =
(
\pIn -> (
\s -> (b, s')
where
(a, s') = (runState pIn) s
b = f a
)

如此一来,我们可以将一系列的依赖外部状态的函数串成一个依赖外部状态的函数,传以初始状态,便可得到结果。

Haskell 笔记:Monad 引论

动机

pure functions 看似完美,但却不能模拟现实世界中的诸多任务。这是由于 pure functions 是良定的映射,对于特定的输入值会返回唯一的输出。这种模式在面对如下任务时会显得苍白无力:

  • 有可能失败的任务。如大多数的 IO。
  • 依赖外部状态的任务。如(伪)随机数生成器。
  • 非确定性任务,即对于确定的输入可能有多个输出。这种在 IP 中较为少见。
  • 对外界会造成影响的任务。如大多数的写入过程。

这些问题可以用数学中的域扩充技巧来解决。

域扩充

在数学中,当定义问题的范畴不足以容纳问题的解时,我们通常会对相关的范畴进行扩充。类似的技巧同样也可以应用在这里。

假设一个不良定的函数 f: A -> B

  • 如果 f 有可能失败,我们可以将 B 扩充为 Err(B) ∪ { reasons of failures },其中 reasons of failures 可能是对异常的描述,也可以是空值一类的东西。则 f': A -> Err(B) 是良定的映射,且与 f 行为一致。事实上,这就是 Maybe Monad 和 Either Monad。
  • 如果 f 依赖于外部状态,我们定义 Pref(B)从外部状态空间到 B 的映射的全体,则 f': A -> Pref(B) 为良定的映射,且行为和 f 一致。换言之,对于特定的输入 af'(a) 返回一个函数,其中蕴含了已知 a 时如何从各种不同状态得到结果的逻辑。事实上,这就是 State Monad。
  • 如果 f 具有非确定性,我们将 B 扩充为 Power(B),即 B 的幂集。则 f': A -> Power(B) 为良定的映射,且行为与 f 一致。事实上,这就是 List Monad。
  • 如果 f 依赖于真实世界,我们将 B 扩充为 IO(B),其中的元素为一些值域为 B伪函数,可能对真实世界有影响。这些伪函数已经脱离了 pure functions 的范畴,但将它们看成元素是没有问题的。如此一来 f': A -> IO(B) 为良定的映射,且行为与 f 一致。事实上,这就是 IO Monad。

以上操作都有一个共同点,即对一个不良定函数的值域做了扩充,使之变成良定函数。如果用 Haskell 语言描述,它们都有相似的型:f :: a -> m b,其中 m 为扩充规则。

一个问题随之而来:这样的新函数该怎么结合?为此我们要对相关逻辑进行抽象。这就是 Monad。

Monad

这里我们尝试从实际需求出发,导出一个 Type Constructor 成为 Monad 的必要条件。

约定两个名称:

  • a -> m b 型函数为 monadic function
  • a -> b 型函数为 non-monadic function

首先需要解决的是 monadic functions 如何结合的问题。这个问题具有重要的现实意义。monadic function 常常代表某种计算任务,它们之间的结合相当于把若干计算任务串行化,而后者是非常常见的需求。

我们希望有一种运算符有如下的类型 (b -> m c) -> (a -> m b) -> (a -> m c),在此记为 >=> (因其形状,常被叫做 fish operator)。一个自然的想法是,Monad m 需要某种平凡的拆箱操作 extract' :: m a -> a。所谓“平凡”,即 extract' 不应该丢失参数的任何信息。但这往往不能实现,因为 m a 通常会比 a 包含更多的信息,导致 extract' 无法构成良定的映射。例如 Maybe a 中的值 Nothing 就无法在 a 中找到对应的值。

而事实上,我们不需要条件这么强的拆箱操作。在 m 已是 Functor 的情况下,拆箱操作可以弱化为 join :: m (m a) -> m a。我们尝试用 fmapjoin 合成 >=>

1
2
3
4
5
6
7
8
9
10
f :: b -> m c
g :: a -> m b
fmap f :: m b -> m (m c)
(fmap f) . g :: a -> m (m c)
join . (fmap f) . g :: a -> m c
-- i.e.
f >=> g = join . (fmap f) . g

Functor 的假设是容易成立的。当然我们可以定义多个不同的 fmap,如此产生的 Monad 会有不同的语义。join 的假设也是容易成立的,m (m a) 通常和 m a 包含相同多的信息。故此做法是实际可行的。

我们再考虑 monadic function 和 non-monadic function 结合的问题。期望有如此一个运算:>.> :: (b -> c) -> (a -> m b) -> (a -> m c)。注意,此处返回值是 a -> m c 而不是 a -> c,因为我们不希望 a -> m b 产生的额外信息有所丢失。自然地,我们希望有一个平凡的装箱操作,return :: a -> m a。如此一来便可结合 >=> 完成上面的运算:

1
2
3
4
5
6
7
8
9
f :: b -> c
g :: a -> m b
return . f :: b -> m c
(return . f) >=> g :: a -> m c
-- i.e.
f >.> g :: (return . f) >=> g

non-monadic function 和 monadic function 另一个方向的结合是平凡的。

综上我们可以得到成为 Monad 的基本条件:

  • 是 Functor,存在 fmap :: (a -> b) -> m a -> m b
  • 有一个平凡的拆箱操作 join :: m (m a) -> m a
  • 有一个平凡的装箱操作 return :: a -> m a

为了描述平凡,我们要求三个函数必须满足如下公理(下面的 f 为 non-monadic function):

  1. return . f == (fmap f) . returnreturn 的平凡性)
  2. join . fmap (fmap f) == (fmap f) . joinjoin 的平凡性)

事实上在 Category Theory 中,还有另外两条公理:

  • join . (fmap join) == join . join
  • join . fmap return == join . return == id

以上四条公理描述了 Id(恒等 Functor)、mm^2m^3 之间的泛性质,并使图交换。

Monad Typeclass

以下为 Prelude 中的定义:

1
2
3
4
class Functor m => m a where
return :: a -> m a
(>>=) :: m a -> (a -> m b) -> m b

此处没有出现 join,也没有 fish operator,而是使用了一个更常用的算符 >>= (通常称为 bind operator)。这是因为在实际中我们不直接将函数结合,而是使用 non-pointfree 的写法。

此外,还有 >> :: m a -> m b -> m b 运算符。return>>=>> 三者是构成 do-notation 的基础。此处不再赘述。

References

Haskell 笔记:Applicative

Motivation

Functor solves the problem of mapping regular one-parameter functions into a sub-category, but that’s not easy for functions with more than one parameters.

Let’s consider a function with two parameters f :: a -> b -> c, which can also read as a -> (b -> c). Applying fmap on f, we will get fmap f :: m a -> m (b -> c). There’s still some distance from what we want: f' :: m a -> m b -> m c. To get f', we need a transform from m (b -> c) to m b -> m c. Here we denote it as <*> :: m (b -> c) -> m b -> m c. We will later show that such transform is universal for functions with more parameters.

Now consider a function with three parameters f :: a -> b -> c -> d. We are going to transform it into a wrapped-value version, with the help of fmap and <*>.

1
2
3
4
5
6
7
8
9
f :: a -> b -> c -> d
(fmap f) :: m a -> m (b -> (c -> d))
\a_ b_ -> (fmap f a_) <*> b_
:: m a -> m b -> m (c -> d)
\a_ b_ c_ -> ((fmap f a_) <*> b_) <*> c_
:: m a -> m b -> m c -> (m d)

Here \a_ b_ c_ -> ((fmap f a_) <*> b_) <*> c_ is in the desired type. For most of the time, applying parameters directly is actually what we want, instead of the function itself, so the code could simply be written as ((fmap f a) <*> b) <*> c, where a, b and c are wrapped values. Parenthesis could be omitted if precedences are set properly, which leads to a neat and easy-to-read form:

1
f `fmap` a <*> b <*> c

In haskell, fmap has an infix name <$>. So finally we get: f <$> a <*> b <*> c.

Applicative

Haskell pre-defined a type class Applicative, which captures the pattern <*>. Any type that implements Applicative works well with <$> and <*>.

1
2
3
4
5
6
class Functor f => Applicative (f :: * -> *) where
pure :: a -> f a
(<*>) :: f (a -> b) -> f a -> f b
GHC.Base.liftA2 :: (a -> b -> c) -> f a -> f b -> f c
(*>) :: f a -> f b -> f b
(<*) :: f a -> f b -> f a

Note that an Applicative is also a Functor. Apart from <*>, there are some other helper functions or operators in Applicative.

pure is equivalent to the default value constructor of f, e.g. (:[]) for List or Just for Maybe. This may be handful when lifting an unwrapped value to a wrapped one.

liftA2 transforms a binary operator to the corresponding version. The function exists as binary operators would be frequently passed among high-order functions.

*> takes two wrapped parameters and simply returns the second one, which sequence up two wrapped values. This is quite useful for Applicative with action semantics, such as IO. In fact, it’s so useful that Haskell introduces a syntax sugar for it, known as the do-notation. Particularly:

1
2
3
do
putStrLn "1"
putStrLn "2"

is equivalent to

1
putStrLn "1" *> putStrLn "2"

<* is similar. Both will be reviewed while studying Monad.