Lecture 31 - Chapter 2: Lawvere Metric Spaces

John Baez · May 2018

Last time I asked you to figure out what's a category enriched in the symmetric monoidal poset of "costs".

The set of costs consists of nonnegative numbers together with infinity:

$$ [0,\infty] . $$ There's an obvious way to define $\le$ for costs, where we decree that everything is less than or equal to $\infty$. There's an obvious way to add costs, where we decree that $\infty$ plus anything equals $\infty$. And there's an obvious unit for this addition operation, namely $0$.

Now comes the tricky part, which tripped me up at first. We've got our hands on a obvious way to create a symmetric monoidal poset, which we could call $ ( [0,\infty], \le, +, 0 )$. However, this is not the one we want! Instead, we will to play a fiendish trick! We'll use the "opposite" symmetric monoidal poset:

$$ \mathbf{Cost} = ( [0,\infty], \ge, + , 0) .$$ Note we've flipped around the direction of our partial order! You can always take any symmetric monoidal poset $\mathcal{V}$, reverse the direction of the partial order this way, and get a new one called the opposite $\mathcal{V}^{\text{op}} $. This can be confusing, and your brain may be screaming in pain, but it's a fundamental fact of life so you have to get used to it.

Let's see what a $\mathbf{Cost}$-category amounts to, and why this "opposite" trick was a good idea here. We'll just run through the definition of enriched category and see what it gives.

A $\mathbf{Cost}$-category, say $\mathcal{X}$, consists of:

a set of objects, $\mathrm{Ob}(\mathcal{X})$, and
an element $\mathcal{X}(x,y) \in \mathbf{Cost} $ for any two objects $x,y$.

So, a $\mathbf{Cost}$-category gives a number in $[0,\infty]$ for each pair of objects $x,y$.

$$ I\leq\mathcal{X}(x,x) \textrm{ for any object } x .$$ However, in $\mathbf{Cost}$ the unit $I$ is the number $0$, and we've fiendishly reversed the ordering. So, in a $\mathbf{Cost}$-category we have

$$ 0 \geq \mathcal{X}(x,x) \textrm{ for all objects } x .$$ But $ \mathcal{X}(x,x) $ is a cost, so we also know $ \mathcal{X}(x,x) \geq 0 $. So, we can just say

$$ \mathcal{X}(x,x) = 0 \textrm{ for all objects } x .$$ Finally:

b) In any enriched category we have

$$ \mathcal{X}(x,y)\otimes\mathcal{X}(y,z)\leq\mathcal{X}(x,z) \textrm{ for all objects } x,y,z. $$ However, in $\mathbf{Cost}$ the monoid operation $\otimes$ is addition, and we've fiendishly reversed the ordering. So, in a $\mathbf{Cost}$-category we have

$$ \mathcal{X}(x,y) + \mathcal{X}(y,z) \geq\mathcal{X}(x,z) \textrm{ for all objects } x,y,z. $$ Now we're done.

But hey: that last inequality is the triangle inequality! So maybe we should think of $\mathcal{X}(x,y)$ as a distance and write it as $d(x,y)$. That's what Bill Lawvere did in 1973... and he invented the concept that's now called a Lawvere metric space. In other words:

Definition. A Lawvere metric space is a $\mathbf{Cost}$-category.

Theorem. A Lawvere metric space consists of a set $X $ together with a function

$$ d : X \times X \to [0,\infty] $$ such that

a) $ d(x,x) = 0 $ for all $ x \in X $

and

b) $ d(x,y) + d(y,z) \geq d(x,y) $ for all $ x,y,z \in X$.

Proof. We've shown that any $\mathbf{Cost}$-category consists precisely of a set $X = \mathrm{Ob}(\mathcal{X})$ together with a cost $d(x,y) = \mathcal{X}(x,y) $ for each $x,y \in X$, obeying these two inequalities. $ \qquad \blacksquare $

Now, you may already have heard about metric spaces. A metric space is a very famous concept: it's a set with a way of measuring distances that obeys a few axioms. These include the two axioms of a Lawvere metric space, but also three more:

d) if $d(x,y) = 0 $ then $x = y $

e) $d(x,y) = d(y,x) $ for all $x,y \in X$, and

f) $d(x,y) < \infty $

for all $x,y \in X$.

These extra axioms hold in a lot of examples, but Lawvere noticed that they aren't really necessary for many of the main theorems involving metric spaces!

