3 ms·
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
by 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 agoWhy do they use |- instead of ->? Contrary to what others have said, I've only ever seen -> (implication) in my logic courses.
- TheAsprngHacker 6y agoTo 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.