The conclusion that I am drawing is that set theory and category theory are different ways of thinking. In set theory, we can appeal to the axiom of extensionality, which says that singletons {a} and {b} are the same iff a=b. But in the category …
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 …
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 ag…
Bartosz Milewski's Blog
Categories For Programmers, which is selection of Bartosz's blog posts
The Comonad Reader Blog
Philip Freeman's Blog
Papers
Wadler, Theorems For Free! (1989)
Meijer et al, Functional Programming with Bananas, Lenses, En…
As far as I know the puzzle doesn't have anything to do with initial F-algebras. I think the type for a list algebra should just be [a] -> a.
@MatthewDoty This contradicts the definition given in the course notes. That's what I'm …
@EricRogstad - As far as I know the puzzle doesn't have anything to do with initial F-algebras. I think the type for a list algebra should just be [a] -> a. There's no need to take any fixedpoints.
Let me keep going with (c). In order to show…
@DavidTanzer: If people are interested I have some independent research I would like to polish up, ultimately for publication. I wouldn't mind making slide decks and presenting. Most of it is pure math I've formalized in a computer proof system, b…
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…
@AlexandreBMass
(1) If you permitted f n = [n...], then you couldn't permit sum xs = foldr (+) (0 :: Integer) xs. This is because there's no inhabitant of Integer that sum . f maps to for any input. In the setting of programming, category theory o…
I don't really care about the name. ProgrammingWithCategories2020 might be good.
I will probably make my own subdirectory for my stuff (this is what we do for our math talks at work).
@EricRogstad - I want to follow up and ellaborate on your question (and clear things up, mostly for my own edification).
How do we know that Fix is an initial algebra?
Bartosz just pointed out that we don't always know if Fix :: f (Fix f) ->…
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 equation…
@EricRogstad Recall that a morphism in the category of F-algebras is a function m :: a -> b mapping f :: f a -> a to g :: f b -> b by obeying the law:
m . f = g . fmap m
In order to show that Fix :: f (Fix f) -> Fix f is initial, we…
Note: I am introducing a nonstandard notion here \(x \triangleright y\) to mean \(x;y\) = x-then-y = \(y \circ x\) = y-after-x. The triangle reads nicely to show that the output of morphism x gets fed into the input of morphism y. It's a left-to-…
Apparently a List-algebra is a kind of monad algebra. According to nlab, we have the following axioms for a monad algebra \(a : T A \to A\):
\[
a \circ \eta = id \\
a \circ T a = a \circ \mu
\]
In Haskell, these laws would be:
a . return = id …
Here you're making the argument that things are not so simple with Haskell.
Well, just different I guess. I'll go into this below.
I still wonder though to what extent it is true within pure category theory. At least for the basic stuff I'…
The hardest part about getting a good system working is identifying the appropriate abstractions and interfaces -- the definitions. Once that's worked out, the actual coding of implementations can be a rather straightforward matter, which follows…
John -
I seem to recall Matthew had trouble proving the composite of conjoints is the conjoint of the composite:
[ \check{FG} \stackrel{?}{=} \check{F} \check{G} .]
I don't even know if this is true! It would seem strangely asymmetrica…
Puzzle 224. Suppose \(\mathcal{X}, \mathcal{Y}\) and \(\mathcal{Z}\) are \(\mathcal{V}\)-enriched categories. Show there is a \(\mathcal{V}\)-enriched profunctor
[ \alpha_{\mathcal{X}, \mathcal{Y},\mathcal{Z}} \colon (\mathcal{X} \otimes \ma…
@John - I was looking at your old Network Theory III notes and I saw a familiar pattern:
Given finite sets \(X\) and \(Y\) , a stochastic map \(f : X \rightsquigarrow Y\) assigns a
real number \(f_{yx}\) to each pair \(x \in X\), \(y \in Y\) i…
Michael Hong wrote:
So for this cap, we have \( \cap_X (x,x') = \hom(x',x) = \cup_X (x,x')\) ?
I think you have \(\cup\) flipped. I think this should be:
[
\cap_X(x,x') \cong \hom(x',x) \cong \cup_X(x',x)
]
They aren't equal, but they are co…
Michael wrote:
I can see how the repaired \(F(x)\) doesn't preserve arbitrary joins since \(4 \leq x \leq 6\) and \(6 \leq x\) both map to 2.
Right. We can use the adjoint functor theorem to check an a candidate to see if it is really an adjoi…
So maybe for cost it would be sum or maximum of the distance from F(x) to G(x) is the cost from F to G?
I think you right! In the case I gave, we have:
[
\begin{align}
\forall x. f(x) \leq_{\mathcal{X}} g(x) & \iff \forall x\in \mathrm{Ob…
Hey Chris,
They are weird, very useful though. It's part of a general maxim in CS that you start counting at 0. I.e. that you want to include the trivial or even pathological cases.
A empty space with no sand is still a heap of sand, at lea…
Hey Chris,
I think you are right!
In a former life I had to do a lot of lattice theory and FOL model theory, and I don't always feel comfortable with these empty objects...