Dropping these extra axioms also allows for new applications. For example, we could let $d(x,y)$ be the cost of going from one place $x$ to another place $y$, using your favorite modes of transportation. There are places you can go for free, so axiom d) does not hold. Sometimes it costs a different price to go from $x$ to $y$ than to go back, so axiom e) does not hold. And there are places you cannot go for any prices, like the Andromeda Nebula, so axiom f) does not hold. (See how economic issues keep coming into the discussions in this chapter?)

In fact, axioms d)-f) are also bad in some purely mathematical ways: there are some nice ways to build new Lawvere metric spaces from old ones (called "coequalizers" and "coproducts") that don't work when you include these extra axioms.

You might think that extra axioms are always good, because they let you prove more theorems. But you have to remember they impose a price: it means the axioms apply to fewer things, so constructing structures that obey these axioms becomes harder.

So, Lawvere metric spaces are a great example of how category theory can lead us to refine and perfect existing ideas. And when you get good at enriched category theory, it means every general result you prove will apply to Lawvere metric spaces as well as preorders!

To see what Lawvere actually did, read this paper:

Bill Lawvere, Metric spaces, generalized logic and closed categories, Rendiconti del Seminario Matematico e Fisico di Milano XLIII (1973), 135-166. Reprinted in Reprints in Theory and Applications of Categories 1 (2002), 1-37.

It's good to look at papers by Lawvere now and then, to see how close you are to being a true category theorist. It's inevitably humbling, at least for me... but I've decided that's a good thing. It drives me to do better, while preventing me from getting a big head.

You may wonder what would happen if we hadn't flipped the order when defining $\mathbf{Cost}$.

Puzzle 90. What's a $\mathbf{Cost}^{\text{op}}$-category, and what if anything are they good for?

Some of you have already answered the first part. Section 2.3.4 of the book leads you through other examples of enriched categories. Here's another. Let

$$ D = \{ \textrm{Monday}, \textrm{Tuesday}, \textrm{Wednesday}, \textrm{Thursday}, \textrm{Friday}, \textrm{Saturday}, \textrm{Sunday} \} $$ and let

$$ \mathcal{V} = \prod_{d \in D} \mathbf{Cost} $$ that is, the product of 7 copies of $\mathbf{Cost}$, one for each day of the week.

Puzzle 91. Show how to make the product of symmetric monoidal posets into a symmetric monoidal poset. Thus, $\mathcal{V} $ becomes a symmetric monoidal poset. What is a $\mathcal{V} $-category like, and what are they good for in everyday life?

To read other lectures go here.

Keith E. Peterson · May 2018

Puzzle KEP: Give some examples of generalized metric spaces. Show that they satisfy the axioms of an enriched category.

John Baez · May 2018

By the way: Proposition 2.20 in the book says that any symmetric monoidal preorder $\mathcal{V}$ has an opposite $\mathcal{V}^{\text{op}}$; completing the proof of this result is Exercise 2.21, and then in Exercise 2.22 you're invited to study $\mathbf{Cost}^{\text{op}}$. Everyone should give them a try!

John Baez · May 2018

I've added some puzzles to the end of today's lecture:

Puzzle 90. What's a $\mathbf{Cost}^{\text{op}}$-category, and what if anything are they good for?

Some of you have already answered the first part. Section 2.3.4 of the book leads you through other examples of enriched categories. Here's another. Let

$$ D = \{ \textrm{Monday}, \textrm{Tuesday}, \textrm{Wednesday}, \textrm{Thursday}, \textrm{Friday}, \textrm{Saturday}, \textrm{Sunday} \} $$ and let

$$ \mathcal{V} = \prod_{d \in D} \mathbf{Cost} $$ that is, the product of 7 copies of $\mathbf{Cost}$, one for each day of the week.

Puzzle 91. Show how to make the product of symmetric monoidal posets into a symmetric monoidal poset. Thus, $\mathcal{V} $ becomes a symmetric monoidal poset. What is a $\mathcal{V} $-category like, and what are they good for in everyday life?

Fredrick Eisele · May 2018

The economic models are "fun". Consider the couch surfer, staying in one place too long will incur a cost but travelling is less costly. The costs increase the longer you stay. They expect you to pay for food and stuff. Not quite sure how to deal with the temporal issues.

I made a diagram for Cost that I think helps the discussion.

Diagram

Also, see Exercise 22 - Chapter 2

