Tech | 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:

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:

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:

and new values:

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 Client

/etc/ss.json:

proxychains

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

Append following lines to /etc/proxychains.conf:

Usage: proxychains [command].

SwitchyOmega.

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> 用于注明通道版本，如：

Sublime 配置

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

• Rust Enhanced（提供 3）
• Anaconda Rust（提供 1 和 2）

Anaconda Rust

racer

racer 需要 nightly 版本，用以下脚本安装：

rustfmt

rustfmt 支持使用 rustup 安装，更省时间：

return 是平凡的：

fmap 可以作如下定义：

动机

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

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

域扩充

• 如果 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。

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

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

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

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

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

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 <*>.

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:

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 <*>.

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:

is equivalent to

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

Category Theory

A category has three components:

• A collection of objects.
• A collection of morphisms, each of which map one object to another.
• A notion of composition of these morphisms, i.e. morphisms can be composed. If f: A -> B and g: B -> C are morphisms, f.g generates a new morphism A -> C.

Note that a morphism has no specific semantics of mapping, but simply links two objects together. Morphisms are also called Arrows.

Examples

Set Category: Set

All sets and standard functions form a category. Functions need not to be surjective, since morphisms have no mapping semantics.

Group Category: Grp

All groups and homomorphisms between groups form a category. A group has specific algebaric structure, which morphisms should preserve.

Laws

Three laws needed to be followed for a category:

• Composition should be associative.
• Composition operation should be closed in the category, i.e. if f: A -> B and g: B -> C, there must be a h: A -> C satisfying h = f . g.
• For each object A, there should exist an identity morphism id(A): A -> A s.t. for every f: A -> B, f = id(A) . f = f . id(B).

Note that:

• There may exist serveral morphisms between A and B.
• An identity has type A -> A, but a morphism with such type needs not to be an identity.

Functors in Category Theory

A functor maps a category to another category. It should contains two mappings for objects and for morphisms, with composition operation and category laws preserved.

There’s a natural functor from Grp to Set, which maps groups to their underlying sets and group morphisms to the function which behave the same but are defined on sets instead of groups.

It’s common to create new types that hold values of other types. List[a] type constructor creates types that holds sequential values of same type; Maybe[a] creates types that hold operation states (failure, or success with returned values).

Usually we want generated types to inherit functions from types being wrapped. For example, List[Int] should have element-wise addition as Int does, and Maybe[Int] should have similar operations with no burden of re-wrapping and unwrapping. Such ‘inheritance’ is only concerned with the structure of types, instead of specific functions, so should be done automatically if possible.

Haskell language itself forms a category, with all types being objects, and functions being morphisms. Such category is called Hask.

A parameteric type implementing class Functor is a category functor mapping Hask to one of its sub-category, where types m a are the object collection. The type constructor m maps objects, and specific fmap defined on m maps corresponding functions.

It’s worth noted that (a -> b) -> m a -> m b can also read as (a -> b) -> (m a -> m b), as -> is right-associative. This may provide a clearer view of fmap, which takes a regular function in Hask and returns the corresponding function in sub-category.

Examples:

fmap (+) :: List[Int] -> List[Int] generates element-wise addition in List[Int].

fmap (+) :: Maybe Int -> Maybe Int generates such function:

• data 创建了新类型，可以有多个 data constructor。
• newtype 创建了新类型，只能有一个 data constructor，同时新类型的内存布局与原来的类型相同。
• type 没有创建新类型，只是建立了 alias，没有新的 data constructor。

Prelude.foldl

foldl 为 left-associative folding。

foldl (+) 0 [1..3] 等价于 (((0 + 1) + 2) + 3)

• 尾递归，因此有 strict 版本 foldl'
• 求值时必须先到达栈底，遍历完列表，因此无法处理无穷列表

Data.List.foldl’

foldl'foldl 的 TRO 版本。

Prelude.foldr

foldr 为 right-associative folding。

foldr (+) 0 [1..3] 等价于 (0 + (1 + (2 + 3)))

• 没有尾递归，有爆栈的危险。

Prelude.foldl1 && Prelude.foldr1

Helper functions。将 operator 限制为同一种类型，同时约去 accumulator。

实践

用 foldr 实现 foldl

g list === foldr f v list.

配置 Aria2

Github 下载源码 ./configure && make -j8 && sudo make install

配置 Chrome 插件

clone https://github.com/acgotaku/BaiduExporter