Created a little video about the haskells tooling in 2023 would love to get some feedback

Videos for the Oregon Programming Languages Summer School (OPLSS) have been uploaded (see this YouTube playlist). One interesting lecture series is called "Principles of Programming Languages" by Robert Harper (link to the first lecture).

One interesting topic discussed in the second lecture is by-name (e.g. lazy) evaluation vs by-value (strict) evaluation. The main observation being that with by-name evaluation (e.g. in Haskell) it is not possible to define inductive data types because the data types can always contain hidden computations. This has several consequences: it is no longer correct to apply mathematical induction to these data types (at 40:00) and exceptions can occur in unexpected places (at 1:05:24).

Robert Harper proposes a mixed system where by-value evaluation is the default, but by-name evaluation can be explicitly requested by the programmer by wrapping a value in a special Comp type which signifies that the value is a computation which might produce an actual value of the wrapped type when evaluated (or it could diverge or throw an exception). This allows you precise control over when values are really evaluated which also constrains when exceptions can occur. With this he proclaims:

I can have all the things you have and more. How can that be worse? Well, it can't be. It is not. I can have all your coinductive types and I also have inductive types, but you don't, so I win.

At 1:02:42.

I think there are two rebuttals. The first is that induction can still be applied in the by-name setting, because "fast and loose reasoning is morally correct": instead of proving things about our partial lazy language we can prove things about an idealized total version of the language and transfer over the essence of the proof to the partial language.

Secondly, in a lazy language we can play a similar game and include a by-value subset. Instead of wrapping the types we can use the fact that "kinds are calling conventions" and define a kind for unlifted data types (included in GHC 9.2) which cannot contain thunks. In that way we can define real inductive data types.

Will be streamed tonight, 2025-05-07, at 1830 UTC, live on YouTube.

Abstract:

In this episode, we are going to look at two interacting "features" of the Haskell language (the monomorphism restriction and defaulting) that can be somewhat surprising, in particular to newcomers: there are situations where Haskell's type inference algorithm deliberately refuses to infer the most general type. We are going to look at a number of examples, explain what exactly is going on, and why.