Where the $ X $ and $ X_{neg} $ have the conventional meaning for $ \le $ and $ \ge $ while the $ X^{op} , X_{neg}^{op} $ have the opposite meaning.

Christopher Upshaw · May 2018

That is a very helpful diagram.

Keith E. Peterson · May 2018

Should add $X^{neg^{op}} $ for completeness.

Christopher Upshaw · May 2018

I would probably call $\mathbf{Cost^{op}}$ $\mathbf{Gross}$, or $\mathbf{Reward}$. It's useful when you are interested in the maximum of alternate paths. What's the most you can get out of going from a to b.

Unfortunately, even though this feels like it should work to describe how much energy you can get by running a heat engine, or how much money you can make on a paper route, any non zero loops force the co distance to infinity.

MatthewDoty · May 2018

Puzzle 90. What's a $\mathbf{Cost}^{\text{op}}$-category, and what if anything are they good for?

The story doesn't look very good for them :(

Theorem. If $\mathcal{X}$ is a $\mathbf{Cost}^{\text{op}}$-enriched category, then:

$$\forall a,b. \mathcal{X}(a,b) = 0 \text{ or } \mathcal{X}(a,b) = \infty$$ Proof.

If every element $\mathcal{X}(a,b) = 0$, we are done.

Next assume to the contrary. We must show that for an arbitrary $a$ and $b$ that $\mathcal{X}(a,b) = \infty$.

So observe there must be some $\hat{a}$ and $\hat{b}$ such that $\mathcal{X}(\hat{a},\hat{b}) > 0$.

It must be $\mathcal{X}(\hat{a},\hat{b}) = \infty$. To see this, we know from the laws of enriched categories (part (b)) that:

$$ \begin{align} \mathcal{X}(\hat{a},\hat{b}) + \mathcal{X}(\hat{b},\hat{a}) & \leq \mathcal{X}(\hat{a},\hat{a}) \\ \implies \mathcal{X}(\hat{a},\hat{b}) & \leq \mathcal{X}(\hat{a},\hat{a}) \end{align} $$ However, then we have

$$ \begin{align} \mathcal{X}(\hat{a},\hat{b}) + \mathcal{X}(\hat{a},\hat{a}) & \leq \mathcal{X}(\hat{a},\hat{b}) \\ \implies 2 \mathcal{X}(\hat{a},\hat{b}) & \leq \mathcal{X}(\hat{a},\hat{b}) \end{align} $$ This can only happen if $\mathcal{X}(\hat{a},\hat{b}) = \infty$ or $\mathcal{X}(\hat{a},\hat{b}) = 0$. But we know $\mathcal{X}(\hat{a},\hat{b}) > 0$ so it must be $\mathcal{X}(\hat{a},\hat{b}) = \infty$ .

Next observe from the enriched category theory law (b) that:

$$ \mathcal{X}(a,\hat{a}) + \mathcal{X}(\hat{a},\hat{b}) \leq \mathcal{X}(a,\hat{b}) $$ So it must be that $\mathcal{X}(a,\hat{b}) = \infty$. But then

$$ \mathcal{X}(a,\hat{b}) + \mathcal{X}(\hat{b},b) \leq \mathcal{X}(a,b) $$ Hence $\mathcal{X}(a,b) = \infty$.$\ \ \ \ \ \ \ \ \Box$

