程序语言理论 - 类型系统

Makabaka18802025年6月17日...大约 3 分钟

程序语言理论 - 类型系统

写在前面

作为一名软件开发者，或多或少会遇到过各种各样的类型系统。虽然说当今的编程语言大多已经十分完善且安全，但每个语言还是有自己的不足，需要学习类型理论来进行特定类型的实现。同时，类型理论的额学习也可以帮助软件开发者更好的写出更加优雅、稳定、且安全的代码，利人利己。我个人认为PLT是计算机科学里面最美的分支了可以用各种神奇的模型来描绘一些我们从来没法想到过的模型，来完成一下完全想不到的壮举。本系列就是为了方便初学者来快速入门类型论、程序语言理论、多范式编程、及范畴论等在传统软件工程领域被严重忽视的理论计算科学。

欢迎大佬帮忙指出错误，我也在学习，大家一起进步～

序言

本节术语 | Glossary

安全性 (safety) - 指程序在运行时避免未定义行为和错误的能力，包括程序的可验证性、鲁棒性以及对异常情况的安全处理。

第0章 - 类型系统

凌晨2:17。显示器冷光刺破黑暗，键盘的敲击声是房间里唯一的声响。

你按下保存，git push，看着CD / CI管线丝滑的运行着，你十分满意。

就在这时...

- ❌ Production deployment failed: Undefined behavior at 0xFFFF0004

没有堆栈跟踪，没有错误上下文。日志里只有一行冰冷的十六进制地址，像黑夜中突然熄灭的灯塔。

这不是恐怖片情节，而是程序安全性缺失的日常噩梦。

一个程序不安全可能有很多原因。

在嵌入式领域，开发者需要和操作系统等其他因素配合，保证不给对方"下绊子"。例如在LPC2214中，VIC(Vector Interruption Controller)采用了多选一的位域设计，理论上来说VICVectCntl寄存器中只可以有一位是1，但是这种设计很难保证在中途不会因为资源竞争(data race)等原因导致未发现的位反转。例如以下情况会使中断系统进入不可预测的状态：

VICVectCntl0_Type VICVectCntl0;
VICVectCntl0.enable = 1;
VICVectCntl0.priority = 3;
VICVectCntl0.vector = (uint32_t)Handler0;

VICVectCntl0_Type VICVectCntl1;
VICVectCntl1.enable = 1;
VICVectCntl1.priority = 2;
VICVectCntl1.vector = (uint32_t)Handler1;