我发誓曾经有一件T 恤出售，上面印着不朽的文字：
哪一部分
你不明白吗？
就我而言，答案是……全部！
特别是，我经常在 Haskell 论文中看到这样的符号，但我不知道它是什么意思。我不知道它应该是什么数学分支。
我当然认识希腊字母表中的字母和诸如“∉”之类的符号（这通常意味着某物不是集合的元素）。
另一方面，我以前从未见过“⊢”（维基百科声称它可能意味着“分区”）。我也不熟悉这里的 vinculum 的使用。（通常，它表示分数，但这里似乎并非如此。）
如果有人至少可以告诉我从哪里开始寻找理解这个符号海洋的含义，那将很有帮助。
如果有人至少可以告诉我从哪里开始寻找理解这片符号的海洋意味着什么
请参阅“编程语言的实践基础”，第 2 章和第 3 章，通过判断和推导来了解逻辑风格。整本书现在可以在亚马逊上买到。
归纳定义是研究编程语言不可或缺的工具。在本章中，我们将开发归纳定义的基本框架，并给出一些使用示例。归纳定义由一组规则组成，用于推导各种形式的判断或断言。判断是关于一个或多个特定类型的句法对象的陈述。规则规定了判决有效的充分必要条件，从而充分确定了判决的含义。
我们从关于句法对象的判断或断言的概念开始。我们将使用多种形式的判断，包括以下示例：
判断表明一个或多个句法对象具有属性或相互之间存在某种关系。属性或关系本身称为判断形式，一个或多个对象具有该属性或处于该关系中的判断称为该判断形式的实例。判断形式也称为谓词，构成实例的对象就是它的主语。我们为断言J成立a的判断写一个 J。当强调判断的主题并不重要时，（文本在此处截断）
符号来自自然演绎。
⊢ 符号称为十字转门。
6条规则很简单。
Var规则是相当微不足道的规则 - 它表示如果标识符的类型已经存在于您的类型环境中，那么推断您只需从环境中获取的类型。
App规则说，如果你有两个标识符e0，e1并且可以推断出它们的类型，那么你就可以推断出 application 的类型e0 e1。e0 :: t0 -> t1如果您知道并且（相同的 t0！），则规则如下所示e1 :: t0，则应用程序类型良好且类型为t1.
Abs并且Let是推断 lambda-abstraction 和 let-in 类型的规则。
Inst规则说您可以用不太通用的类型替换一种类型。
有两种方法可以考虑 e：σ。一个是“表达式 e 具有类型 σ”，另一个是“表达式 e 和类型 σ 的有序对”。
将 Γ 视为关于表达式类型的知识，实现为一组表达式和类型对，e : σ。
旋转门⊢表示从左边的知识，我们可以推断出右边的内容。
因此可以阅读第一条规则 [Var]：
如果我们的知识 Γ 包含对 e : σ，那么我们可以从 Γ 推断出 e 具有类型 σ。
第二条规则 [App] 可以理解为：
如果我们从 Γ 可以推断出 e_0 具有类型 τ → τ'，并且我们可以从 Γ 中推断出 e_1 具有类型 τ，那么我们可以从 Γ 中推断出 e_0 e_1 具有键入τ'。
通常写为 Γ, e : σ 而不是 Γ ∪ {e : σ}。
第三条规则 [Abs] 因此可以解读为：
如果我们从 Γ 扩展 x : τ 可以推断出 e 具有类型 τ'，那么我们可以从 Γ 推断出 λx.e 具有类型 τ → τ'。
第四个规则 [Let] 留作练习。:-)
第五条规则 [Inst] 可以解读为：
如果我们从 Γ 可以推断出 e 具有类型 σ'，并且 σ' 是 σ 的子类型，那么我们可以从 Γ 推断出 e 具有类型 σ。
第六条也是最后一条规则 [Gen] 可以解读为：
如果我们从 Γ 可以推断出 e 具有类型 σ，并且 α 在 Γ 中的任何类型中都不是自由类型变量，那么我们可以从 Γ 推断出 e 具有类型∀ασ。