本文为Type Theory and Formal Proof : An Introduction 的笔记，纯个人向（

之前我们遇到了以下的依赖关系：

• 依赖于项的项：$\lambda_\to$.
• 依赖于项的项$+$依赖于类型的项：$\lambda2$.
• 依赖于项的项$+$依赖于类型的类型：$\lambda\underline{\omega}$.

显然有一个扩展缺失了：

• 依赖于项的项$+$依赖于项的类型：$\lambda{\rm P}$.

最近在尝试用Haskell实现Peter Shirley的Ray Tracing in a Weekend一书，发现了这个问题，并琢磨出了一些解法，看起来像是发现了一种设计模式，不过不知道叫什么名字（

本文为Type Theory and Formal Proof : An Introduction 的笔记，纯个人向（

类型构造子

之前我们从项$\lambda x:\sigma.x$中由类型变量抽象出$\lambda \alpha:\ast.\lambda x:\alpha.x$. 类似的，我们也可以从类型上抽象. 如类型$\beta\to\beta,\ \gamma\to\gamma,\ (\gamma\to\beta)\to(\gamma\to\beta),\ \dots$，都有$\Diamond\to\Diamond$这样的结构.

本文为Type Theory and Formal Proof : An Introduction 的笔记，纯个人向（

类型抽象和类型应用（Type-abstraction and type-application）

对于抽象这个过程，我们有项$M$，其中可能有自由变量$x$，假设$x$有类型$\sigma$，我们从$M$中抽象$x$，可以得到项$\lambda x : \sigma.M$，同时，所有在$M$中的自由变量$x$被绑定了，我们说：

项$\lambda x:\sigma.M$依赖于项$x$.

因此，$\lambda{\to}$中可以构造依赖于项的项（terms depending on terms）.

相应的是应用，对于$MN$的构造，我们可以把$M$应用到$N$，也得到一个项.

这称为一阶（first order）抽象，或一阶依赖，因为这个抽象是在项上进行的. 同时应用也是一阶的.

现在我们引入依赖于类型的项（terms depending on types），称二阶运算（second order operations）或二阶依赖（second order dependency）.

得到的这一系统称二阶类型lambda演算（second order typed lambda calculus），或$\lambda 2$.

本文为Type Theory and Formal Proof : An Introduction 的笔记，纯个人向（

简单类型（Simple types）

我们从一个类型变量（type variables）的无限集开始：$\mathbb{V}=\lbrace \alpha,\beta,\gamma,…\rbrace$.

所有简单类型的集合$\mathbb{T}$

1. 类型变量（Type variable）若$\alpha \in \mathbb{V}$，则$\alpha \in \mathbb{T}$
2. 箭头类型（Arrow type）若$\sigma,\tau \in \mathbb{T}$，则$(\sigma \to \tau) \in \mathbb{T}$

即 $\mathbb{T= V\ \mid\ T \to T}$ .

本文为Type Theory and Formal Proof : An Introduction 的笔记，纯个人向（

对于函数的抽象，有两个构造方法和一个计算规则：

抽象（Abstraction）

由一个表达式$M$和一个变量$x$ 可以构造表达式$\lambda x.M$，称为$M$上$x$的抽象（abstraction of x over M）

应用（Application）

由表达式$M$和$N$可以构造表达式$M\ N$，称为$M$对$N$的应用（application of M to N）

Beta化简（β-reduction）

形如$(\lambda x.M)N$的表达式可以被改写成$M[x:=N]$，意思是表达式中的$M$中的每个$x$换成$N$，这一过程称为由$(\lambda x.M)N$到$M[x:=N]$的Beta化简（β-reduction）.

注意“应用”仅是构造另一个lambda项的过程，而真正得到结果的过程则是“Beta化简”.

以下是严格定义

单子是Haskell语言中较难理解的概念，本文将以简明的语言介绍这一概念及其应用，由于通俗性与严谨性不可兼顾，本文会牺牲一定的严谨性（）。

单子

Monad在Haskell中是一个类型类，中文通常翻译为单子，在GHC7.10以后它的定义如下：

1
2
3
4
5
6

class Applicative m => Monad m where
  (>>=) :: m a -> (a -> m b) -> m b
  (>>) :: m a -> m b -> m b
  return :: a -> m a
  {-# MINIMAL (>>=) #-}
        -- Defined in ‘GHC.Base’

可以看出Monad是实现了一个(>>=)运算符的Applicative。而这个(>>=)运算符（Bind）类型古怪：它连接的左侧是一个Monad类型的值，右侧则是一个函数。

Identity单子

我们从最基本的例子开始。

Identity单子定义在Control.Monad.Identity中：

1

newtype Identity a = Identity {runIdentity :: a}

我们已经熟悉使用map函数对列表进行操作了：

1

map :: (a -> b) -> [a] -> [b]

而函子就是对这一操作进行的抽象。Haskell通过类型类提供一些抽象的接口，将一些与类型相关的操作封装在了类型（对于类型类）的实现上。

大一上学期结束了，给我最大震撼的还是这门SICP课；由于过于震撼，我觉得有必要记录下来。原本打算学期结束后写一系列文章总结一下，不料下学期课业过于刺激，只好草草以一篇“序”结束。不过虽然课程结束了，学习仍要继续，所以学习笔记也会不断延伸（？）