#### Howdy, Stranger!

It looks like you're new here. If you want to get involved, click one of these buttons!

Options

# Mac Lane Exercise II.3.2

edited January 2020

Show that the product of two preorders is a preorder.

• Options
1.
edited February 2020

Let $$\mathcal{P} := \langle P, \preceq_P \rangle$$ and $$\mathcal{Q} := \langle Q, \preceq_Q \rangle$$. Define $$\mathcal{P} \times \mathcal{Q} := \langle P \times Q, \preceq_{P\times Q} \rangle$$ where:

$(a,b) \preceq_{P\times Q} (c,d) \text{ if and only if } a \preceq_P c \text{ and } b \preceq_Q d$

We need to check reflexivity and transitivity.

Reflexivity - Since $$a \preceq_P a$$ and $$b \preceq_Q b$$ then $$(a,b) \preceq_{P \times Q} (a,b)\ \ \ \Box$$

Transitivity - Let $$(a,b) \preceq_{P \times Q} (c,d)$$ and $$(c,d) \preceq_{P \times Q} (e,f)$$. Then we have $$a \preceq_P c \preceq_P e$$ and $$b \preceq_Q d \preceq_Q f$$.

Since $$\preceq_P$$ and $$\preceq_Q$$ are transitive, then $$a \preceq_P e$$ and $$b \preceq_P f$$.

Hence $$(a,b) \preceq_{P \times Q} (e,f)\ \ \ \Box$$

We can also show that this product order is the product in the category of preorders where the morphisms are order-preserving maps.

In fact, the category of preorders is bicartesian closed. There's an initial preorder, a final preorder, products and coproducts and an exponential. If this is interesting we can go into this construction and the proof.

Comment Source:Let \$$\mathcal{P} := \langle P, \preceq_P \rangle\$$ and \$$\mathcal{Q} := \langle Q, \preceq_Q \rangle\$$. Define \$$\mathcal{P} \times \mathcal{Q} := \langle P \times Q, \preceq_{P\times Q} \rangle\$$ where: \$(a,b) \preceq_{P\times Q} (c,d) \text{ if and only if } a \preceq_P c \text{ and } b \preceq_Q d \$ We need to check reflexivity and transitivity. _Reflexivity_ - Since \$$a \preceq_P a\$$ and \$$b \preceq_Q b\$$ then \$$(a,b) \preceq_{P \times Q} (a,b)\ \ \ \Box\$$ _Transitivity_ - Let \$$(a,b) \preceq_{P \times Q} (c,d)\$$ and \$$(c,d) \preceq_{P \times Q} (e,f)\$$. Then we have \$$a \preceq_P c \preceq_P e\$$ and \$$b \preceq_Q d \preceq_Q f\$$. Since \$$\preceq_P\$$ and \$$\preceq_Q\$$ are transitive, then \$$a \preceq_P e\$$ and \$$b \preceq_P f\$$. Hence \$$(a,b) \preceq_{P \times Q} (e,f)\ \ \ \Box\$$ -------------------------------- We can also show that this product order is the product in the category of preorders where the morphisms are order-preserving maps. In fact, the category of preorders is _bicartesian closed_. There's an initial preorder, a final preorder, products and coproducts and an exponential. If this is interesting we can go into this construction and the proof.
• Options
2.
edited February 2020

Hi @MatthewDoty,

Yes, it's interesting, please go on. Thanks

Comment Source:Hi @MatthewDoty, Yes, it's interesting, please go on. Thanks
• Options
3.
edited February 2020

Okay, let's first prove that the product preorder is the Product in the category of preorders.

