4 ms·
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 notat
by 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 agoSorry. 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.