3 ms·

The inference rule notation is standard within mathematical logic, which is where it comes from. I'm not an expert on the history of mathematics, but I've seen

The inference rule notation is standard within mathematical logic, which is where it comes from. I'm not an expert on the history of mathematics, but I've seen inference rules for example in Gentzen's 1935 paper and I'm sure they are quite a bit older. I haven't seen a notation that is easier to read than inference rules. Writing them as functional programs can be problematic, as the rules do not always fully specify an algorithm. One judgement may have different derivations. If one writes down algorithms, such as HM type inference, then one does in fact often use notation in the style of functional programming. Incedentally, rather than abolishing the inference rule notation, there are actually tendencies to introduce them into programming: https://en.wikipedia.org/wiki/Epigram_%28programming_language%29 https://en.wikipedia.org/wiki/Epigram_%28programming_languag... (though it remains to be seen if this is a good idea)

auggierose 13y ago
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 13y 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 13y 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 13y 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/
jrabone 13y ago
Given the JVM supports Unicode identifiers, and given the rich vein of mathematical operators therein, I always thought it would be fun to do the APL thing with Java. Scala went a (very) little way towards this, but I don't think anyone has taken it to logical extremes yet. (although I did once threaten my co-workers that I would tell the theoretical mathematician on the team about Unicode identifiers in Java. He used to write LaTeX in the Javadoc comments [which Doxygen handles rather nicely])
- wtetzner 13y ago
  I believe Fortress used Unicode identifiers quite extensively. http://en.wikipedia.org/wiki/Fortress_(programming_language) http://en.wikipedia.org/wiki/Fortress_(programming_language)
  - riffraff 13y ago
    I believe you misremember. From what I recall fortress had an ascii syntax where special combinations would be translated into symbols by the doc/rendering system, eg NN would be rendered as (bold N used for natural numbers).
- limmeau 13y ago
  This would be even more fun if Java supported user-defined infix operators with adjustable precedence, like Haskell. Or even mix-fix operators like Maude. Maude lets you define operators with variable arity and arbitrary stuff before, between and after, like let _ = _ in _ _::_(_) _,_ |- _ You _, but I _ Always considered this a cool feature.
- mcguire 13y ago
  "tell the theoretical mathematician on the team about Unicode identifiers in Java" ...thus reducing his productivity to zero while he hunts through the Unicode maps to find the glyph he wants?
  - tikhonj 13y ago
dchichkov 13y ago
Let us agree to disagree. There are tendencies only to remove strict math notations (particularly ones with implicit assumptions) from programming. Once removed programming languages that use such notation gets adapted by wider and wider communities and gradually become mainstream. And on the opposite, languages that use heavy math notations, even if pushed vehemently by academic community tend to die down. I think this will be demise of Haskell by the way. As good as it is, the notation is still full of '||', '!!', '++', ':' ... So I think there would be another iteration in the functional world. Haskell will die, just like ML/Ocaml/etc had died, because Haskell with slightly better syntactic sugar had captured that segment of developers.
- more_original 13y ago
  Actually, I also think that Haskell will not become mainstream. As a matter of fact, one of the main things I do not like about Haskell is that the type class mechanism makes too many things implicit and that it allows too much overloading. It seems that it is sometimes hard to understand what a code fragment does by just looking at the fragment. By contrast, OCaml code is much easier to understand. But these are not so much syntactic issues. It always seemed to me that people are actually drawn to Haskell's syntax.
  - dons 13y ago
    > By contrast, OCaml code is much easier to understand. Where you have a different + for doubles and ints...
    - more_original 13y ago
      Yes, it's verbose, but verbosity also adds information that may be useful (although + is probably not a good example for this). With 'easier to understand' I mean that when looking at a bit of code I can tell what it does without having to know much about the context (typing, overloading). I did not mean to say that the code is prettier. Haskell code tends to be very pretty. It's probably difficult to strike the right balance between too little and too much overloading. Maybe OCaml does not allow enough overloading. For my taste typical Haskell code uses too much. But that's a matter of taste, I suppose.

auggierose 13y ago

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 13y 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 13y 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 13y 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/

jrabone 13y ago

Given the JVM supports Unicode identifiers, and given the rich vein of mathematical operators therein, I always thought it would be fun to do the APL thing with Java. Scala went a (very) little way towards this, but I don't think anyone has taken it to logical extremes yet. (although I did once threaten my co-workers that I would tell the theoretical mathematician on the team about Unicode identifiers in Java. He used to write LaTeX in the Javadoc comments [which Doxygen handles rather nicely])

wtetzner 13y ago
I believe Fortress used Unicode identifiers quite extensively. http://en.wikipedia.org/wiki/Fortress_(programming_language) http://en.wikipedia.org/wiki/Fortress_(programming_language)
- riffraff 13y ago
  I believe you misremember. From what I recall fortress had an ascii syntax where special combinations would be translated into symbols by the doc/rendering system, eg NN would be rendered as (bold N used for natural numbers).
limmeau 13y ago
This would be even more fun if Java supported user-defined infix operators with adjustable precedence, like Haskell. Or even mix-fix operators like Maude. Maude lets you define operators with variable arity and arbitrary stuff before, between and after, like let _ = _ in _ _::_(_) _,_ |- _ You _, but I _ Always considered this a cool feature.
mcguire 13y ago
"tell the theoretical mathematician on the team about Unicode identifiers in Java" ...thus reducing his productivity to zero while he hunts through the Unicode maps to find the glyph he wants?
- tikhonj 13y ago

dchichkov 13y ago

Let us agree to disagree. There are tendencies only to remove strict math notations (particularly ones with implicit assumptions) from programming. Once removed programming languages that use such notation gets adapted by wider and wider communities and gradually become mainstream. And on the opposite, languages that use heavy math notations, even if pushed vehemently by academic community tend to die down. I think this will be demise of Haskell by the way. As good as it is, the notation is still full of '||', '!!', '++', ':' ... So I think there would be another iteration in the functional world. Haskell will die, just like ML/Ocaml/etc had died, because Haskell with slightly better syntactic sugar had captured that segment of developers.

more_original 13y ago
Actually, I also think that Haskell will not become mainstream. As a matter of fact, one of the main things I do not like about Haskell is that the type class mechanism makes too many things implicit and that it allows too much overloading. It seems that it is sometimes hard to understand what a code fragment does by just looking at the fragment. By contrast, OCaml code is much easier to understand. But these are not so much syntactic issues. It always seemed to me that people are actually drawn to Haskell's syntax.
- dons 13y ago
  > By contrast, OCaml code is much easier to understand. Where you have a different + for doubles and ints...
  - more_original 13y ago
    Yes, it's verbose, but verbosity also adds information that may be useful (although + is probably not a good example for this). With 'easier to understand' I mean that when looking at a bit of code I can tell what it does without having to know much about the context (typing, overloading). I did not mean to say that the code is prettier. Haskell code tends to be very pretty. It's probably difficult to strike the right balance between too little and too much overloading. Maybe OCaml does not allow enough overloading. For my taste typical Haskell code uses too much. But that's a matter of taste, I suppose.