[jameshart]

Thanks for responding - just to reiterate, I am a big fan of this original post, and indeed your other writing - my only critique here is that I'm looking for ways to make the insights in them more transparent to, particularly, people who aren't well-positioned to analogize how to apply Haskell concepts to other languages.

I see you read 'narrowing type conversions' rather literally in my statement - that might be my making my own analogy that doesn't go over very well. I literally mean using 'constructive modeled types' is a way to create true type-narrowing conversions, in the sense that a 'nonempty list' is a narrower type than 'list', or 'one to five' is a narrower type than 'int'.

[lexi-lambda]

You know what, you’re right—I misread your original comment. I was just going through this thread and replying to a number of comments making that particular misconception, since it is particularly common, but upon taking a closer look, you were saying something else. I apologize!

As for the difficulty in applying these ideas in other languages, I am sympathetic. The problem I always run into is that there is necessarily a tension between (a) presentations that are accessible to working programmers, (b) explanations that distill the essential ideas so they aren’t coupled to particular languages or language features, and (c) examples small enough to be clarifying and to fit in a blog post. Haskell is certainly not the best choice along that first axis, but it is quite exceptionally good along the second two.

For a somewhat concrete example of what I mean, see this comment I wrote a few years ago that translates the NonEmpty example into Java: https://news.ycombinator.com/item?id=21478322 I think the added verbosity and added machinery really does detract significantly from understanding. Meanwhile, a TypeScript translation would make a definition like this one quite tempting:

    type NonEmpty<T> = [T, ...T[]]

However, I find this actually obscures application of the technique because it doesn’t scale to more complex examples (for the reasons I discussed at quite some length in https://lexi-lambda.github.io/blog/2020/08/13/types-as-axiom...).

There are probably ways to thread this needle, but I don’t think any one “solution” is by any means obviously the best. I think the ways that other people have adapted the ideas to their respective ecosystems is probably a decent compromise.