4 ms·

Most of the notation was invented either before or at the dawn of the computer age. It's also not particularly difficult to pick up. We teach basic sequent cal

Most of the notation was invented either before or at the dawn of the computer age. It's also not particularly difficult to pick up. We teach basic sequent calculus proofs to high schoolers in our summer program. If you can follow the two column proofs from high school geometry, then you can follow the notation used in standard programming language texts and papers.

mehrdadn 6y ago
> Most of the notation was invented either before or at the dawn of the computer age. I mean, what's why I said almost? > It's also not particularly difficult to pick up. Well, what I said was from personal experience, so maybe I'm just dumb... I'm not sure what else to tell you. Never in my life had so much of my continual struggling with a technical topic been solely due its pointlessly convoluted notation and roundabout communication as it had with PL theory.
- throwawaygh 6y ago
  Our highschoolers pick it up just fine, and are building complicated proofs within 3 lessons. That's not intended as any sort of attack, but it does make it hard for me to believe that the notation is particularly difficult to learn. Some things are difficult to learn without a good teacher. New notation is probably toward the top of that list. And there's really no way to study something like type systems without inventing some sort of notation. You can go back and read early papers in mathematical logic before the notation was invented. They take pages upon pages to communicate very simple things.
  - mehrdadn 6y ago
    So are you really telling me your high schoolers would've had no trouble with this [1] (pages 52, 58, etc.)? How do you think the average CS student would fare? Is this kind of notation genuinely as intuitive to you as other mathematical notation? My brain takes like O(n^3) to read this stuff and it's not the first time it's doing it either. [1] https://www.google.com/books/edition/Advanced_Topics_in_Types_and_Programming/A5ic1MPTvVsC?hl=en&gbpv=1&pg=PA52&printsec=frontcover https://www.google.com/books/edition/Advanced_Topics_in_Type...
    - TheAsprngHacker 6y ago
      For the record: I am a high school senior who learned about type theory in my free time. When I make this comment, I do not mean to boast, and I did invest a lot of time into learning TT. It's a coincidence, because I was just reading that chapter on pure type systems earlier today. Yes, I understand that notation. FWIW those aren't proofs; those are typing rules. The top-left rule on page 52 says that given that: - In context Gamma, T1 = T2 where both have kind * - If x : T1 is added to the context Gamma, K1 = K2 you can derive that in context Gamma, (x : T1) -> K1 = (x : T2) -> K2. A context is just a symbol table mapping names to types. Conventionally, uppercase gamma or uppercase delta is used. The uppercase pi is just another way of writing the dependent function type. If you think of types algebraically, dependent function types are similar to repeated multiplication, which use capital pi. It's similar to how summation uses capital sigma (and therefore the dependent sum type uses capital sigma as well).
      - mehrdadn 6y ago
        I appreciate that you're trying to help but I'm confused why you're constantly trying to explain the notation to me. I'm not saying I never understood the notation, I'm saying I very much did study and understand it, and found it incredibly convoluted, unintitive, unwarranted, and painful to deal with.
        TheAsprngHacker 6y ago
        Sorry. For me, when I see the rules, I just scan over them and figure out what it says. I think it just comes from seeing the notation many times - I guess when I first came across the notation (when learning about Hindley-Milner) it was completely foreign to me, but now I can recognize common patterns: Gamma |- exp : A This is a common pattern that says that exp has type A when the contents of Gamma are in scope. Gamma |- exp1 = exp2 : A This is a common pattern that says that exp1 and exp2 are equal terms of type A when the contents of Gamma are in scope. I've found that most type system rules follow the same format more or less. Sometimes, I do misread things. (When reading the page you linked, at first I mistook T1 = T2 for a type of kind *, then I realized I misunderstood it.)
jcranmer 6y ago
Mathematics does have a notation problem, and that means you effectively have to learn a foreign language to be able to understand it. And like foreign languages, learning it outside of a structured, classroom environment can be difficult to sustain. Even worse is the fact that while terminology like "monad" can easily be searched for to find its definition [1], how is one supposed to search for ℜ? Dismissing this foreign language aspect as easy to learn doesn't get to the heart of the matter. Is it really too much to be ask to be taught in vernacular English rather than foreign Church Latin, er, Mathematical Notation? [1] Assuming that you don't get an answer like "a monad is a monoid in the category of endofunctors," which unfortunately does tend to be the case for higher mathematical concepts.
- bjl 6y ago
  Vernacular English isn't capable of describing some concepts succinctly enough to be useful to mathematicians. If English was superior people would be using it. This 'argument' always just seems to be a thinly veiled excuse to avoid putting in the bare minimum effort required to understand a complicated topic.
