您不了解Hindley-Milner的哪一部分? [英] 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.

推荐答案

• 水平条表示"[在上方] 暗含 [在下方]".
• 如果[上方]中有多个表达式，则将它们分别 anded 一起考虑；为了保证[以下]，所有[以上]都必须为真.
• :表示已输入
• ∈表示在. (同样，∉表示不在".)
• Γ通常用于指环境或上下文；在这种情况下，可以将其视为一组类型注释，将标识符与其类型配对.因此，x : σ ∈ Γ意味着环境Γ包括x具有类型σ的事实.
• ⊢可以理解为证明或确定. Γ ⊢ x : σ表示环境Γ确定x具有类型σ.
• ,是一种将包括特定附加假设纳入环境Γ的方法.
  因此，Γ, x : τ ⊢ e : τ'表示环境Γ，具有其他重要的假设，即x具有τ 类型，证明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:

• 语言特定的infix和mixfix运算符，例如λ x . e，∀ α . σ和τ → τ'，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

这篇关于您不了解Hindley-Milner的哪一部分?的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！