1 · 类型系统

规则：值的类型、类型之间的关系、类型之间的约束 作用：避秒类型错误、提供抽象能力

数据在机器层，都是位，需要另一层表示其含义：无符号数、带符号数、UTF8编码字符

类型系统->类型安全->内存安全 抽象能力

1.1 · Types and Programming Languages#

https://www.cis.upenn.edu/~bcpierce/tapl http://lucacardelli.name/papers/typesystems.pdf

1. 无类型 λ 演算：介绍函数式编程的核心（变量、抽象、应用）
2. 简单类型 λ 演算：
3. 逐步引入复杂类型：子类型、递归类型、多态
   1. 子类型：类型之间的包含关系
   2. 递归类型：类型引用自身
   3. 多态：
4. 高阶系统？

1.1.1 · 无类型 λ 演算：核心

https://www.bilibili.com/video/BV1hX4y1i7hY

目标：将函数抽象（定义）、函数应用（调用）作为逻辑系统的原生概念，从而推理出其他概念与定理

1. 变量（符号）表示一切: 比如函数名称 f1, f2, x…
2. 抽象出函数: 函数定义 (λ p. body)
3. 函数的应用：函数调用 (f p) NOTE: 函数定义时，参数只能一个

函数等价性!

约定：全大写变量，表示符合演算的3个规则

1.1.1.1 · 演算：数字（整数）

用函数应用（调用）次数表示数字，强调的是动作执行的次数

1 -> f(x) 2 -> f(f(x)) 3 -> f(f(f(x)))

one = () => f(x) one = (f, x) => f(x) one = f => x => f(x) 柯里化 two = f => x => f(f(x)) zero = f => x => x 调用零次

转换成阿拉伯数：x为0，f为+1

1.1.1.2 · 演算：布尔

两个值互斥；布尔看作选择器

TRUE = x => y => x FALSE = x => y => y

1.1.1.3 · 演算：IF#

IF = bool => value1 => value2 => bool(value1)(value2)

IF(TRUE)(‘yes’)(‘no’) => ‘yes’ IF(FALSE)(‘yes’)(‘no’) => ‘no’

根据函数等价性：IF = bool => bool

1.1.1.4 · 演算：IS_ZERO（数字+IF）#

IS_ZERO = n => n( ()=>FALSE )(TRUE) // n 为数字，接收两个参数f和x // n == ZERO, return TRUE; ZERO 不会调用f，直接返回x，即TRUE // n != ZERO, return FALSE; 非ZERO 会调用f，直接返回FALSE

1.1.1.5 · 演算：加一

UP = n => f => x => f(n(f)(x)) // n(f)(x) 表示数字n // f() 表示加1

1.1.1.6 · 演算：减一

PAIR = x => y => f(x)(y) FIRST = pair => pair(x => y => x) SECOND = pair => pair(x => y => y)

// 接收两个连续数字，把窗口向右滑一位数 // 连续n次调用SLIDE，得到[n-1, n] // 传入 n 的到 [n-1, n] // n(SLIDE)(PAIR(ZERO)(ZERO)) SLIDE 为 f; PAIR(ZERO)(ZERO) 为x; 和数字一样，即为调用 SLIDE n 次; SLIDE = p => PAIR(SECOND(p))(UP(SECOND(p)))

DOWN = n => FIRST(n(SLIDE)(PAIR(ZERO)(ZERO)))