Hindley do you not understand?"
I can't find it now, but I swear there used to be a T-shirt for sale featuring the immortal words:
What part of
do you not understand?
In my case, the answer would be... all of it!
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 recognise the letters of the Greek alphabet of course, and symbols such as "∉" (which usually means that something is not an element of a set).
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.)
I imagine SO is not a good place to be explaining the entire Milner Hindley algorithm. But if somebody could at least tell me where to start looking to comprehend what this sea of symbols means, that would be helpful. (I'm sure I can't be the only person who's wondering...)
: 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 τ' . This syntax, while it may look complicated, is actually fairly simple. The basic idea comes from logic: the whole expression is an implication with the top half being the assumptions and the bottom half being the result. That is, if you know that the top expressions are true, you can conclude that the bottom expressions are true as well.
Symbols
Another thing to keep in mind is that some letters have traditional meanings; particularly, Γ represents the "context" you're in—that is, what the types of other things you've seen are. So something like Γ ⊢ ... means "the expression ... when you know the types of every expression in Γ .
The ⊢ symbol essentially means that you can prove something. So Γ ⊢ ... is a statement saying "I can prove ... in a context Γ . These statements are also called type judgements.
Another thing to keep in mind: in math, just like ML and Scala, x : σ means that x has type σ . You can read it just like Haskell's x :: σ .
What each rule means
So, knowing this, the first expression becomes easy to understand: if we know that x : σ ∈ Γ (that is, x has some type σ in some context Γ ), then we know that Γ ⊢ x : σ (that is, in Γ , x has type σ ). So really, this isn't telling you anything super-interesting; it just tells you how to use your context.
The other rules are also simple. For example, take [App] . This rule has two conditions: e₀ is a function from some type τ to some type τ' and e₁ is a value of type τ . Now you know what type you will get by applying e₀ to e₁ ! Hopefully this isn't a surprise :).
The next rule has some more new syntax. Particularly, Γ, x : τ just means the context made up of Γ and the judgement x : τ . So, if we know that the variable x has a type of τ and the expression e has a type τ' , we also know the type of a function that takes x and returns e . This just tells us what to do if we've figured out what type a function takes and what type it returns, so it shouldn't be surprising either.
The next one just tells you how to handle let statements. If you know that some expression e₁ has a type τ as long as x has a type σ , then a let expression which locally binds x to a value of type σ will make e₁ have a type τ . Really, this just tells you that a let statement essentially lets you expand the context with a new binding—which is exactly what let does!
The [Inst] rule deals with sub-typing. It says that if you have a value of type σ' and it is a sub-type of σ ( ⊑ represents a partial ordering relation) then that expression is also of type σ .
The final rule deals with generalizing types. A quick aside: a free variable is a variable that is not introduced by a let-statement or lambda inside some expression; this expression now depends on the value of the free variable from its context.The rule is saying that if there is some variable α which is not "free" in anything in your context, then it is safe to say that any expression whose type you know e : σ will have that type for any value of α .
How to use the rules
So, now that you understand the symbols, what do you do with these rules? Well, you can use these rules to figure out the type of various values. To do this, look at your expression (say fxy ) and find a rule that has a conclusion (the bottom part) that matches your statement. Let's call the thing you're trying to find your "goal". In this case, you would look at the rule that ends in e₀ e₁ . When you've found this, you now have to find rules proving everything above the line of this rule. These things generally correspond to the types of sub-expressions, so you're essentially recursing on parts of the expression. You just do this until you finish your proof tree, which gives you a proof of the type of your expression.
So all these rules do is specify exactly—and in the usual mathematically pedantic detail :P—how to figure out the types of expressions.
Now, this should sound familiar if you've ever used Prolog—you're essentially computing the proof tree like a human Prolog interpreter. There is a reason Prolog is called "logic programming"! This is also important as the first way I was introduced to the HM inference algorithm was by implementing it in Prolog. This is actually surprisingly simple and makes what's going on clear. You should certainly try it.
Note: I probably made some mistakes in this explanation and would love it if somebody would point them out. I'll actually be covering this in class in a couple of weeks, so I'll be more confident then :P.
if somebody could at least tell me where to start looking to comprehend what this sea of symbols means
See " Practical Foundations of Programming Languages. ", chapters 2 and 3, on the style of logic through judgements and derivations. The entire book is now available on Amazon.
Chapter 2
Inductive Definitions
Inductive definitions are an indispensable tool in the study of programming languages. In this chapter we will develop the basic framework of inductive definitions, and give some examples of their use. An inductive definition consists of a set of rules for deriving judgments, or assertions, of a variety of forms. Judgments are statements about one or more syntactic objects of a specified sort. The rules specify necessary and sufficient conditions for the validity of a judgment, and hence fully determine its meaning.
2.1 Judgments
We start with the notion of a judgment, or assertion about a syntactic object. We shall make use of many forms of judgment, including examples such as these:
A judgment states that one or more syntactic objects have a property or stand in some relation to one another. The property or relation itself is called a judgment form, and the judgment that an object or objects have that property or stand in that relation is said to be an instance of that judgment form. A judgment form is also called a predicate, and the objects constituting an instance are its subjects. We write a J for the judgment asserting that J holds of a. When it is not important to stress the subject of the judgment, (text cuts off here)
链接地址: http://www.djcxy.com/p/2286.html上一篇: jQuery.extend的反转（true，...）
下一篇: 欣德利你不明白吗？“