[Edit: Updated following Christopher's suggestion. Thanks Chris!]

Christopher Upshaw · May 2018

Hmm. Your proof as written doesn't quite work because you have $\chi (a,b)$ where it should be $\chi(a,b)$, and there's only guaranteed to be a maximal hom object if $Obj \times Obj$ is finite.

But I think both issues can be repaired:

Let $a, b$ be objects of a $\mathbf {Cost^{op}}$-category. By the co-triangle inequality

\[\mathcal{X}(a,b)+\mathcal{X}(b,a)≤\mathcal{X}(a,a) \]

Adding a non-negative number can't decrease a real value, so

\[\mathcal{X}(a,b)≤\mathcal{X}(a,a) ,\]

however by the co- triangle inequality

\[ \mathcal{X}(a,b)+\mathcal{X}(a,a)≤\mathcal{X}(a,b) \]

by$\mathbf {Cost^{op}}$ being a monoidal preorder

\[ \mathcal{X}(a,b)+\mathcal{X}(a,b)≤\mathcal{X}(a,b) \]

\[ 2\mathcal{X}(a,b)≤\mathcal{X}(a,b) \]

So $\mathcal{X}(a,b)= 0 $ or $\infty $.

MatthewDoty · May 2018

there's only guaranteed to be a maximal hom object if Obj×Obj is finite.

Good point, I'll update the statement of the theorem.

Anindya Bhattacharyya · May 2018

Thinking out loud here, but metric spaces are examples of topological spaces... so is there an equivalent "generalised topological space" for Lawvere metric spaces?

I can see how dropping axiom (d) just means the space has indistinguishable points (ie it no longer has to be $T_0$), and dropping (f) just means it no longer has to be connected... but dropping axiom (e) seems to have stranger effects, ones that can't obviously be captured by our usual concept of topology.

MatthewDoty · May 2018

Anindya Bhattacharyya

I can see how dropping axiom (d) just means the space has indistinguishable points (ie it no longer has to be T0), and dropping (f) just means it no longer has to be connected... but dropping axiom (e) seems to have stranger effects, ones that can't obviously be captured by our usual concept of topology.

Well, in the very least we can think of Lawvere metric spaces as inducing Bitopological spaces.

Ordinarily, a metric space topology is defined using a metric $(X,d)$ by taking the set of open balls as a topological basis:

$$ B_r(p) = \{ x \in X \mid d(x,p) < r \} \text{ where } r \in \mathbb{R}^+ $$ This would be the end of it, except in a Lawvere space $d(x,p) \neq d(p,x)$

So we can construct another topology by flipping the usual definition:

$$ A_r(p) = \{ x \in X \mid d(p,x) < r \} \text{ where } r \in \mathbb{R}^+ $$ Puzzle MD1. Show these each form a topological basis. That is, show:

For each $x$ in $X$, there is at least one basis element $E$ containing $x$.
If $x$ belongs to the intersection of two basis elements $E_1$ and $E_2$, then there is a basis element $E_3$ containing $x$ such that $E_3$ subset $E_1$ intersection $E_2$.

Puzzle MD2. Morphisms over enriched categories are maps $\phi : \mathcal{X} \to \mathcal{Y} $ obeying:

$ \mathcal{X}(a,b) \leq_{\mathcal{X}} \mathcal{X}(c,d) \implies \mathcal{Y}(\phi(a),\phi(b)) \leq_{\mathcal{Y}} \mathcal{Y}(\phi(c),\phi(d)) $

$ \mathcal{X}(a,b) \otimes_{\mathcal{X}} \mathcal{X}(c,d) \leq_{\mathcal{X}} \mathcal{X}(e,f) \implies \mathcal{Y}(\phi(a),\phi(b)) \otimes_{\mathcal{Y}} \mathcal{Y}(\phi(c),\phi(d)) \leq_{\mathcal{Y}} \mathcal{Y}(\phi(e),\phi(f)) $

$ \mathcal{X}(a,b) = I \implies \mathcal{Y}(\phi(a),\phi(b)) = I $

Let $\mathcal{X}$ and $\mathcal{Y}$ be Cost-enriched categories, and let $\phi : \mathcal{X} \to \mathcal{Y}$ be a morphism between them. Does $\phi$ induce a pairwise continuous map over their bitopologies? Or the other way around - does a pairwise continuous map between the bitopologies of $\mathcal{X}$ and $\mathcal{Y}$ induce an enriched category morphism?

I don't know the answer to MD2...

Christopher Upshaw · May 2018

Oh, fancy.

Tobias Fritz · May 2018

@Matthew: that's an interesting take on the question! But did you check whether each one of your two systems of open balls actually is a basis?

Turning a Lawvere metric space into (something like) a topological space in a nice way is known to be quite tricky. I think that there are some well-known answers, but I don't understand the details. There's interesting material along these lines in the papers of Jean Goubault-Larrecq, as in this one. It's much easier to turn a Lawvere metric space into a quasiuniform space, for those who are into this sort of stuff.

Christopher Upshaw · May 2018

Hmm. Well it looks like every quasi uniform space is a topology, but it also looks like maybe it will be easier to make a directed* quasi uniform space then a directed topology.

"directed" meaning non symmetric, by analogy with graphs.

Oh, hmm. Hmm, maybe we want a topology on ordered pairs of points, with basis \[ B_r(p,q)= \{ (x,y) | d (p,x) + d(x,y) + d (y,q) < r + d (p,q)\}\]

I'm on my phone so I can't type out the equations to check if that works, and I'm not up to doing it in my head, but i will look at it later.

MatthewDoty · May 2018

@Tobias - I checked the proofs but I am always confused by the flipped order of Cost.

Am I missing something? I am struggling to think of a counter example to MD1...

John Baez · May 2018

Great solution to Puzzle 90, Matthew and Christopher! Good work! We now see how disastrous the 'co-triangle inequality' $d(a,b) + d(b,c) \le d(a,c)$ would be.

Christopher had written:

Okay, why the hell is \chi working, but \Chi isn't?

LaTeX doesn't have \Chi because they believe a capital Greek letter Chi looks just like an X. But you were trying to draw what Matthew was drawing, namely $\mathcal{X}$, and that's done using \mathcal{X}. Fong and Spivak use the \mathcal font for enriched categories.

You can always click the little gear at the upper right of someone's comment to see how they did what they did.

Tobias Fritz · May 2018

@Matthew: ah, good. I was a bit worried that you might have to use symmetry to do Puzzle MD1.2, but after some calculation I agree with you. Neat!

Christopher Upshaw · May 2018

Ah, for some reason on my phone the gear is only there on my own posts. Mobile browsing is always a little caveat emptor.

Also i think we can fix the problem by adding a $-\infty$ value, and setting ${-\infty} + {+\infty} = -\infty$

Simon Willerton · May 2018

Christopher, you should maybe follow your nose with the $-\infty$ idea...

Sophie Libkind · May 2018

After reading Matthew's proof in #8, I think that a $\mathbf{Cost}^{\text{op}}$-category is equivalent to a $ (\{ \tt{true}, \tt{false}\}, \implies, \tt{false}, \tt{or}) $-category, that Daniel described in #10 of Lecture 29.

Both Daniel and Matthew point out that either, $\mathcal X(x,y) = \tt{true}$ for all pairs $x,y)$ or $\mathcal X(x,y) = \tt{false}$ for all pairs $x,y)$. Thinking about the set of objects as a discrete points and drawing an arrow between objects where $\mathcal X(x,y) = \tt{true}$, we could visualize every $\mathbf{Cost}^{\text{op}}$-category as either a discrete set of points or as a fully connected graph.

