5 ms·

Just in case you're wondering if it's just you: no it's not. PL theory seems almost deliberately designed to make even the most mundane things insanely complica

Just in case you're wondering if it's just you: no it's not. PL theory seems almost deliberately designed to make even the most mundane things insanely complicated and difficult to formulate or parse. I'm convinced much of the complexity is absolutely unwarranted and only serves to gate the field to newcomers. It makes things so much more painful than they need to be and turns what could be otherwise a potentially interesting topic into something that's more dry than cardboard.

throwawaygh 6y ago
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
- 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.
curryhoward 6y ago
I completely sympathize with the difficulty in understanding the notation and wish it were more accessible. I struggled with it for some time. But as someone who eventually learned it, I find it to be fairly sensible. What would be a better way to write the that judgment?
- mehrdadn 6y ago
  Well for starters I wouldn't have lost sleep over an arrow. (Even ⇒... blasphemy, I know.) Instead of, you know, a 3-way intersection sign making me wonder why I need to look both ways before crossing. Or, you know, they could just use a couple keywords from some actual programming languages from this century or get things going in plain English. Maybe "is" or "instanceof" or whatever. Then if you really, genuinely think your readers need to obsess with your formalism (which they very likely don't unless they have the basics down and are also planning to get a PhD in a proof theory-adjacent topic), you can switch from the 21st century English and math notation into cuneiform and hieroglyphics. (You can probably tell I didn't enjoy the experience...)
  - TheAsprngHacker 6y ago
    I think there's perhaps an analogy to be made between FP terminology that comes from math, and is therefore unfamiliar to non-math people, and type theory notation such as this. For example, an FP "functor" comes from the idea of (endo)functor from category theory, but people try to rename it (e.g. "Mappable") to make programmers understand it better. In the same way, you're proposing to rename the turnstile to an arrow symbol. The article "Why 'Functor' Doesn't Matter" [0] is relevant. In this case, the turnstile symbol comes from logic, and means "entails": Given the information on the left, you can derive the judgement on the right. There is an important distinction to be made between the turnstile and the double arrow [1]. For what it's worth, I haven't formally learned higher-level math, but I've been able to pick up type theory notation just by getting used to it. I can't necessarily explain how; it was just a gradual thing for me. [0] https://www.parsonsmatt.org/2019/08/30/why_functor_doesnt_matter.html https://www.parsonsmatt.org/2019/08/30/why_functor_doesnt_ma... [1] https://math.stackexchange.com/questions/286077/implies-rightarrow-vs-entails-models-vs-provable-vdash https://math.stackexchange.com/questions/286077/implies-righ...

throwawaygh 6y ago

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

curryhoward 6y ago

I completely sympathize with the difficulty in understanding the notation and wish it were more accessible. I struggled with it for some time. But as someone who eventually learned it, I find it to be fairly sensible. What would be a better way to write the that judgment?

mehrdadn 6y ago
Well for starters I wouldn't have lost sleep over an arrow. (Even ⇒... blasphemy, I know.) Instead of, you know, a 3-way intersection sign making me wonder why I need to look both ways before crossing. Or, you know, they could just use a couple keywords from some actual programming languages from this century or get things going in plain English. Maybe "is" or "instanceof" or whatever. Then if you really, genuinely think your readers need to obsess with your formalism (which they very likely don't unless they have the basics down and are also planning to get a PhD in a proof theory-adjacent topic), you can switch from the 21st century English and math notation into cuneiform and hieroglyphics. (You can probably tell I didn't enjoy the experience...)
- TheAsprngHacker 6y ago
  I think there's perhaps an analogy to be made between FP terminology that comes from math, and is therefore unfamiliar to non-math people, and type theory notation such as this. For example, an FP "functor" comes from the idea of (endo)functor from category theory, but people try to rename it (e.g. "Mappable") to make programmers understand it better. In the same way, you're proposing to rename the turnstile to an arrow symbol. The article "Why 'Functor' Doesn't Matter" [0] is relevant. In this case, the turnstile symbol comes from logic, and means "entails": Given the information on the left, you can derive the judgement on the right. There is an important distinction to be made between the turnstile and the double arrow [1]. For what it's worth, I haven't formally learned higher-level math, but I've been able to pick up type theory notation just by getting used to it. I can't necessarily explain how; it was just a gradual thing for me. [0] https://www.parsonsmatt.org/2019/08/30/why_functor_doesnt_matter.html https://www.parsonsmatt.org/2019/08/30/why_functor_doesnt_ma... [1] https://math.stackexchange.com/questions/286077/implies-rightarrow-vs-entails-models-vs-provable-vdash https://math.stackexchange.com/questions/286077/implies-righ...