#函数式编程

使用 Bird Meertens Formalism 导出高效程序与进行自动并行化。

类型论的实践：函数式程序推理与演算。Agda 中的证明、归纳、列表、Internal Verification 和等式理论。

函数式语言如何引入副作用：函子、应用函子、单子。

函数式语言的基础特性概览：列表、类型与高阶函数。

最经典的类型论例子：无类型 λ 演算的规则、使用和合流性。