3 ms·
> Furthermore, even in Haskell, there is no such thing as the category of Haskell types[0] (because of things like divergence and partiality). Divergence and p
by ebingdom 5y ago
> Furthermore, even in Haskell, there is no such thing as the category of Haskell types[0] (because of things like divergence and partiality).
Divergence and partiality can easily be modeled by the category of complete partial orders and Scott-continuous maps. This is what you learn in, e.g., a course on domain theory and/or denotational semantics.
Andrej Bauer is mainly arguing that Hask isn't a category because no one has formally specified it. For example, we would need to come up with a policy on when two arrows are considered equal, and it's not clear what that notion of equality should be.
- siraben 5y agoRight, domain theory and denotational semantics let you talk about ⊥ in an order-theoretic setting, and I think it's also rich in connections between topology and lambda calculus. Though it might be the case that if functors already pose a pedagogical conundrum for programmers, Scott-continuity might be even harder to get across. A quote from Bauer's post is particularly relevant: > [I am arguing against] the fact that some people find it acceptable to defend broken mathematics on the grounds that it is useful. Non-broken mathematics is also useful, as well as correct. Good engineers do not rationalize broken math by saying “life is tough”.
- catgary 5y agoBrauer has clearly had a different experience with classical mechanics and engineering physics courses than I did…