Viewing profile — yoneda

The "obvious" observation from the article is: > Obviously, λx.M should be seen as a sort of function The fact that lambdas can be seen as a syntax for describing functions (or fun…

> Quite a few times I was surprised that Rust breaks with some old patterns that were copied over and over in the last 50 years or so. For example: "match" instead of "switch", or …

Yes, Java's type system "so weak". Just because many other popular languages have similarly weak type systems doesn't make them less weak. Also, as a long-time Haskell user, I can …

Logically speaking, Rust's "enums" are neither enums (in the traditional sense) nor unions. They are tagged unions / disjoint unions / variants / coproducts / algebraic data types.…

I generally agree, except the part about the low risk of runtime surprises. Java's type system is so weak that it doesn't even prevent null from inhabiting almost every type. The p…

Huh, so equality isn't transitive in Go. Yikes.

> It’s important to understand that this is a big problem. If a type system is Turing complete, than it either has to be inconsistent or incomplete. In other words it either must a…

This is a great writeup, and I just want to offer a counterpoint regarding the eager vs. lazy trade-offs. I found this article really helpful for explaining why laziness is importa…

> but can't typically "find their own way" to the proof of a theorem That's not what proof assistants like Lean and Coq are about. Sure, they can automate some trivial things, but …

Seems like you didn't read my comment in its entirety. I acknowledged that the article discusses exhaustiveness checking, so you don't need to point that out to me. I didn't make a…

One of my favorite qualities of the Haskell community is how honest they are about the weaknesses of the ecosystem (we often discuss issues like these, e.g., on r/haskell or in mai…

The primary advantage of proper pattern matching compared to ad hoc "instanceof" checks is exhaustiveness checking. I love the comfort in knowing the compiler will tell me all the …

On the contrary, I find myself more productive in languages that do not have pervasive null because then I don't have to manually reason about which values might be null.