4 ms·

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?

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.)
    - nyanpasu64 6y ago
      Why do they use |- instead of ->? Contrary to what others have said, I've only ever seen -> (implication) in my logic courses.
      - TheAsprngHacker 6y ago
        To my understanding: -> is material implication, so it is an operator of the object language. |- is part of the metalanguage that you use to reason about the object language. I am not that knowledgeable in logic, however.
- deleted 6y ago
  [deleted]
bjl 6y ago
I mean, yeah? I think you were trying to give an example of a hard to understand notation, but that page is relatively straightforward and concise. In fact, I can't think of a more straightforward (and non-ambiguous) way to express those concepts. Frankly, I'd expect any CS student at a decent university to be able to parse that page fairly easily.

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.)
  - nyanpasu64 6y ago
    Why do they use |- instead of ->? Contrary to what others have said, I've only ever seen -> (implication) in my logic courses.
    - TheAsprngHacker 6y ago
      To my understanding: -> is material implication, so it is an operator of the object language. |- is part of the metalanguage that you use to reason about the object language. I am not that knowledgeable in logic, however.
deleted 6y ago
[deleted]

bjl 6y ago

I mean, yeah? I think you were trying to give an example of a hard to understand notation, but that page is relatively straightforward and concise. In fact, I can't think of a more straightforward (and non-ambiguous) way to express those concepts. Frankly, I'd expect any CS student at a decent university to be able to parse that page fairly easily.