Suppose you define a typeclass that represents an algebraic structure (like Monoid for example). This structure has some associated algebraic laws. I understand that in Haskell, you can’t enforce that instances of your typeclass obey these algebraic laws. Are there any programming languages that do a better job than Haskell at enforcing algebraic laws in typeclass instances?
you can write proofs in agda about your code in relation to laws and then generate haskell from it. see https://github.com/agda/agda2hs
that’s the ideal, but it has a lot of restrictions
In general, there is a precise correspondence between variants of typed lambda calcului and what is known as the “internal logic” of categories which obey certain extra properties.
Here are some words:
Simply typed lambda calculus is the internal logic of Cartesian closed categories.
Linear typed lambda calculus is the internal logic of symmetric monoidal categories.
The “reason” for these correspondences is that one can use a category as an “abstract machine” to compile these lambda calculi into. For worked out examples, see the paper “compiling to categories” by conal Ellott. Finally, I apologise for not linking to anything, as I’m typing on my phone :)
Previous discussions include What category do Haskell types and functions live in? (2009) and Hask is not a category (2016).
Okay, so what programming language is category theory? Is there a language where you can define algebraic laws and enforce them?
None of them are “category theory” in the same way no programming languages are “linear algebra” or “complex analysis”.
Suppose you define a typeclass that represents an algebraic structure (like Monoid for example). This structure has some associated algebraic laws. I understand that in Haskell, you can’t enforce that instances of your typeclass obey these algebraic laws. Are there any programming languages that do a better job than Haskell at enforcing algebraic laws in typeclass instances?
Pretty much “any” dependently typed language should allow formulating those laws I presume: Coq, Agda, Idris, Lean, …
Idris does, but then you get into the general madness of formal verification.
you can write proofs in agda about your code in relation to laws and then generate haskell from it. see https://github.com/agda/agda2hs that’s the ideal, but it has a lot of restrictions
In general, there is a precise correspondence between variants of typed lambda calcului and what is known as the “internal logic” of categories which obey certain extra properties.
Here are some words:
Simply typed lambda calculus is the internal logic of Cartesian closed categories.
Linear typed lambda calculus is the internal logic of symmetric monoidal categories.
The “reason” for these correspondences is that one can use a category as an “abstract machine” to compile these lambda calculi into. For worked out examples, see the paper “compiling to categories” by conal Ellott. Finally, I apologise for not linking to anything, as I’m typing on my phone :)