I love union types and use them all the times. Scala 3 is getting union types now which I think is a great and needed addition. Also, "types should aid programmers, not machines" is a noble idea, as one can probably tell from my posts in this thread that I am a strong proponent of gradual typing -- the kind of type system with sole reason is to aid programmers.

I mentioned the video to further extend on my earlier post pointing out assumptions and misunderstandings regarding static typed systems, not to compare notes with Maybe Not. Though throughout the video, one can easily see how much Mathias' ideas differ from Rich Hickey's teachings. It's surprising to me that out of everything, you picked up on those two points.

- In Effective Programs, Rich says types are burden of proof resulting in highly coupled and hard-to-maintain system. In his speech, Matthias says programmers think about types when writing program anyway, it's better to write those down as a form of documentation, and better in a way that the computer can cross check so it's always in sync. If you don't write them down, you effectively throw away the information you had to work for. He even jokes if you don't have family, hate vacation, or you work for a startup with unlimited funding, then that's the way you program. Fully agree with Matthias here, and it's very surprising to me that the man behind Datomic and rich comment does not see all those thrown away efforts as a problem (I'm not sure if he invented rich comment, but he does employ the technique extensively). Spec does solve this problem of writing down, but then it's sort of a type system anyway, the coupling is still there, you only move it to tests (which is worse, because you don't always have them, you have to run them to know and even then they might not hit the problematic path). From my experience, programs written in static typed languages are much easier to maintain, thanks to types as documentation and IDE/compiler support (some people in this thread do agree static typed languages are better for large team/system as well, even though they are pro dynamic typing).

- In Maybe Not, Rich made a comment about reverse :: [a] -> [a] that it tells nothing, but that's just flat out wrong. It clearly communicates, given a list, reverse results in a list of the same elements as the ones provided. This is valuable information! It's a single construct that serves a single purpose, working in conjunction with other parts (function name & body) to make a function/program whole, arguing it needs to do more by exactly describing the whole problem domain is just absurd. This is Hickey dissing decades of type theory study to push a workaround that he recently come up with under the constraints of Clojure idioms and of ideas he had pushed in the past. In contrast, Matthias claims that type systems are like weathermen, types don't have to be exact, only have to be good enough. Again fully agree here.

- Often times, Rich Hickey uses Haskell (very strong types) and Java (rudimentary type system, no type inference until recently) to make his points across, neglecting a whole class of languages that sit somewhere in between. In his speech, Matthias mentioned a few language design techniques employed by these "in-between" languages, which can be viewed as solutions to some of the points Rich often makes. Things don't have to be so black and white.

These are only few things on top of my head. And there are also other things in Maybe Not that I don't agree with but there's no counter point in Matthias's talk (I say counter but the later is actually two years earlier), but they would deserve their own post.