7 ms·

Unfortunately you need to know type theory/logic notation in order to read this. Here's the English translation: - There is a variable called `x` in scope. -

Unfortunately you need to know type theory/logic notation in order to read this. Here's the English translation: - There is a variable called `x` in scope. - `x` is known to have type `A`. - `B` is a function that, when given `x` as an argument, returns a type. If this seems weird, it's because you need dependent types to even be able to say this. Honestly, this article is not written for programmers, and I don't know why it's on Hacker News right now. Most HN readers don't have the necessary background to follow it.

Gravityloss 6y ago
Thank you, it is easy to understand when explained like that! Maybe there could be a programming language where these concepts were used but slightly more explicitly, verbosely or in general easier to read fashion. A lot of successful languages are big on ergonomics or low barriers for entry.
- icen 6y ago
  If you're passingly familiar with Haskell or similar languages, you could give Idris a try. https://www.idris-lang.org/ https://www.idris-lang.org/
- kungato 6y ago
  Unfortunately, it often seems like "low barrier to entry" means "no prior effort invested" even if it means knowing basic logic notation which is taught in gymnasiums
  - Gravityloss 6y ago
    Hmm, is that symbol basic logic notation, and were you taught that symbol in high school? Which one of these? Do you type it often? https://en.wikipedia.org/wiki/Turnstile_(symbol) https://en.wikipedia.org/wiki/Turnstile_(symbol)
  - nyanpasu64 6y ago
    Is a gymnasium a school in Europe? It's an exercise facility in the USA. I've gone through high school and taken CS (and a bit of discrete math and logic) in college, and never seen the ⊢ symbol before.
    - mcaruso 6y ago
      > Is a gymnasium a school in Europe? It's an exercise facility in the USA. https://en.wikipedia.org/wiki/Gymnasium_(school) https://en.wikipedia.org/wiki/Gymnasium_(school) > I've gone through high school and taken CS (and a bit of discrete math and logic) in college, and never seen the ⊢ symbol before. Interesting. I was taught ⊢ first semester in CS in Logic class. Along with most other common logic notation.
    - throwawaygh 6y ago
      > Is a gymnasium a school in Europe? It's an exercise facility in the USA. https://en.wikipedia.org/wiki/Gymnasium_(Germany) https://en.wikipedia.org/wiki/Gymnasium_(Germany) And yes, teaching basic notation from mathematical logic is pretty standard in Gymnasium's. I've taught sequent calculi at US high school enrichment programs; honestly, the students get it perfectly fine. The notation is no more difficult to understand than a two column proof. It's always the teachers who struggle. Every attempt at math ed reform in the US meets that crux -- the teachers' and parents' willingness/ability to learn anything new is always massively over-estimated. The only way to teach real mathematics in US high schools is to smuggle it in through "enrichment" programs. > I've gone through high school and taken CS (and a bit of discrete math and logic) in college, and never seen the ⊢ symbol before. Discrete math courses are different from university to university; sometimes formal logic is covered, and sometimes it's more of an "introduction to basic proof techniques and combinatorics" course. A university course in logic should certainly have shown you a sequent calculus at some point. I'm actually confused about how you would fill a semester-long course on logic without a turnstile ever showing up. What notation were you using to write down your derivations? They used to say "the US has the best high schools in the world; unfortunately, they're called universities". But the universities have become so watered down that many Americans get university degrees without ever passing through an institution at the level of a good gymnasium.
- mehrdadn 6y ago
  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.
rustybolt 6y ago
Yes, god forbid if anyone tries to post something that needs some kind of knowledge!
mcphage 6y ago
So `A` is a type, and `Type` is a type?
- throwaway17_17 6y ago
  In this context, ‘A’ is an instance of Type, and ‘Type’ is the type of types (usually the term used for type of type is Kind). So while ‘x’ could be the value 7 and ‘A’ could be the type Int, the ‘B(x):Type’ means that the value of B(x) is some Type, could be Int, Char, Bool, etc.
  - mcphage 6y ago
    Thank you!
