Question

范畴，类型，语法

Answer 1

有些东西终究是串在一起的。

一环套一环，一个概念跟随着另一个，哪里是源头呢？

故事的起源，关于程序的编译过程，遇见的是各种从未见过的概念，词法，语法，语义。这是一个十分陌生的世界，关于程序的一切信息都被降维了，一个一个字符的读取，一个程序被拆解的支离破碎。

陌生的数学领域，关于字符和字符串的处理与判别，没有加法，没有数字，这些传统的数学对象都消失不见了，似乎一切都要重新开始。

程序拆解为孤立的字符序列，从这样的序列中不断识别出关键字，识别出变量名，随后依靠着预先定义的语法，识别出表达式，最后对表达式进行语义判断，环环相扣，程序又变回程序了，并且得到了编译器的检查。

这个过程如此的神奇，打碎后又得到了还原。

在这整个过程中，最关键的部分就在语法上面了。

语法定义是以一种十分简洁而又难以理解的方式进行，仅仅依靠几段符号，却可以对如此大量的字符串进行分类，这些是变量，那些是表达式，这边是循环结构，那边的则是分支结构等等。

那时，看得稀里糊涂。

这是数理逻辑的一个子目，本应该毫无干系的，数学中的逻辑往往用于阐述证明结构或者方法，曾经我也是这么想的，证明是很吃力的事情，不论是看懂证明，或者写出证明，甚至于要看懂参考答案都是很困难的事情。他们难以捉摸，十分神秘，奇怪的构造函数，诡异的放缩手法，从天而降的参数代换实在是让人摸不着头脑。

不过，那不过是证明的书写者为了省事所遗留的问题，证明过程的每一步都可以写的十分易懂，它们不过是一些最基本事实的罗列与堆叠，只不过，这样展开带来的就是无聊而冗长的符号表。如果可以自动转化成不同的证明版本就好了，基础扎实水平高的读者看简略的证明，基础不太好只能看出明显事实的就给出完整证明，对于缺乏基础的给出傻瓜式证明，虽然同样可以读懂，但篇幅就十分劝退了。这种机器估计是还没有，不过，对于人而言显然可以做到，只是要花很多时间。

类型论，就是通过字符串运算的方式来进行的。

对于字符串的运算，包括连接两个字符串，用一个字符串代替另一个字符串等等，通过对这些操作定义一定的意义就可以将证明中的表达式转化为这样的字符串和运算了。

于是，似乎建立了联系，在数值表达式，数值运算与字符串，字符串运算之间建立了联系。

联系的关键就是类型论。

范畴论谈的比较多了，之前也写了很多理解，尽管现在看来有很多的偏差，毕竟学习是渐进的，总不能奢求一遍就成，在反复的揣摩中才能慢慢消化。

通过范畴论的语言可以将这种联系给准确表述出来，首先定义类型范畴，定义代数运算范畴，然后通过函子构建联系，听说伴随函子才是关键，不过，鉴于还未学习到，也没办法介绍。总体上还是可以建立一个直观的印象，那就是这两种看似区别极大的数学对象是有着内在联系的。有联系就代表着可以实现知识的迁移，将成熟领域的各种定义定理，通过这种微妙的联系转化到陌生领域，极大提高研究效率。