yoneda

3 года назадdiscuss

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 who knows basic programming language theory (and many software engineers who use lambdas when they map over a list, for example).

The sentence before it about β-reduction is describing the rule for how to call a function, which we learned in high school as "plug-and-chug".

I think the confusion here might just be that the syntax is unfamiliar. You have probably seen these concepts before.

yoneda

5 лет назадdiscuss

> 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 it is a statement or a value. These are small touches, but they show attention to detail.

These are good ideas for sure, but they are bread and butter to anyone who is familiar with functional programming. The Lisp and ML families of languages have had them for many decades.

The fact that more languages _aren't_ like this is what's surprising to me, given how effective they are. I love that Rust is bringing them to the masses, but what on earth took the industry so long to accept them?

I guess the answer is that algebraic data types (inductively defined data) tend to be pitted against object-oriented programming (coinductively defined data), and object-oriented programming has dominated the industry for the past 3 decades. Some languages like Kotlin have tried to combine them, but personally I'd rather just embrace the former and relegate the latter to a seldomly-used design pattern, not a programming paradigm hardcoded into the language.

yoneda

5 лет назадdiscuss

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 nothing new even several decades ago. Perhaps you have only worked with object-oriented languages, where nullability is typically the default (which is a bad idea).

yoneda

5 лет назадdiscuss

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 concept, but "union" is not one of them, because a union allows for a non-empty intersection.

Under the hood, of course, they are implemented with C-style unions with fields sharing memory. But to conflate Rust's enums with how they are implemented is to disregard the extra safety that they provide.

yoneda

5 лет назадdiscuss

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 when a value can be null or not, and of course humans can easily make mistakes in doing so. This inevitably leads to NullPointerExceptions at runtime when a project becomes sufficiently complex. Type systems of "low risk" languages prevent such mistakes by offloading this kind of error-prone reasoning from the programmer to the machine.

yoneda

5 лет назадdiscuss

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

yoneda

5 лет назадdiscuss

> 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 some type valid programs (or both!).

No, you're mixing up concepts (consistency vs. soundness).

If a type system has non-normalizing types (or non-normalizing terms which appear in types), then it is inconsistent as a logic, which means that via Curry-Howard you can prove anything (ex falso quodlibet). Regarding incompleteness, any sufficiently expressive logic is incomplete per Gödel's first incompleteness theorem.

A type system which is inconsistent as a logic can still be sound as a type system. Soundness is the property that you described in your second paragraph (not letting "invalid" programs through). A simple example is System U. It's sound as a type system, but inconsistent as a logic. That means it works for programming, but not for proving.

yoneda

5 лет назадdiscuss

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/05/more-points-for-lazy-ev...

In particular, scroll down to the "Reuse" section. Lazy evaluation enables you to compose functions to build new functions with the right performance characteristics (constant factors aside), as in:

  any :: (a -> Bool) -> [a] -> Bool
  any p = or . map p

In an eager language, predicate `p` would have to be evaluated on every element in the list, even if the predicate is already satisfied after the first element. So instead you'd have to write this function in an ad hoc way with explicit recursion/looping, without being able to reuse the more primitive functions.

Of course, in an impure language, laziness can't be the default because you wouldn't be able to reason about when your side effects occur. But in my mind that's an argument for purity rather than an argument for eagerness.

BTW, comparing "strict" vs. "lazy" is a category error. The proper comparison would be either "strict" vs. "non-strict" or "eager" vs. "lazy". The former is in reference to the denotational semantics, whereas the latter characterizes the operational semantics.

yoneda

5 лет назадdiscuss

> 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 they check your reasoning, not come up with it for you.

yoneda

5 лет назадdiscuss

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; I stated my opinion of their opinion.

yoneda

5 лет назадdiscuss

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 fact that the author is happy with their decision despite these drawbacks is a testament to the language itself.

yoneda

5 лет назадdiscuss

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 add a new case to an algebraic data type. I know the article touches on this, but IMHO the author under-appreciates this important feature.

yoneda

5 лет назадdiscuss

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.

Submissions

An Introduction to Session Types

comments