OCaml学习笔记
小陌白 2023/10/19 模型检验形式化方法
# 1 Introduction
OCaml是一款函数式语言。函数式语言提供了一种与之前编程不同的视角。适应这种视角需要放弃旧的想法:赋值语句、循环、类和对象等等。
“A language that doesn’t affect the way you think about programming is not worth knowing.”
—Alan J. Perlis (1922-1990), first recipient of the Turing Award
# 1.1 The Past of OCaml
OCaml起源于Lisp编程语言系列。早先用Lisp进行定理证明时有缺陷,在进行改进时产出的OCaml。微软的F#是Ocaml变体。
# 1.2 The Present of OCaml
OCaml是一款函数式语言,函数式语言的关键语言抽象是数学函数。Ocaml的不变性可以更好的构建并发程序。Ocaml是静态类型和类型安全的编程语言。
- 静态类型语言在编译时检测类型错误
- 类型安全的语言限制了哪些类型的操作可以在哪些类型的数据上执行
OCaml中一些高级特性:
- 代数数据类型:可以构建复杂的数据类型而无需操心指针和内存管理。
- 类型推断:不需要把类型信息写在所有地方,编译器会自动找出绝大多数类型,使得代码更容易阅读和维护。
- 参数多态性:函数和数据结构可以在类型上参数化,有利于代码重用。
- 垃圾回收:自动内存管理让人从内存分配和释放的负担中解脱,内存分配和释放是C等语言常见的bug来源。
- 模块:OCaml通过使用模块使构建大型系统变得容易。模块用于封装接口后面的实现。OCaml通过提供操作模块的函数(称为函子),远远超出了大多数模块语言的功能。
OCaml和其他函数式语言远不如Python、C或Java流行。OCaml的真正优势在于语言操作(即编译器、分析器、验证器、证明器等)。这并不奇怪,因为OCaml是从定理证明领域发展而来的。