Comment by TheAsprngHacker | Hacker News Reader

Comment by TheAsprngHacker | Hacker News Reader

Parent Full thread

TheAsprngHacker

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

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.

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

Why do they use |- instead of ->? Contrary to what others have said, I've only ever seen -> (implication) in my logic courses.

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.

Reply on news.ycombinator.com