本文为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课；由于过于震撼，我觉得有必要记录下来。原本打算学期结束后写一系列文章总结一下，不料下学期课业过于刺激，只好草草以一篇“序”结束。不过虽然课程结束了，学习仍要继续，所以学习笔记也会不断延伸（？）