写在前面
作为一名软件开发者,或多或少会遇到过各种各样的类型系统。虽然说当今的编程语言大多已经十分完善且安全,但每个语言还是有自己的不足,需要学习类型理论来进行特定类型的实现。同时,类型理论的额学习也可以帮助软件开发者更好的写出更加优雅、稳定、且安全的代码,利人利己。我个人认为PLT是计算机科学里面最美的分支了可以用各种神奇的模型来描绘一些我们从来没法想到过的模型,来完成一下完全想不到的壮举。本系列就是为了方便初学者来快速入门类型论、程序语言理论、多范式编程、及范畴论等在传统软件工程领域被严重忽视的理论计算科学。
欢迎大佬帮忙指出错误,我也在学习,大家一起进步~
写在前面
学这个主要是因为我们社团准备要规范一些写代码的习惯以及结构 确定了OOP以及函数化编程后在寻找适合函数化编程的伪代码规范的时候决定恶补一下底层知识
本文适合对于计算机科学与代数有一定了解的同学 最好是python 我文中就先用py的lambda expression来做的implementation
我自己做了个-calculus的演算器,可以来玩玩 网站 GitHub
结尾有Cheatsheet哈~
一切从小时候的一个发现说起。
那时,常看到爸妈坐在一个嗡嗡作响的大盒子旁,盯着一个发光的屏幕,手里握着一个小小的黑色盒子。
满心好奇,问老爸:“这是什么呀?”他笑着回答:“这是电脑啊。”一下子来了兴趣,脱口而出:我也想要一个!
没过多久,客厅里真的多了一个用纸壳做的大盒子。老爸把发光的屏幕摆到我面前,又递给我那个小黑盒子。我好奇地摆弄着显示器,而他和妈妈站在一旁,满脸笑意地看着我。
自此之后,老爸也给我打造了各式各样的好玩的“电器”,我的房间很快也被这个纸壳王国吞噬了。
本节术语 | Glossary
- 图灵机 (Turing's machine) 利用无限长的纸带和读写头搭建的计算模型
- λ演算 (The Lambda Calculus) 利用无限长的纸带和读写头搭建的计算模型
- 简单类型λ演算 (STLC) 一种带有简单chaining的类型系统
- 上下文 (Context) 关联变量及其类型的数据结构
- 作用域 (Scope) 一种在程序语言中的实现
- 类型判断 (Type Judgement) 通过类型系统来验证程序的合理性