|
|
|
|
|
|
by spekcular
1929 days ago
|
|
|
Thanks. I ask that question a lot on here and I think your first bullet point is the first really substantive answer I've gotten. It's an interesting paper. I don't have time to read the rest of your links, unfortunately. However, I'm uncomfortable appealing to Haskell (or Ocaml/Scala) as evidence that category theory provides core abstractions for programming. It's true in this context, but only because Haskell was designed to make it true. I am skeptical that category theory has much to say about practical work in the languages used by most programmers, like C, javascript, and python. Anyway, about HoTT: I don't think it aims to accomplish what you want it to. Its primary concerns seem to be 1) formalized math and 2) serving as an alternative foundation to ZFC. But if it eventually does what you want, great! |
|
|
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/...