- curryhoward 6y ago
  `A` is a type, yes. Whether `Type` is a type depends on what type system you're working in. If `Type` is its own type, then it turns out you can use that to do infinite recursion (this is called Girard's paradox). Dependent types are often used for proving theorems, where infinite recursion corresponds to circular reasoning—a big no-no. So, in many dependently typed languages, `Type` is not its own type (instead, it's common to have an infinite tower of types: `42` has type `Int`, `Int` has type `Type0`, `Type0` has type `Type1`, `Type1` has type `Type2`, and so on). However, if the programming language is just used for programming and not for proving, then it's perfectly fine (and quite convenient) to have `Type` be its own type.
fastball 6y ago
I mean, the syntax really isn't that far off from how you might describe this in programming. To describe this with Python's type hints, for example, you would write this: def B(x: A) -> Type:

Gravityloss 6y ago

Thank you, it is easy to understand when explained like that! Maybe there could be a programming language where these concepts were used but slightly more explicitly, verbosely or in general easier to read fashion. A lot of successful languages are big on ergonomics or low barriers for entry.

icen 6y ago
If you're passingly familiar with Haskell or similar languages, you could give Idris a try. https://www.idris-lang.org/ https://www.idris-lang.org/
kungato 6y ago
Unfortunately, it often seems like "low barrier to entry" means "no prior effort invested" even if it means knowing basic logic notation which is taught in gymnasiums
- Gravityloss 6y ago
  Hmm, is that symbol basic logic notation, and were you taught that symbol in high school? Which one of these? Do you type it often? https://en.wikipedia.org/wiki/Turnstile_(symbol) https://en.wikipedia.org/wiki/Turnstile_(symbol)
- nyanpasu64 6y ago
  Is a gymnasium a school in Europe? It's an exercise facility in the USA. I've gone through high school and taken CS (and a bit of discrete math and logic) in college, and never seen the ⊢ symbol before.
  - mcaruso 6y ago
    > Is a gymnasium a school in Europe? It's an exercise facility in the USA. https://en.wikipedia.org/wiki/Gymnasium_(school) https://en.wikipedia.org/wiki/Gymnasium_(school) > I've gone through high school and taken CS (and a bit of discrete math and logic) in college, and never seen the ⊢ symbol before. Interesting. I was taught ⊢ first semester in CS in Logic class. Along with most other common logic notation.
  - throwawaygh 6y ago
    > Is a gymnasium a school in Europe? It's an exercise facility in the USA. https://en.wikipedia.org/wiki/Gymnasium_(Germany) https://en.wikipedia.org/wiki/Gymnasium_(Germany) And yes, teaching basic notation from mathematical logic is pretty standard in Gymnasium's. I've taught sequent calculi at US high school enrichment programs; honestly, the students get it perfectly fine. The notation is no more difficult to understand than a two column proof. It's always the teachers who struggle. Every attempt at math ed reform in the US meets that crux -- the teachers' and parents' willingness/ability to learn anything new is always massively over-estimated. The only way to teach real mathematics in US high schools is to smuggle it in through "enrichment" programs. > I've gone through high school and taken CS (and a bit of discrete math and logic) in college, and never seen the ⊢ symbol before. Discrete math courses are different from university to university; sometimes formal logic is covered, and sometimes it's more of an "introduction to basic proof techniques and combinatorics" course. A university course in logic should certainly have shown you a sequent calculus at some point. I'm actually confused about how you would fill a semester-long course on logic without a turnstile ever showing up. What notation were you using to write down your derivations? They used to say "the US has the best high schools in the world; unfortunately, they're called universities". But the universities have become so watered down that many Americans get university degrees without ever passing through an institution at the level of a good gymnasium.
mehrdadn 6y ago
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.

rustybolt 6y ago

Yes, god forbid if anyone tries to post something that needs some kind of knowledge!

mcphage 6y ago

So `A` is a type, and `Type` is a type?

throwaway17_17 6y ago
In this context, ‘A’ is an instance of Type, and ‘Type’ is the type of types (usually the term used for type of type is Kind). So while ‘x’ could be the value 7 and ‘A’ could be the type Int, the ‘B(x):Type’ means that the value of B(x) is some Type, could be Int, Char, Bool, etc.
- mcphage 6y ago
  Thank you!
curryhoward 6y ago
`A` is a type, yes. Whether `Type` is a type depends on what type system you're working in. If `Type` is its own type, then it turns out you can use that to do infinite recursion (this is called Girard's paradox). Dependent types are often used for proving theorems, where infinite recursion corresponds to circular reasoning—a big no-no. So, in many dependently typed languages, `Type` is not its own type (instead, it's common to have an infinite tower of types: `42` has type `Int`, `Int` has type `Type0`, `Type0` has type `Type1`, `Type1` has type `Type2`, and so on). However, if the programming language is just used for programming and not for proving, then it's perfectly fine (and quite convenient) to have `Type` be its own type.

fastball 6y ago

I mean, the syntax really isn't that far off from how you might describe this in programming. To describe this with Python's type hints, for example, you would write this: def B(x: A) -> Type: