[chas]

I'm happy to hear that you found the first paper interesting!

While I agree that it is unlikely C and Python programmers will take up categorical abstractions any time soon, there is some interest from the JavaScript world. As an example of how this manifests this is a concurrency library (https://www.npmjs.com/package/fluture) and parser combinator library (https://www.npmjs.com/package/parsimmon) that are explicitly using built functors, applicatives and monads as programmatic abstractions. I don't think that this is going to be the mainstream of JavaScript in the near future, but it does suggest that some folks in the JavaScript world think that categorical abstractions are relevant to their practical work.

I also think it is the case that it is a bit strong to claim that Haskell was designed as a programming language for categorical abstractions because none of the ones that I mentioned were included in the initial design of the language. The Haskell 1.0 report[0] was published in 1990 and while it had typeclasses[1], the Functor and Monad typeclasses weren't added until the introduction of monadic IO for Haskell 1.3 in 1996[0]. Moggi's first paper on monads for computation[2] was in 1988, but to my knowledge no one involved in Haskell was introduced to it until several years later[4]. While applicative functors are in the middle of the popular hierarchy, they were the most recently introduced to functional programming. It took until 2008 for them to be explicitly identified as an interesting abstraction in "Applicative programming with effects"[3]. Making a language where programs compose nicely was an explicit design goal, so I don't think that it is a surprise that that's where category theory first landed as an explicit tool for programming abstractions. The categorical abstractions replaced non-categorical abstractions because they did a better job of solving the real problems that the people programming in these languages had, so I think it is a meaningful application of category theory to computing even if it hasn't happened yet in the mainstream of computer programming.

I agree with your assessment of HoTT as well. I'm not currently working on HoTT or on the use of homotopy and (co)homology as programming abstractions, so if they make some contributions to that on the way to their actual goals, I will be super happy.

[0] https://wiki.haskell.org/Language_and_library_specification [1] https://imgur.com/a/OS6yaSr [2] https://www.irif.fr/~mellies/mpri/mpri-ens/articles/moggi-co... [3] http://www.staff.city.ac.uk/~ross/papers/Applicative.pdf [4] https://www.microsoft.com/en-us/research/wp-content/uploads/...