3 ms·

I don't like the notation, because there are usually a lot of implicit assumptions made for each particular set of inference rules. In order to understand the i

I don't like the notation, because there are usually a lot of implicit assumptions made for each particular set of inference rules. In order to understand the inference rules, you usually first have to understand what implicit assumptions are made in the current context. In the current example, there is just no need to write Hindley-Milner in this notation. Using pattern matching and sets will do just fine.

more_original 14y ago
I think there are philosophical reasons why people prefer inference rules over working with sets. Many people work or have worked in a context of constructive logic, as constructivism comes in naturally when you consider computability. Now, implication is a far simpler concept than sets. Implication is modelled by cartesian closed categories, while for sets one needs additional structure, e.g. toposes. So I suppose the fact that inference rules are preferred over pattern matching and sets has to do with them being percieved as being based on simpler principles. Of course, all this is a matter of taste and for particular applications like HM it doesn't make any difference at all which notation to use. I don't want to defend the rule notation too much; it takes up a lot of space in papers and if you have something better then fine. But maybe that explains why people prefer this notation.
jules 14y ago
One thing that's bad about the notation is not so much the horizontal bar notation, but that the pattern matching leaves so much implicit. You would have exactly the same confusion with pattern matching with sets. The problem is that the names of the variables are semantically significant. For example x can only stand for a program variable, not for a compound expression, e can stand for a compound expression, but not for a program variable. There is nothing except the name to distinguish them, and this is usually not explained. Similarly, τ stands for a monotype, whereas σ stands for a polytype (leaving aside the inst rule, where σ can confusingly also stand for a monotype, and the first rule, which should use τ instead of σ). Additionally a lot is left unexplained by the absence of the square inclusion relation and the free(.) function. The horizontal bar notation is not ideal however. In my opinion Prolog notation is clearer, because it reads the right way around, and it makes it clear what relation we are defining. In Prolog notation you'd define a typeof(context, term, type) relation: typeof(C,var(X),T) |- X:T in C typeof(C,app(X,Y),B) |- typeof(C,X,A -> B), typeof(C,Y,A) ... In Prolog you should read |- as "if". So the first rule says: "the type of a variable X is T if `X:T` is in the context C".
- swannodette 14y ago
  It's even nicer in alphaProlog where you can express the scoping implied by lambda terms http://homepages.inf.ed.ac.uk/jcheney/programs/aprolog/ http://homepages.inf.ed.ac.uk/jcheney/programs/aprolog/

more_original 14y ago

I think there are philosophical reasons why people prefer inference rules over working with sets. Many people work or have worked in a context of constructive logic, as constructivism comes in naturally when you consider computability. Now, implication is a far simpler concept than sets. Implication is modelled by cartesian closed categories, while for sets one needs additional structure, e.g. toposes. So I suppose the fact that inference rules are preferred over pattern matching and sets has to do with them being percieved as being based on simpler principles. Of course, all this is a matter of taste and for particular applications like HM it doesn't make any difference at all which notation to use. I don't want to defend the rule notation too much; it takes up a lot of space in papers and if you have something better then fine. But maybe that explains why people prefer this notation.

jules 14y ago

One thing that's bad about the notation is not so much the horizontal bar notation, but that the pattern matching leaves so much implicit. You would have exactly the same confusion with pattern matching with sets. The problem is that the names of the variables are semantically significant. For example x can only stand for a program variable, not for a compound expression, e can stand for a compound expression, but not for a program variable. There is nothing except the name to distinguish them, and this is usually not explained. Similarly, τ stands for a monotype, whereas σ stands for a polytype (leaving aside the inst rule, where σ can confusingly also stand for a monotype, and the first rule, which should use τ instead of σ). Additionally a lot is left unexplained by the absence of the square inclusion relation and the free(.) function. The horizontal bar notation is not ideal however. In my opinion Prolog notation is clearer, because it reads the right way around, and it makes it clear what relation we are defining. In Prolog notation you'd define a typeof(context, term, type) relation: typeof(C,var(X),T) |- X:T in C typeof(C,app(X,Y),B) |- typeof(C,X,A -> B), typeof(C,Y,A) ... In Prolog you should read |- as "if". So the first rule says: "the type of a variable X is T if `X:T` is in the context C".

swannodette 14y ago
It's even nicer in alphaProlog where you can express the scoping implied by lambda terms http://homepages.inf.ed.ac.uk/jcheney/programs/aprolog/ http://homepages.inf.ed.ac.uk/jcheney/programs/aprolog/