你不明白欣德利-米尔纳的哪一部分? [英] What part of Hindley-Milner do you not understand?

问题描述

我发誓曾经有一件T恤出售，上面印有不朽的文字:

I swear there used to be a T-shirt for sale featuring the immortal words:

什么部分

你不明白吗?

就我而言，答案是……全部！

In my case, the answer would be... all of it!

特别是，我经常在 Haskell 论文中看到这样的符号，但我不知道它是什么意思.我不知道它应该是什么数学分支.

In particular, I often see notation like this in Haskell papers, but I have no clue what any of it means. I have no idea what branch of mathematics it's supposed to be.

我当然认识希腊字母表的字母和符号，例如∉"(通常表示某物不是集合的元素).

I recognize the letters of the Greek alphabet of course and symbols such as "∉" (which usually means that something is not an element of a set).

另一方面，我以前从未见过⊢"(维基百科声称这可能意味着分区").我也不熟悉这里的vinculum的使用.(通常，它表示一个分数，但这里似乎不是这种情况.)

On the other hand, I've never seen "⊢" before (Wikipedia claims it might mean "partition"). I'm also unfamiliar with the use of the vinculum here. (Usually, it denotes a fraction, but that does not appear to be the case here.)

如果有人至少能告诉我从哪里开始寻找理解这片符号海洋的含义，那会很有帮助.

If somebody could at least tell me where to start looking to comprehend what this sea of symbols means, that would be helpful.

推荐答案

• 水平条表示[上方] 暗示 [下方]".
• 如果[above]中有多个表达式，则将它们和放在一起考虑；所有[以上]必须真实，以保证[以下].
• : 表示有类型
• ∈ 表示在.(同样，∉ 表示不在".)
• Γ 通常用于指代环境或上下文；在这种情况下，它可以被认为是一组类型注释，将标识符与其类型配对.因此x : σ ∈ Γ 意味着环境Γ 包括x 具有类型σ 的事实.莉>
• ⊢ 可以读作证明或确定.Γ ⊢ x : σ 表示环境Γ确定x的类型为σ.
• , 是一种将特定的附加假设包含到环境Γ中的方法.
  因此，Γ, x : τ ⊢ e : τ' 意味着环境 Γ，附加的、覆盖的假设 x 具有type τ，证明e的类型为τ'.
• The horizontal bar means that "[above] implies [below]".
• If there are multiple expressions in [above], then consider them anded together; all of the [above] must be true in order to guarantee the [below].
• : means has type
• ∈ means is in. (Likewise ∉ means "is not in".)
• Γ is usually used to refer to an environment or context; in this case it can be thought of as a set of type annotations, pairing an identifier with its type. Therefore x : σ ∈ Γ means that the environment Γ includes the fact that x has type σ.
• ⊢ can be read as proves or determines. Γ ⊢ x : σ means that the environment Γ determines that x has type σ.
• , is a way of including specific additional assumptions into an environment Γ.
  Therefore, Γ, x : τ ⊢ e : τ' means that environment Γ, with the additional, overriding assumption that x has type τ, proves that e has type τ'.

按要求:运算符优先级，从高到低:

As requested: operator precedence, from highest to lowest:

• 特定于语言的中缀和混合运算符，例如 λ x .e, ∀α .σ, and τ → τ', let x = e0 in e1, 以及函数应用的空格.
• :
• ∈ 和 ∉
• ,(左关联)
• ⊢
• 空格分隔多个命题(关联)
• 单杠
• Language-specific infix and mixfix operators, such as λ x . e, ∀ α . σ, and τ → τ', let x = e0 in e1, and whitespace for function application.
• :
• ∈ and ∉
• , (left-associative)
• ⊢
• whitespace separating multiple propositions (associative)
• the horizontal bar

这篇关于你不明白欣德利-米尔纳的哪一部分?的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！