Somehow this has the feeling of adjoints, since the discrete set of points under-estimates the connections between objects and the fully connected graph over-estimates the connections between objects.

Sophie Libkind · May 2018

Puzzle 91

Let's start with the first part

Show how to make the product of symmetric monoidal posets into a symmetric monoidal poset.

Let $(X, \leq_X, I_X, \otimes_X)$ and $(Y, \leq_Y, I_Y, \otimes_Y)$. We can define a new symmetric monoidal poset $ (X\times Y, \leq_{X \times Y}, I_{X \times Y}, \otimes_{X\times Y} ) $ where

$$(x, y) \leq_{X \times Y} (x', y') \textrm{ iff } x \leq_X x' \textrm{ and } y \leq_Y y' $$ $$I_{X \times Y} = (I_X, I_Y)$$ $$(x_1, y_1) \otimes_{X \times Y} (x_2, y_2) = (x_1 \otimes_X x_2, y_1 \otimes_Y y_2)$$ Proving that this is a symmetric monoidal poset follows pretty immediately from breaking down each property into a property about $(X, \leq_X, I_X, \otimes_X)$ and a property about $(Y, \leq_Y, I_Y, \otimes_Y)$ and then applying the fact that they are both symmetric monoidal posets.

Here is an example:

We want to show that if $ (x_1, y_1) \leq_{X \times Y} (x_1', y_1') $ and $ (x_2, y_2) \leq_{X \times Y} (x_2', y_2') $, then \[(x_1, y_1)\otimes_{X \times Y} (x_2, y_2) \leq_{X \times Y} (x_1', y_1')\otimes_{X \times Y} (x_2', y_2') . \]

By the definition of $\leq_{X \times Y}$, the hypotheses imply that

$$ x_1 \leq_X x_1' ,\quad x_2 \leq_X x_2' ,\quad y_1 \leq_Y y_1' , \quad \textrm{ and } y_2 \leq_Y y_2' .$$ Since $(X, \leq_X, I_X, \otimes_X)$ and $(Y, \leq_Y, I_Y, \otimes_Y)$ are monoidal posets we have that

