6 ms·

His question is very valid. I got a math degree before I got a PhD in computer science, and this weird notation was the hardest part about the switch. The funny

His question is very valid. I got a math degree before I got a PhD in computer science, and this weird notation was the hardest part about the switch. The funny thing is, if you submit papers using a more sane and easier to understand notation (like, notation more close to a functional program) then computer scientists freak out and complain about notation. I predict this kind of notation to be dead within the next 20 years, its just too ugly.

mzl 14y ago
Is really sequent calculus (http://en.wikipedia.org/wiki/Sequent_calculus http://en.wikipedia.org/wiki/Sequent_calculus) that odd, that you never encountered it in your math studies? I personally find it quite easy to read, with nicely structured proofs.
- auggierose 14y ago
  Of course what is "easy" to read is always up to the individual to a certain degree. But this notation is used nowhere in math outside of logic. That should tell you something :-) Also in modern logic that is actually used in interactive proof assistants, this notation actually is not present any more, but then reintroduced when you write a paper about what you did!
  - tikhonj 14y ago
    Isn't this sort of notation used in Coq, at least when it displays your current goal? Admittedly, it's an ASCII bastardization of the notation, but it's the same idea.
    - auggierose 14y ago
      I don't mind writing instead of A => B => C the following: A B ---- C I just hate pressing everything into this style.
  - mzl 14y ago
    Well, of course the logic notation in question is used in mostly in logic contexts. In the same manner, as a student of logic I will not come across special notation from analysis. Although I am not working in that area any more, when I used interactive theorem provers the one I used mostly would present the proofs in Sequent calculus. It showcased a nice connection between the logical framework and a small step operational semantics reading of te formulas. In my view, it is important to understand the reasons for different fields choices of notation; it typically reveals interesting things about the fields in question. When starting out learning a new field, it often seems strange and un-intuitive, but after a while one starts to recognize that there are many valid reasons for why a certain style of notation is used. Of course, sometimes it is just an accident of history, and bad choices stick around :) I've hopped around quite a bit in my studies (semantics, formal methods, operations research, theoretical computer science, pure algebra, logic), and I always feel overwhelmed with new notations and concepts. Nowadays I tend to expect it when trying to learn something new.
more_original 14y ago
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 14y 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 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.
limmeau 14y ago
Have you got an example of a more sane and easier to understand notation for type inference rules? I find the horizontal-bar notation quite readable.
scott_s 14y ago
Can you provide any examples of the more sane notions? I'm very curious to compare.

mzl 14y ago

Is really sequent calculus (http://en.wikipedia.org/wiki/Sequent_calculus http://en.wikipedia.org/wiki/Sequent_calculus) that odd, that you never encountered it in your math studies? I personally find it quite easy to read, with nicely structured proofs.

auggierose 14y ago
Of course what is "easy" to read is always up to the individual to a certain degree. But this notation is used nowhere in math outside of logic. That should tell you something :-) Also in modern logic that is actually used in interactive proof assistants, this notation actually is not present any more, but then reintroduced when you write a paper about what you did!
- tikhonj 14y ago
  Isn't this sort of notation used in Coq, at least when it displays your current goal? Admittedly, it's an ASCII bastardization of the notation, but it's the same idea.
  - auggierose 14y ago
    I don't mind writing instead of A => B => C the following: A B ---- C I just hate pressing everything into this style.
- mzl 14y ago
  Well, of course the logic notation in question is used in mostly in logic contexts. In the same manner, as a student of logic I will not come across special notation from analysis. Although I am not working in that area any more, when I used interactive theorem provers the one I used mostly would present the proofs in Sequent calculus. It showcased a nice connection between the logical framework and a small step operational semantics reading of te formulas. In my view, it is important to understand the reasons for different fields choices of notation; it typically reveals interesting things about the fields in question. When starting out learning a new field, it often seems strange and un-intuitive, but after a while one starts to recognize that there are many valid reasons for why a certain style of notation is used. Of course, sometimes it is just an accident of history, and bad choices stick around :) I've hopped around quite a bit in my studies (semantics, formal methods, operations research, theoretical computer science, pure algebra, logic), and I always feel overwhelmed with new notations and concepts. Nowadays I tend to expect it when trying to learn something new.

more_original 14y ago

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 14y 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 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.

limmeau 14y ago

Have you got an example of a more sane and easier to understand notation for type inference rules? I find the horizontal-bar notation quite readable.

scott_s 14y ago

Can you provide any examples of the more sane notions? I'm very curious to compare.