Hacker News Reader

Comment by curryhoward | Hacker News Reader

I completely sympathize with the difficulty in understanding the notation and wish it were more accessible. I struggled with it for some time. But as someone who eventually learned it, I find it to be fairly sensible. What would be a better way to write the that judgment?

View on HN

Well for starters I wouldn't have lost sleep over an arrow. (Even ⇒... blasphemy, I know.) Instead of, you know, a 3-way intersection sign making me wonder why I need to look both ways before crossing. Or, you know, they could just use a couple keywords from some actual programming languages from this century or get things going in plain English. Maybe "is" or "instanceof" or whatever. Then if you really, genuinely think your readers need to obsess with your formalism (which they very likely don't unless they have the basics down and are also planning to get a PhD in a proof theory-adjacent topic), you can switch from the 21st century English and math notation into cuneiform and hieroglyphics.

(You can probably tell I didn't enjoy the experience...)

I think there's perhaps an analogy to be made between FP terminology that comes from math, and is therefore unfamiliar to non-math people, and type theory notation such as this. For example, an FP "functor" comes from the idea of (endo)functor from category theory, but people try to rename it (e.g. "Mappable") to make programmers understand it better. In the same way, you're proposing to rename the turnstile to an arrow symbol.

The article "Why 'Functor' Doesn't Matter" [0] is relevant.

In this case, the turnstile symbol comes from logic, and means "entails": Given the information on the left, you can derive the judgement on the right. There is an important distinction to be made between the turnstile and the double arrow [1].

For what it's worth, I haven't formally learned higher-level math, but I've been able to pick up type theory notation just by getting used to it. I can't necessarily explain how; it was just a gradual thing for me.

[0] https://www.parsonsmatt.org/2019/08/30/why_functor_doesnt_ma...

[1] https://math.stackexchange.com/questions/286077/implies-righ...

I never got used to it is the thing. And I spent a heck of a lot of time on it. Yet I still look at a link like [1] and it may as well look like hieroglyphics to me. It's not that I can't parse it, it's just that it's like forcing me to do 500 push-ups in the process, to communicate something that shouldn't need more than 10 push-ups to warm up at most. Mathematical notation isn't all like this. Some stuff is actually intuitive. PL/proof theory notation just seems to be actively designed to make your life harder for some reason.

[1] https://www.google.com/books/edition/Advanced_Topics_in_Type...

(I just responded to your other comment pointing out this example right before reading this reply.)

Well lambda calculus always looked weird and unapproachable to me until I finally sat down one day and said "I'm going to finally learn this" and it was really, really easy after an hour or two of going through the notation. Sometimes math is like that.

I spent way more than an hour or two on this. And even by the end, it wasn't that I couldn't read it, it's that it was always a process of perpetual dragging me through molasses.

Reply on news.ycombinator.com