- FridgeSeal 6y ago
  > Mathematics does have a notation problem An opinion that’s largely held by programmers and not people who actually do maths. You learn the symbols and notation as you go and it very quickly becomes understandable. I certainly Duns I have less issues understanding mathematical notation than I do reading some programming languages. > how is one supposed to search for ℜ? That’s chalkboard R, represents the real numbers. Searching “fancy R mathematics” (in Duck duck go) nets a page that explains what the chalkboard R, N, P, Q and C symbols all mean. > Is it really too much to be ask to be taught in vernacular English Mathematical texts used to be written in plain English without the notation, it’s honestly so, so much worse. It’s multitude more verbose and so much harder to grasp.
  - jcranmer 6y ago
    > An opinion that’s largely held by programmers and not people who actually do maths. The "people who actually do maths" will almost by definition exclude anyone who has issues understanding the notation. You need to look at the latter group of people to work out if the notation is unnecessarily obtuse. > it’s honestly so, so much worse. It’s multitude more verbose and so much harder to grasp. As a counterexample, consider the proof that undirected Hamiltonian cycles is NP-complete, by reduction from directed Hamiltonian cycles. Karp's original paper says literally just this: N = V × {0, 1, 2} A = {{<u,0>, <u,1>}, {<u,1>, <u,2>} | u ∈ V} ∪ {{<u,2>,<v,0>} | <u,v> ∈ E} By contrast, a vernacular English description would look like this: Replace every node in the directed graph with a set of three nodes in a line. Gather all the incoming edges to the first node, and all the outgoing edges to the last node. Every path that visits every node exactly once must reach the middle node by starting at the first node and going through to the last node, and thence to the first node of a corresponding subsequent node, so every Hamiltonian path in the undirected graph is a Hamiltonian path in its directed counterpart. More verbose, yes, but (IMO) easier to grasp.

mehrdadn 6y ago

> Most of the notation was invented either before or at the dawn of the computer age. I mean, what's why I said almost? > It's also not particularly difficult to pick up. Well, what I said was from personal experience, so maybe I'm just dumb... I'm not sure what else to tell you. Never in my life had so much of my continual struggling with a technical topic been solely due its pointlessly convoluted notation and roundabout communication as it had with PL theory.

throwawaygh 6y ago
Our highschoolers pick it up just fine, and are building complicated proofs within 3 lessons. That's not intended as any sort of attack, but it does make it hard for me to believe that the notation is particularly difficult to learn. Some things are difficult to learn without a good teacher. New notation is probably toward the top of that list. And there's really no way to study something like type systems without inventing some sort of notation. You can go back and read early papers in mathematical logic before the notation was invented. They take pages upon pages to communicate very simple things.
- mehrdadn 6y ago
  So are you really telling me your high schoolers would've had no trouble with this [1] (pages 52, 58, etc.)? How do you think the average CS student would fare? Is this kind of notation genuinely as intuitive to you as other mathematical notation? My brain takes like O(n^3) to read this stuff and it's not the first time it's doing it either. [1] https://www.google.com/books/edition/Advanced_Topics_in_Types_and_Programming/A5ic1MPTvVsC?hl=en&gbpv=1&pg=PA52&printsec=frontcover https://www.google.com/books/edition/Advanced_Topics_in_Type...
  - TheAsprngHacker 6y ago
    For the record: I am a high school senior who learned about type theory in my free time. When I make this comment, I do not mean to boast, and I did invest a lot of time into learning TT. It's a coincidence, because I was just reading that chapter on pure type systems earlier today. Yes, I understand that notation. FWIW those aren't proofs; those are typing rules. The top-left rule on page 52 says that given that: - In context Gamma, T1 = T2 where both have kind * - If x : T1 is added to the context Gamma, K1 = K2 you can derive that in context Gamma, (x : T1) -> K1 = (x : T2) -> K2. A context is just a symbol table mapping names to types. Conventionally, uppercase gamma or uppercase delta is used. The uppercase pi is just another way of writing the dependent function type. If you think of types algebraically, dependent function types are similar to repeated multiplication, which use capital pi. It's similar to how summation uses capital sigma (and therefore the dependent sum type uses capital sigma as well).
    - mehrdadn 6y ago
      I appreciate that you're trying to help but I'm confused why you're constantly trying to explain the notation to me. I'm not saying I never understood the notation, I'm saying I very much did study and understand it, and found it incredibly convoluted, unintitive, unwarranted, and painful to deal with.
      - TheAsprngHacker 6y ago
        Sorry. For me, when I see the rules, I just scan over them and figure out what it says. I think it just comes from seeing the notation many times - I guess when I first came across the notation (when learning about Hindley-Milner) it was completely foreign to me, but now I can recognize common patterns: Gamma |- exp : A This is a common pattern that says that exp has type A when the contents of Gamma are in scope. Gamma |- exp1 = exp2 : A This is a common pattern that says that exp1 and exp2 are equal terms of type A when the contents of Gamma are in scope. I've found that most type system rules follow the same format more or less. Sometimes, I do misread things. (When reading the page you linked, at first I mistook T1 = T2 for a type of kind *, then I realized I misunderstood it.)