The classic presentation of products introduces them with this commuting diagram (which I've taken from wikipedia):

Let's turn this into some equational laws. I'll be roughly following Conal Elliot's Compiling to Categories (2017) and John Wiegley's formalization in Coq

A Product $$(\times)$$ for a category $$\mathcal{C}$$ has three components:

• A family of morphisms $$\pi_1 : A \times B \to A$$
• Another family of morphisms $$\pi_2 : A \times B \to A$$
• A unique morphism composition operation $$(\triangle):(A \to B) \Rightarrow (A \to C) \Rightarrow A \to B \times C$$ obeying the laws below

(The reason for the two kinds of arrows is to distinguish between morphisms in the Category and functions in the meta-language. See the Conal Elliot and John Wiegley linked above for formulations with Haskell and Coq as the meta languages, respectively.)

I've seen $$\pi_1$$ and $$\pi_2$$ called projections. John Wiegley refers to $$(\triangle)$$ as "fork" in his code, which seems a fine name to me.

A product obeys the following laws:

$\pi_1 \cdot f \triangle g = f\\ \pi_2 \cdot f \triangle g = g\\ (\pi_1 \cdot f) \triangle (\pi_2 \cdot f) = f$

In Haskell, using itself as its own meta-language, we have $$(\times)$$ is the type constructor (,), $$\pi_1$$ is fst :: (a,b) -> a and $$\pi_2$$ is snd :: (a,b) -> b. Lastly, we have $$(\triangle)$$ is Control.Arrow.(&&&). You can check that fst . (f &&& g) = f and snd . (f &&& g) = g by looking at the instantiation of the Arrow class for (->) in base.

So let's extend the definition of the product preorder $$\mathcal{P} \times \mathcal{Q}$$ to a product by defining $$\pi_1$$, $$\pi_2$$ and $$(\triangle)$$.

• $$\pi_1$$ is the map $$(a,b) \mapsto a$$
• $$\pi_2$$ is the map $$(a,b) \mapsto b$$
• $$(\triangle)$$ is the map $$f \mapsto g \mapsto (a \mapsto (f (a), g (a)))$$

These definitions are very similar to the Haskell correlates. Checking the laws are obeyed is just evaluating the functions.

It's a bit less trivial to check that $$\pi_1$$, $$\pi_2$$ and $$f \triangle g$$ are all morphisms. In this case, we need them to be order preserving maps.

• Suppose that $$(a,b) \preceq_{P \times Q} (c,d)$$. Then $$a \preceq_{P} c$$ by definition, hence $$\pi_1(a,b) \preceq \pi_1(c,d)$$
• The proof that $$\pi_2$$ is order preserving is similar to the proof of $$\pi_1$$ above.
• Let $$f : A \to B$$ and $$g: A \to C$$ be order preserving maps. Moreover, let $$a \preceq_A b$$. We need to show $$(f \triangle g)(a) \preceq_{B \times C} (f \triangle g)(b)$$. This is the same thing as showing $$(f (a), g(a)) \preceq_{B \times C} (f(b), g(b))$$. But since $$f$$ and $$g$$ are both order preserving, we know that $$f(a) \preceq_B f(b)$$ and $$g(a) \preceq_C g(b)$$, hence we have the result by definition.

I'll try to find the time next week to show the other properties that make $$PreOrder$$ Bicartesian closed. It's my opinion that it's important to learn the algebraic formulations of the category theoretic laws rather than just the traditional commuting diagrams. But thankfully we can always find correlates in Haskell, since (->) is also Bicartesian closed.

I might do a little less proving, though. I think if we want to get serious about writing proofs we should consider formulating this stuff in Coq or Lean. These systems really drive home the connection between CT and programming.

[EDIT: Adding third law for products, fixing up proper usage of terms.] [EDIT2: Adding uniqueness constraint]

Comment Source:Okay, let's first prove that the product preorder is the Product in the category of preorders. The classic presentation of products introduces them with this commuting diagram (which I've taken from [wikipedia](https://en.wikipedia.org/wiki/Product_(category_theory))): ![Product](https://upload.wikimedia.org/wikipedia/commons/b/b2/CategoricalProduct-03.png) Let's turn this into some equational laws. I'll be roughly following Conal Elliot's [Compiling to Categories (2017)](http://conal.net/papers/compiling-to-categories/compiling-to-categories.pdf) and John Wiegley's [formalization in Coq](https://github.com/jwiegley/category-theory/blob/master/Structure/Cartesian.v) A _Product_ \$$(\times)\$$ for a category \$$\mathcal{C}\$$ has three components: - A family of morphisms \$$\pi_1 : A \times B \to A\$$ - Another family of morphisms \$$\pi_2 : A \times B \to A\$$ - A unique _morphism composition_ operation \$$(\triangle):(A \to B) \Rightarrow (A \to C) \Rightarrow A \to B \times C\$$ obeying the laws below (The reason for the two kinds of arrows is to distinguish between morphisms in the Category and functions in the meta-language. See the Conal Elliot and John Wiegley linked above for formulations with Haskell and Coq as the meta languages, respectively.) I've seen \$$\pi_1\$$ and \$$\pi_2\$$ called _projections_. John Wiegley refers to \$$(\triangle)\$$ as _"fork"_ in his code, which seems a fine name to me. A product obeys the following laws: \$\pi_1 \cdot f \triangle g = f\\\\ \pi_2 \cdot f \triangle g = g\\\\ (\pi_1 \cdot f) \triangle (\pi_2 \cdot f) = f \$ In Haskell, using itself as its own meta-language, we have \$$(\times)\$$ is the type constructor (,), \$$\pi_1\$$ is fst :: (a,b) -> a and \$$\pi_2\$$ is snd :: (a,b) -> b. Lastly, we have \$$(\triangle)\$$ is [Control.Arrow.(&&&)](https://hackage.haskell.org/package/base-4.12.0.0/docs/Control-Arrow.html#v:-38--38--38-). You can check that fst . (f &&& g) = f and snd . (f &&& g) = g by looking at the [instantiation of the Arrow class for (->) in base](https://hackage.haskell.org/package/base-4.12.0.0/docs/src/Control.Arrow.html#line-143). -------------------------------- So let's extend the definition of the product preorder \$$\mathcal{P} \times \mathcal{Q}\$$ to a product by defining \$$\pi_1\$$, \$$\pi_2\$$ and \$$(\triangle)\$$. - \$$\pi_1\$$ is the map \$$(a,b) \mapsto a\$$ - \$$\pi_2\$$ is the map \$$(a,b) \mapsto b\$$ - \$$(\triangle)\$$ is the map \$$f \mapsto g \mapsto (a \mapsto (f (a), g (a)))\$$ These definitions are _very_ similar to the Haskell correlates. Checking the laws are obeyed is just evaluating the functions. It's a bit less trivial to check that \$$\pi_1\$$, \$$\pi_2\$$ and \$$f \triangle g\$$ are all morphisms. In this case, we need them to be _order preserving maps_. - Suppose that \$$(a,b) \preceq_{P \times Q} (c,d)\$$. Then \$$a \preceq_{P} c\$$ by definition, hence \$$\pi_1(a,b) \preceq \pi_1(c,d)\$$ - The proof that \$$\pi_2\$$ is order preserving is similar to the proof of \$$\pi_1\$$ above. - Let \$$f : A \to B\$$ and \$$g: A \to C\$$ be order preserving maps. Moreover, let \$$a \preceq_A b\$$. We need to show \$$(f \triangle g)(a) \preceq_{B \times C} (f \triangle g)(b)\$$. This is the same thing as showing \$$(f (a), g(a)) \preceq_{B \times C} (f(b), g(b))\$$. But since \$$f\$$ and \$$g\$$ are both order preserving, we know that \$$f(a) \preceq_B f(b)\$$ and \$$g(a) \preceq_C g(b)\$$, hence we have the result by definition. I'll try to find the time next week to show the other properties that make \$$PreOrder\$$ Bicartesian closed. It's my opinion that it's important to learn the algebraic formulations of the category theoretic laws rather than just the traditional commuting diagrams. But thankfully we can always find correlates in Haskell, since (->) is also Bicartesian closed. I might do a little less proving, though. I think if we want to get serious about writing proofs we should consider formulating this stuff in Coq or Lean. These systems really drive home the connection between CT and programming. [EDIT: Adding third law for products, fixing up proper usage of terms.] [EDIT2: Adding uniqueness constraint]
• Options
4.
edited February 2020

Okay, so far we've shown that $$PreOrder$$ has products. We can go a bit further to show it's a Cartesian category.

In order for a category to be a Cartesian category, it must have a Cartesian category which is Monoidal. In this case we just need an object $$\mathbf{1}$$ which obeys the following axiom:

$X \times \mathbf{1} \simeq X$

Here $$\mathbf{1}$$ is called a unit.

Here I'm following Hinze's axiomatization of a Bicartesian closed category in Reason Isomorphically! (2010). In the general case of Monoidal categories the axioms are more complicated.

Before looking at $$PreOrder$$, lets see how $$Hask$$ is a Cartesian category.

In the case of Hask, the unit $$\mathbf{1}$$ is (). In order to show this, we need to find an isomorphism between (a,()) and a. The following two functions do the trick:

  pairUnit :: a -> (a,())
pairUnit x = (x,())

unpairUnit :: (a,()) -> a
unpairUnit (x,()) = x


In $$PreOrder$$, $$\mathbf{1}$$ is the preorder with just one element. In this setting we take analogues of pairUnit and unpairUnit and observer they are order-preserving.

Comment Source:Okay, so far we've shown that \$$PreOrder\$$ has products. We can go a bit further to show it's a _Cartesian category_. In order for a category to be a Cartesian category, it must have a Cartesian category which is [_Monoidal_](https://en.wikipedia.org/wiki/Monoidal_category). In this case we just need an object \$$\mathbf{1}\$$ which obeys the following axiom: \$X \times \mathbf{1} \simeq X \$ Here \$$\mathbf{1}\$$ is called a _unit_. Here I'm following Hinze's axiomatization of a Bicartesian closed category in [Reason Isomorphically! (2010)](http://www.cs.ox.ac.uk/people/daniel.james/iso/iso.pdf). In the general case of Monoidal categories the axioms are more complicated. ------------------------------- Before looking at \$$PreOrder\$$, lets see how \$$Hask\$$ is a Cartesian category. In the case of Hask, the unit \$$\mathbf{1}\$$ is (). In order to show this, we need to find an isomorphism between (a,()) and a. The following two functions do the trick: pairUnit :: a -> (a,()) pairUnit x = (x,()) unpairUnit :: (a,()) -> a unpairUnit (x,()) = x ------------------------------- In \$$PreOrder\$$, \$$\mathbf{1}\$$ is the preorder with just one element. In this setting we take analogues of pairUnit and unpairUnit and observer they are order-preserving.
• Options
5.

@MatthewDoty wrote:

In fact, the category of preorders is bicartesian closed. There's an initial preorder, a final preorder, products and coproducts and an exponential. If this is interesting we can go into this construction and the proof.

So:

• Initial preorder = empty set
• Final preorder = terminal preorder = singleton set

What are the exponential of two preorders? I'm guessing that $$A^B$$ is the set of order preserving maps from $$B$$ to $$A$$, where the maps are ordered by pointwise comparisons: $$f \le g$$ means $$f(x) \le g(x)$$ for all $$x$$.

Guessing again, is the coproduct formed by taking the disjoint union of the underlying sets, and the disjoint union of the ordering relations?

Comment Source:@MatthewDoty wrote: > In fact, the category of preorders is _bicartesian closed_. There's an initial preorder, a final preorder, products and coproducts and an exponential. If this is interesting we can go into this construction and the proof. So: * Initial preorder = empty set * Final preorder = terminal preorder = singleton set What are the exponential of two preorders? I'm guessing that \$$A^B\$$ is the set of order preserving maps from \$$B\$$ to \$$A\$$, where the maps are ordered by pointwise comparisons: \$$f \le g\$$ means \$$f(x) \le g(x)\$$ for all \$$x\$$. Guessing again, is the coproduct formed by taking the disjoint union of the underlying sets, and the disjoint union of the ordering relations? 
• Options
6.
edited February 2020

Those seem like such natural candidates that it would be surprising if it weren't them. I know it's just a homework exercise to draw the diagrams and check the claims. Maybe tomorrow when I'm feeling more fresh. I had a professor in college who would scribble all kinds of long detailed computations on the board. One day he said: when in doubt, do the dog work.

Since I'm feeling tired and lazy tonight, anyone feel free to cut in and prove or disprove my hypotheses.

Comment Source:Those seem like such natural candidates that it would be surprising if it weren't them. I know it's just a homework exercise to draw the diagrams and check the claims. Maybe tomorrow when I'm feeling more fresh. I had a professor in college who would scribble all kinds of long detailed computations on the board. One day he said: when in doubt, do the dog work. Since I'm feeling tired and lazy tonight, anyone feel free to cut in and prove or disprove my hypotheses.
• Options
7.
edited February 2020

What are the exponential of two preorders? I'm guessing that $$A^B$$ is the set of order preserving maps from $$B$$ to $$A$$, where the maps are ordered by pointwise comparisons: $$f \leq g$$ means $$f(x) \leq g(x)$$ for all $$x$$. Guessing again, is the coproduct formed by taking the disjoint union of the underlying sets, and the disjoint union of the ordering relations?

From my understanding this is all correct.

I know it's just a homework exercise to draw the diagrams and check the claims.

So... drawing and scanning diagrams by hand is a lot of work, or making them with TikZ and exporting them to png and so on (this forum doesn't support svgs sadly).

I find the equational approach is a bit easier online, and it often corresponds super nicely with Haskell.

So let's start with coproducts. They are very similar to the products. They have morphisms $$i_1 : A \to A + B$$ and $$i_2 : B \to A + B$$ and morphism composition $$(\nabla) : (A \to C) \Rightarrow (B \to C) \Rightarrow A + B \to C$$. I'll come back later and write the equations out unless someone else wants to. The analogues in Haskell can all be found in the Prelude, unlike products where we need Control.Arrow.(&&&).

For exponentials, one way of defining them is via the adjunction $$\bullet \times A \dashv \bullet^A$$. In this case we would want to show, for all $$B$$:

$Hom(- \times A, B) \simeq Hom(-, B^A)$

Finally, it's possible to define coproducts via an adjunction and exponentials via equations. These aren't as natural in Haskell, however.

I'll come back later and chip away at these proofs @DavidTanzer.

[EDIT: Clarifying exponential adjunction equation to follow usual notation]

Comment Source:> What are the exponential of two preorders? I'm guessing that \$$A^B\$$ is the set of order preserving maps from \$$B\$$ to \$$A\$$, where the maps are ordered by pointwise comparisons: \$$f \leq g\$$ means \$$f(x) \leq g(x)\$$ for all \$$x\$$. > Guessing again, is the coproduct formed by taking the disjoint union of the underlying sets, and the disjoint union of the ordering relations? From my understanding this is all correct. > I know it's just a homework exercise to draw the diagrams and check the claims. So... drawing and scanning diagrams by hand is a lot of work, or making them with TikZ and exporting them to png and so on (this forum doesn't support svgs sadly). I find the equational approach is a bit easier online, and it often corresponds super nicely with Haskell. ------ So let's start with coproducts. They are very similar to the products. They have morphisms \$$i_1 : A \to A + B\$$ and \$$i_2 : B \to A + B\$$ and morphism composition \$$(\nabla) : (A \to C) \Rightarrow (B \to C) \Rightarrow A + B \to C\$$. I'll come back later and write the equations out unless someone else wants to. The analogues in Haskell can all be found in the Prelude, unlike products where we need Control.Arrow.(&&&). ------ For exponentials, one way of defining them is via the adjunction \$$\bullet \times A \dashv \bullet^A\$$. In this case we would want to show, for all \$$B\$$: \$Hom(- \times A, B) \simeq Hom(-, B^A) \$ ------ Finally, it's possible to define coproducts via an adjunction and exponentials via equations. These aren't as natural in Haskell, however. I'll come back later and chip away at these proofs @DavidTanzer. [EDIT: Clarifying exponential adjunction equation to follow usual notation]
• Options
8.
edited February 2020

Great, thanks @MatthewDoty!

This is informative. All chippings away are appreciated. I can almost see the co-products. Equational presentation would be great to see. Maybe that would help me to better parse Haskell. I'm more comfortable with the straight mathematical language, and with "ordinary" languages like Python, but when I look at Haskell code it can look blurry.

Another option for these kinds of focussed explanations would be to create small discussions, in the category "Forum Mini-Talks". A wrote a few there. They're not meant to be some kind of earth shaking thing, just to have a useful point that is intended to be made, and to be explained in a way that tries to help the reader get from point A to point B.

Or these approaches could be combined. Answers made in the context of a discussion here could later be culled and organized into a mini-talk.

Comment Source:Great, thanks @MatthewDoty! This is informative. All chippings away are appreciated. I can almost see the co-products. Equational presentation would be great to see. Maybe that would help me to better parse Haskell. I'm more comfortable with the straight mathematical language, and with "ordinary" languages like Python, but when I look at Haskell code it can look blurry. Another option for these kinds of focussed explanations would be to create small discussions, in the category "Forum Mini-Talks". A wrote a few there. They're not meant to be some kind of earth shaking thing, just to have a useful point that is intended to be made, and to be explained in a way that tries to help the reader get from point A to point B. Or these approaches could be combined. Answers made in the context of a discussion here could later be culled and organized into a mini-talk. 
• Options
9.
edited February 2020

Equational presentation would be great to see. Maybe that would help me to better parse Haskell. I'm more comfortable with the straight mathematical language, and with "ordinary" languages like Python, but when I look at Haskell code it can look blurry.

I have to admit I really like Haskell and I think its great for studying category theory. Equational reasoning in Haskell is quite common in research papers.

That being said, I'll try to balance these discussions with more traditional mathematics.

Anyhow, here's the usual commutative diagram for the coproduct:

The diagram doesn't mention the morphism composition operation $$(\nabla) : (A \to C) \Rightarrow (B \to C) \Rightarrow A + B \to C$$, but it takes the place of $$f$$. Instead of $$f$$, we would write $$f_1 \nabla f_2$$.

The morphism composition operation $$(\nabla)$$ is unique in obeying the equations for the coproduct, are quite similar to the product equations:

$f \nabla g \cdot i_1 = f\\ f \nabla g \cdot i_2 = g\\ (f \cdot i_1) \nabla (f \cdot i_2) = f$

In Hask, $$i_1$$ is Left :: a -> Either a b, $$i_2$$ is Right :: b -> Either a b, and $$(\nabla)$$ is either :: (a -> c) -> (b -> c) -> Either a b -> c

Once again, I feel the only real challenge in the case of PreOrder is showing all of the morphisms involved are order preserving maps. I did something similar above so I'll just wave my hand at that.

The adjunction $$\bullet \times A \dashv \bullet^A$$ is realized by the functors (,a) and (->) a. That second functor is called the reader monad. It comes up pretty often when you have to read information from a config for a web app and you don't want to carry a parameter around.

The isomorphism Hom(- \times A, B) \simeq Hom(-, B^A) is realized by two functions:

  uncurry :: (c -> a -> b) -> (c,a) -> b
curry :: ((c,a) -> b) -> (c -> a -> b)


Okay, it's getting a bit late, more tomorrow...

[EDIT: Formatting, mentioning uniqueness]

Comment Source:> Equational presentation would be great to see. Maybe that would help me to better parse Haskell. I'm more comfortable with the straight mathematical language, and with "ordinary" languages like Python, but when I look at Haskell code it can look blurry. I have to admit I really like Haskell and I think its great for studying category theory. Equational reasoning in Haskell is quite common in research papers. That being said, I'll try to balance these discussions with more traditional mathematics. Anyhow, here's the usual commutative diagram for the coproduct: ![Coproduct](https://upload.wikimedia.org/wikipedia/commons/thumb/2/2b/Coproduct-03.svg/200px-Coproduct-03.svg.png) The diagram doesn't mention the morphism composition operation \$$(\nabla) : (A \to C) \Rightarrow (B \to C) \Rightarrow A + B \to C\$$, but it takes the place of \$$f\$$. Instead of \$$f\$$, we would write \$$f_1 \nabla f_2\$$. The morphism composition operation \$$(\nabla)\$$ is unique in obeying the equations for the coproduct, are quite similar to the product equations: \$f \nabla g \cdot i_1 = f\\\\ f \nabla g \cdot i_2 = g\\\\ (f \cdot i_1) \nabla (f \cdot i_2) = f \$ In *Hask*, \$$i_1\$$ is Left :: a -> Either a b, \$$i_2\$$ is Right :: b -> Either a b, and \$$(\nabla)\$$ is either :: (a -> c) -> (b -> c) -> Either a b -> c Once again, I feel the only real challenge in the case of *PreOrder* is showing all of the morphisms involved are order preserving maps. I did something similar above so I'll just wave my hand at that. ----------------------------------- The adjunction \$$\bullet \times A \dashv \bullet^A \$$ is realized by the functors (,a) and (->) a. That second functor is called the _reader monad_. It comes up pretty often when you have to read information from a config for a web app and you don't want to carry a parameter around. The isomorphism Hom(- \times A, B) \simeq Hom(-, B^A) is realized by two functions: uncurry :: (c -> a -> b) -> (c,a) -> b curry :: ((c,a) -> b) -> (c -> a -> b) Okay, it's getting a bit late, more tomorrow... [EDIT: Formatting, mentioning uniqueness]
• Options
10.

I have to admit I really like Haskell and I think its great for studying category theory. Equational reasoning in Haskell is quite common in research papers.

Sounds good! I'm glad to try on some new glasses.

Comment Source:> I have to admit I really like Haskell and I think its great for studying category theory. Equational reasoning in Haskell is quite common in research papers. Sounds good! I'm glad to try on some new glasses.