yoneda

3 ms·

1.
by yoneda 3y ago
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 function-like things) is kind of obvious to anyone
2.
by yoneda 5y ago
> 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 the same if/else regardless if i
3.
by yoneda 5y ago
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 assure you that nullable types were noth
4.
by yoneda 5y ago
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. We many names for this c
5.
by yoneda 5y ago
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 programmer is then forced to manually reason about
6.
by yoneda 6y ago
Huh, so equality isn't transitive in Go. Yikes.
7.
by yoneda 6y ago
> 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 allow type invalid programs through, or it must prevent so
8.
by yoneda 6y ago
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 important: http://augustss.blogspot.com/2011/0
9.
by yoneda 6y ago
> 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 generally their main utility is that
10.
by yoneda 6y ago
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 any guesses about the author's experience
11.
by yoneda 6y ago
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 mailing lists). These are legitimate concerns, but the fac
12.
by yoneda 6y ago
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 places in the code that need to be updated when I
13.
by yoneda 6y ago
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.
14.
An Introduction to Session Types(wen.works)
1 points by yoneda 6y ago|0 comments