I disagree. This list contains lots of "Haskellisms" like monad transformers and lenses, which are effectively design patterns which have emerged over time as powerful ways to work within and around the idiosyncracies of Haskell.
We could argue all day about whether different 'families' of FP languages, like MLs, Lisps, Joys, etc. are more or less "advanced", so let's avoid any ambiguity and stick to the Haskell family of languages. Let's pick a language which is strictly more advanced and powerful than Haskell, such as Agda or Idris: not only can we implement all of the Haskell concepts in these languages (especially Idris, since we can toggle totality checking, rather than having to work around it), but the inclusion of dependent types lets us implement many more powerful patterns, and even simplifies many of the Haskell patterns (e.g. there's no need for hacks like singletons, normal functions can be used instead of type families, etc.).
So, given this vast landscape of new possibilities, which of the many 'design pattern' concepts have been chosen from these ultra-advanced, super-powerful languages?
> Dependent-Types, Singleton Types
That's it! Apparently the only new concept in these languages is the fact that dependent types exist; but even that's been constrained to a Haskell context, by lumping it in with singletons!
There's no mention of proof objects (de Bruijn criterion, etc.), computational content, erasure or proof irrelevance. No mention of tactic languages. They do give kinds and rank-n types, but they don't mention cumulative universes! No HoTT concepts are mentioned, like types-as-spaces, identity-as-paths or univalence. There's not even a mention of intensionality vs extensionality!
So what about skills? Surely there'd be specifics like modelling divergence co-inductively via Partial/Delay? Maybe propagating invariants with initial algebras, even if it's just a Vector example? What about something trivial, like heterogeneous equality?
> Use proof systems to formally prove properties of code.
> Use dependent-typing to prove more properties at compile time
Again, they've just listed that "these things exist", rather than giving any specifics whatsoever.
What about Haskell? Does that exist? You bet! It even has this thing called lenses; and not only do they exist, there are all sorts of nuanced proficiencies to them!
.... except! I really think Lenses are a concept orthogonal to Haskell. They can be implemented anywhere and usually make good sense. I think we have a long way to go before we've come to understand their best place in functional programming—especially construed as widely as you note.
We could argue all day about whether different 'families' of FP languages, like MLs, Lisps, Joys, etc. are more or less "advanced", so let's avoid any ambiguity and stick to the Haskell family of languages. Let's pick a language which is strictly more advanced and powerful than Haskell, such as Agda or Idris: not only can we implement all of the Haskell concepts in these languages (especially Idris, since we can toggle totality checking, rather than having to work around it), but the inclusion of dependent types lets us implement many more powerful patterns, and even simplifies many of the Haskell patterns (e.g. there's no need for hacks like singletons, normal functions can be used instead of type families, etc.).
So, given this vast landscape of new possibilities, which of the many 'design pattern' concepts have been chosen from these ultra-advanced, super-powerful languages?
> Dependent-Types, Singleton Types
That's it! Apparently the only new concept in these languages is the fact that dependent types exist; but even that's been constrained to a Haskell context, by lumping it in with singletons!
There's no mention of proof objects (de Bruijn criterion, etc.), computational content, erasure or proof irrelevance. No mention of tactic languages. They do give kinds and rank-n types, but they don't mention cumulative universes! No HoTT concepts are mentioned, like types-as-spaces, identity-as-paths or univalence. There's not even a mention of intensionality vs extensionality!
So what about skills? Surely there'd be specifics like modelling divergence co-inductively via Partial/Delay? Maybe propagating invariants with initial algebras, even if it's just a Vector example? What about something trivial, like heterogeneous equality?
> Use proof systems to formally prove properties of code.
> Use dependent-typing to prove more properties at compile time
Again, they've just listed that "these things exist", rather than giving any specifics whatsoever.
What about Haskell? Does that exist? You bet! It even has this thing called lenses; and not only do they exist, there are all sorts of nuanced proficiencies to them!