$$x_1 \otimes_X x_2 \leq_X x_1' \otimes_X x_2' \textrm{ and } y_1 \otimes_Y y_2 \leq_Y y_1' \otimes_Y y_2' $$ And so by the definition of $ \leq_{X \times Y}$,

$$ ( x_1 \otimes_X x_2, y_1 \otimes_Y y_2 ) \leq_{X \times Y} (x_1' \otimes_X x_2', y_1' \otimes_Y y_2' ).$$ Of course applying the definition of $\otimes_{X \times Y}$ gives us our desired result:

$$(x_1, y_1)\otimes_{X \times Y} (x_2, y_2) \leq_{X \times Y} (x_1', y_1')\otimes_{X \times Y} (x_2', y_2') .$$ Now onto the next part

Thus, $\mathcal{V} $ becomes a symmetric monoidal poset. What is a $\mathcal{V} $-category like, and what are they good for in everyday life?

A $\mathcal{V} $-category assigns to every pair of objects a cost for each day of the week. Projecting to just the costs for one of the days of the week will give you a Lawvere metric space.

This might be useful when thinking about commutes. For example, my commute to and from work is very bad on Monday - Thursday, it's a little better on Friday because some people work from home, and on Saturday and Sunday it's very good. So as a objects of a $\mathcal{V} $-category, I might represent this as

$$ \mathcal{X}( \textrm{home}, \textrm{work}) = (30, 30, 30, 30, 25, 15, 15) $$

John Baez · May 2018

Sophie wrote:

Let $(X, \leq_X, I_X, \otimes_X)$ and $(Y, \leq_Y, I_Y, \otimes_Y)$. We can define a new symmetric monoidal poset $ (X\times Y, \leq_{X \times Y}, I_{X \times Y}, \otimes_{X\times Y} ) $ where
$$(x, y) \leq_{X \times Y} (x', y') \textrm{ iff } x \leq_X x' \textrm{ and } y \leq_Y y' $$ $$I_{X \times Y} = (I_X, I_Y)$$ $$(x_1, y_1) \otimes_{X \times Y} (x_2, y_2) = (x_1 \otimes_X x_2, y_1 \otimes_Y y_2)$$

Yes, that's the best way to make $X \times Y$ into a symmetric monoidal poset! If we ever get around to talking about the category of symmetric monoidal posets, this will be the product in that category!

