haskell - 表达操作语义时遇到符号问题

Question

我正在尝试编写一些推理规则，但我无法理解通常用于编写它们的符号的含义。

例如:我为某种类型表达式编写了以下规则:

 class(r) ∈ t,  \there_exists v ⊢ r ∈ type(v)
-------------------------------------------------------------
 Γ, m:n -> r ⊢ n:(Γ, r, {}) <-  r

m 是一个声明，其中 n 被 r 替换。

(如果表达式中的r属于t(类型表达式)并且存在v使得r 属于 v 类型)。

可能我的方程完全错误。至少请有人解释一下 ⊢ 和 : 运算符的含义。同样在 Benjamin Pierce 的书中，他将 Γ 称为打字上下文。有人可以用一个例子解释它的含义吗(如果这个例子是用 Haskell、Lisp 或 C++ 编写的，我会很感激)

谢谢

PS:这不是作业。

Answer 1

在较高层次上，符号很简单:假设行上方的条件成立，则行下方的表达式为真。

Γ 是一个类型上下文——也就是说，它是一组变量和类型对。这些对将变量映射到类型。 ⊢ 的意思是“在上下文中”。冒号只是将变量与类型组合起来——就像 ::在 Haskell 中或 :在 Scala 或 Ocaml 中。所以类似 Γ ⊢ x:σ意味着“在上下文 Γ 中，x 具有类型 σ”。类似 Γ,x:σ表示由 Γ 组成的上下文和x:σ .

本质上，上下文代表了其他变量所具有的所有类型。所以x:σ ∈ Γ意味着x类型为σ在Γ ，这可以让您轻松解决 Γ ⊢ x:σ 。这一切都说明如果 x绑定(bind)到上下文中的某种类型，它在该上下文中具有该类型。

您可以将类型上下文视为来自“外部”的所有类型信息。因此，上一段中的简单陈述基本上告诉您，如果您看到 x和x已经有类型 σ ，你可以推断 x类型为σ 。不是很有趣，但非常重要!

您可以将此规则写为:

x:σ ∈ Γ
-------
Γ ⊢ x:σ

如果我们有 LaTeX 就好了:P。我想我们没有 math.se 或 cstheory.se 那么酷。

这是一个稍微复杂一点的例子。本质上，我们想要在简单类型的 lambda 演算中对应用程序的工作方式进行编码。其实很简单:给定一个函数f类型 τ → τ'和一个值x类型 τ然后f x类型为τ' 。在 Haskell 中，这看起来像应用 f :: Int -> Bool上x :: Int 。很明显 f x :: Bool 。所以让我们把这个写出来。

条件(最高位)是，在某些上下文中，f有一个类型 τ → τ' :Γ ⊢ f:τ → τ' 。此外，在同一上下文中，x类型为τ :Γ ⊢ x:τ 。放在一起，我们得到:Γ ⊢ f:τ → τ' Γ ⊢ x:τ .

现在到最后一点。鉴于这两种类型，我们知道什么？我们知道应用程序的类型f x 但仅在相同的上下文中。 (这就是为什么 Γ 很重要。)所以我们得到: Γ ⊢ f x:τ' .

现在，把所有这些放在一起，我们有:

Γ ⊢ f:τ → τ' Γ ⊢ x:τ 
--------------------
     Γ ⊢ f x:τ'

看到 StackOverflow 语法荧光笔与最后一个示例的斗争很有趣。我想知道它认为是哪种语言。