jcranmer 6y ago

Mathematics does have a notation problem, and that means you effectively have to learn a foreign language to be able to understand it. And like foreign languages, learning it outside of a structured, classroom environment can be difficult to sustain. Even worse is the fact that while terminology like "monad" can easily be searched for to find its definition [1], how is one supposed to search for ℜ? Dismissing this foreign language aspect as easy to learn doesn't get to the heart of the matter. Is it really too much to be ask to be taught in vernacular English rather than foreign Church Latin, er, Mathematical Notation? [1] Assuming that you don't get an answer like "a monad is a monoid in the category of endofunctors," which unfortunately does tend to be the case for higher mathematical concepts.

bjl 6y ago
Vernacular English isn't capable of describing some concepts succinctly enough to be useful to mathematicians. If English was superior people would be using it. This 'argument' always just seems to be a thinly veiled excuse to avoid putting in the bare minimum effort required to understand a complicated topic.
FridgeSeal 6y ago
> Mathematics does have a notation problem An opinion that’s largely held by programmers and not people who actually do maths. You learn the symbols and notation as you go and it very quickly becomes understandable. I certainly Duns I have less issues understanding mathematical notation than I do reading some programming languages. > how is one supposed to search for ℜ? That’s chalkboard R, represents the real numbers. Searching “fancy R mathematics” (in Duck duck go) nets a page that explains what the chalkboard R, N, P, Q and C symbols all mean. > Is it really too much to be ask to be taught in vernacular English Mathematical texts used to be written in plain English without the notation, it’s honestly so, so much worse. It’s multitude more verbose and so much harder to grasp.
- jcranmer 6y ago
  > An opinion that’s largely held by programmers and not people who actually do maths. The "people who actually do maths" will almost by definition exclude anyone who has issues understanding the notation. You need to look at the latter group of people to work out if the notation is unnecessarily obtuse. > it’s honestly so, so much worse. It’s multitude more verbose and so much harder to grasp. As a counterexample, consider the proof that undirected Hamiltonian cycles is NP-complete, by reduction from directed Hamiltonian cycles. Karp's original paper says literally just this: N = V × {0, 1, 2} A = {{<u,0>, <u,1>}, {<u,1>, <u,2>} | u ∈ V} ∪ {{<u,2>,<v,0>} | <u,v> ∈ E} By contrast, a vernacular English description would look like this: Replace every node in the directed graph with a set of three nodes in a line. Gather all the incoming edges to the first node, and all the outgoing edges to the last node. Every path that visits every node exactly once must reach the middle node by starting at the first node and going through to the last node, and thence to the first node of a corresponding subsequent node, so every Hamiltonian path in the undirected graph is a Hamiltonian path in its directed counterpart. More verbose, yes, but (IMO) easier to grasp.