(Actually it will be the product even if we don't get around to talking about it.)

A $\mathcal{V} $-category assigns to every pair of objects a cost for each day of the week. Projecting to just the costs for one of the days of the week will give you a Lawvere metric space.

This might be useful when thinking about commutes.

Yes, that's exactly the example I had in mind! Or museum prices: sometimes there's a discount for getting into the museum on certain days of the week.

Christopher Upshaw · May 2018

Christopher, you should maybe follow your nose with the $-\infty$ idea...`

Its interesting to note if we use the Haskell type former Maybe to add an extra value, every thing just works out of the box, the new value:Nothing is the bottom of the default order, and the default lifting works for what ever the monoid structure is.

That is let $M(S) = {\bot} \sqcup S$, and (eliding the inl/inr by abuse of notation) let the preorder $\le = {(\bot, x) | x \in S} \cup {(x,y) | x \le y}$ where the abuse of notation is 90% of whats going on. >_< and define $ lift2(F)(x,y) = \text{if}\, x = \bot \lor y = \bot\, \text{then}\, \bot \, \text{else}\, f(x,y)$

then $M([0,\infty])$ is a monoidal preorder with $\le$ as above, and lift2(+) the monoid.

And this fixes our problems: because if $\mathcal{X}(b,a)=-\infty$ then it can be the case that $\mathcal{X}(a,a) \le \mathcal{X}(a,b)$ so finite values are allowed, and can be distinct from one homobject to another.

Simon Willerton · May 2018

Christopher, I don't follow your Haskell reasoning, but I agree with your conclusion!

Christopher Upshaw · May 2018

Just saying we want the new value to be bottom in the order, and a absorbtive value for the monoidal operation.

And that is the default behavior on the order, and the default lifting of a function of two arguments produces the new monoid we want.

(It's unfortunately not the.default monoid on Maybe a. That uses Nothing as an identity. It's not a great default. About as good as having multiply as the default on the reals would be. It is sometimes what you want, but not often enough to be a good default. )

MatthewDoty · May 2018

Hey Chris,

After a quick glance at Simon's publications, I think maple might be a better lingua franca than Haskell if we are talking programming languages.

Haskell is pretty niche.

That being said, I think you are wrong here:

It's unfortunately not the.default monoid on Maybe a. That uses Nothing as an identity.

Maybe a does not have an instance for Monoid in the Prelude.

There is an instance Semigroup a => Monoid (Maybe a) in Data.Monoid.

You can define Monoid semantics like you want Maybe a, but you might need -fno-warn-orphan-instances to be turned on.

Simon Willerton · May 2018

After a quick glance at Simon's publications, I think maple might be a better lingua franca than Haskell if we are talking programming languages.

That did actually make me laugh. I used a lot of maple because that was what I used in my thesis a long time ago and just got into the habit of using it. I would not recommend it as a lingua franca! I've more or less kicked the habit now. I teach a course on Python and use Sage if I need more algebraic structure. For more mundane things like websites I use php and MySQL. Haskell is the language I'd like to know.

Haskell seems to be very relevant to this course as there seems to be a connection to FQL which we might find out about as things progress, I don't know. FQL appears to be a database language but with similarities to Haskell, here F stands for Functorial, and QL for Query Language like in MySQL.

So, do continue to write in Haskell to each other, just don't assume that all of us will understand it! I guess that Python ('excecutable pseudo-code') is considered a bit of a lingua franca on the web these days.

MatthewDoty · May 2018

For more mundane things like websites I use php and MySQL. Haskell is the language I'd like to know.

You can use Haskell and MySQL for CRUD web apps. I like Servant for routing. There's also scotty for routing which is inspired by Ruby's Sinatra. For MySQL I would use MySQL-simple.

If you want to learn Haskell, you might try what Prof. Robby Findler at Northwestern University does. He organizes mostly student-run seminars every other semester. He explores stuff like the K Framework, Coq and other cutting edge topics.

I guess that Python ('executable pseudo-code') is considered a bit of a lingua franca on the web these days.

Python is great for algorithms, and I agree along with JavaScript it is the lingua franca of the web.

I will try my hardest to use Python to communicate ideas.

Christopher Upshaw · May 2018

It's a little strange to think of Haskell as obscure for me because it's how i got into category theory.

But objectively it is obscure.

Keith E. Peterson · May 2018

I like the language Racket, because you can do magic like this,

INPUT:

#lang sweet-exp racket require(rename-in(racket/base (define ≝) (<= ≤))) {min(x y) ≝ (if {x ≤ y} x y) } min(0 5) min(6 3) min(9 9)

OUTPUT:

0 3 9 >

Yes, that is the unicode characters ≝ and ≤.

MatthewDoty · May 2018

Hey Keith,

You might consider formatting your coding blocks with <pre>...</pre> rather than backticks.

Moreover, should you ever become a professional software engineer, you should know using unicode a lot can be hard on coworkers who aren't into that sort of thing.

Keith E. Peterson · May 2018

Luckily I'm only interested in doing so as a means to make programming easier to teach to mathematicians, more specifically, myself.

Keith E. Peterson · May 2018

It's nice because,

{min(x y)
    ≝ (if {x ≤ y}
         x
        y)
 }

is basically how a mathematician defines a function,

\[ \begin{align} \min(x,y) \overset{\mathrm{def}}{=} \texttt{if } [x \leq y] \\ \texttt{then } x ; \\ \texttt{else } y. \\ \end{align} \]

Christopher Upshaw · May 2018

I must admit that I prefer Haskell written without Unicode, to Haskell with it.

Keith E. Peterson · May 2018

That isn't Haskell. It's a Scheme variant, Racket.

Christopher Upshaw · May 2018

Yes Haskell would use a lot fewer parentheses. :)

But Haskell also allows Unicode operators, and i mostly prefer just using 8 bit characters for source code. Though the space of 1 or 2 character operators is a bit overfull.

The use of operators instead of words is one of the things that confuses and scares people off from both Haskell in General and off of a number of libraries. Like lenses, which has a well organized but very large collection of them.

Christopher Upshaw · June 2018

@SimonWillerton Nothing other then the names "Maybe" and "Nothing" is actually Haskell in post #24.

JimStuttard · June 2018

Unicode is anathema if you're a working touch typist. It's a pity Agda developers obviously aren't.

Azimuth Forum

Howdy, Stranger!

Categories

Lecture 31 - Chapter 2: Lawvere Metric Spaces

Comments