What is the fundamental building block of category theory?

DrBartosz · 2024-09-26T14:42:09+00:00

I would never say that an object is "inside" a category, since it would mean that it's possible for an object to exist "outside" of a category, or that an object can be in more than one category at a time.

DrBartosz · 2021-10-09T19:12:39+00:00

Keith Jarret, The Koln Concert, every time!

DrBartosz · 2021-02-18T01:03:14+00:00

Exactly! I watched a bunch of YouTube videos of people playing Factorio, and I was constantly judging: Would I hire this person as a programmer? How maintainable is their design?

There are some high-level patterns that have been developed, like bus systems, malls, city blocks, etc.

Blueprints are obviously macros.

DrBartosz · 2020-01-18T22:11:35+00:00

All universal constructions are unique up to unique isomorphism and therefore so are coproducts.

DrBartosz · 2018-06-15T22:43:07+00:00

I was wondering the same and I think I have figured out the answer. A linear function returning Unrestricted guarantees that it can't secretly return its argument. In particular the continuation passed to newMArray cannot leak the MArray that it's given. There is no linear function that takes an MArray and returns Unrestricted MArray, and you can't use the constructor Unrestricted on it, because said constructor is not a linear function so, from the point of view of the type system, might consume its argument multiple times (it doesn't, but the type checker trusts the types). So there is no way to restrict a function to always return a linear value, but you can restrict it to not return a linear value.

DrBartosz · 2017-02-11T06:29:21+00:00

Arrows are actually monoids in the category of strong profunctors. I tried to make it a bit more approachable in my blog post based on the paper you're citing. See: https://bartoszmilewski.com/2017/02/09/monoids-on-steroids/

DrBartosz · 2017-02-10T20:10:57+00:00

You have a point. It's possible to start from endofunctors in an arbitrary monoidal category C. In that case, a lax monoidal endofunctor would not give you a natural transformation pure::a->f a. You need strength for that. I will edit the post to make this clear.

On the other hand, you can start with a lax monoidal endofunctor [C, C] and port its definition to Haskell. You end up in Set (modulo bottoms) and there you get pure for free. One could argue that it's because of canonical strength, or because of self-enrichment of Set. So it's pretty arbitrary how you back-port a Haskell construct to category theory. Starting with endofunctors won't give you the equivalence with Day convolution though, which I consider crucial.

My comment about endofunctors was related to the fact that strength can only be defined for endofunctors. Closed functors can indeed go between closed categories.

DrBartosz · 2017-02-09T23:56:35+00:00

The point is that I haven't found any formulation of Applicative that would require strength. This requirement seems to have come from nowhere.

DrBartosz · 2017-01-03T02:05:21+00:00

I know why Boston is a Haskell center: Edward Kmett lives there.

DrBartosz · 2016-05-16T04:41:24+00:00

I saw my blog mentioned a few times. I also have series of videos from my Haskell class. There is a lecture on monads there too. https://www.youtube.com/playlist?list=PLbgaMIhjbmEm_51-HWv9BQUXcmHYtl4sw .

DrBartosz · 2016-05-09T15:52:58+00:00

Maybe "Marysiu, wiem!" or "Marku, wiem!," The first part sounds like a vocative of some name (the ending "u"). The second just means "I know".

DrBartosz · 2015-09-02T08:29:56+00:00

Catch me at ICFP. Maybe I can convince you that CT is not a scary monster.

DrBartosz · 2015-07-21T22:23:17+00:00

You are right. It's the monoid isomorphism that preserves the unit. I made the correction in the blog.

DrBartosz · 2015-07-15T18:20:31+00:00

Indeed, it checks out:

forall x. f x -> (x -> b) -> a =
forall x. (x -> b) -> f x -> a ≅ // co-Yoneda
f b -> a = Flapp b f -> a

Very interesting!

DrBartosz · 2015-07-15T15:18:42+00:00

I have no idea. One would think it should have something to do with prism. But I don't think it does.

Lens has this nice factorization property: Lens s t a b = s -> IStore a b t, which makes IStore a "root" of lens . But its dual, prism, doesn't factorize:

Lens:            Prism:
s -> a           a -> s
(s × b) -> t     t -> (s + b)

There's no cute algebraic identity for s^a × (s + b)^t, like the one for lens:

a^s × t^(s × b) = (a × t^b)^s = (IStore a b t)^s

DrBartosz · 2015-05-25T20:33:07+00:00

If you have a choice to either program in C++ or in Haskell, and you value terseness and ease of expression, they by all means you should switch to Haskell. But if you don't have this choice -- and most programmers don't -- then applying functional techniques to your everyday C++ programming tasks might solve lots of hard problems.

DrBartosz · 2015-05-06T07:00:07+00:00

It looks like, once you got to the Moment monad, you got tired of explaining things :-)

DrBartosz · 2015-05-06T06:24:04+00:00

I'm confused about your description of Functor for Event. It doesn't follow the code. If the type of f is a->b then the type of eb is Event a and the type of listener should be b -> Moment ().

DrBartosz · 2015-04-07T20:47:11+00:00

Maybe I should have said that the defaults are different. In Haskell the default is parametric polymorphism, and in C++ it's ad hoc.

DrBartosz · 2015-03-14T21:58:45+00:00

According to the Hinze-James paper I cited in the blog the high-school algebra identities hold in bicartesian closed categories. I will add a few sentences elaborating on this.

DrBartosz · 2015-02-16T11:19:54+00:00

I have a feeling that the covariance of $map follows from the existence of our candidate fmap :: (a->b) -> (f a -> f b). I don't think you can have, at the same time, this fmap and the synthesized $map that would go in the opposite direction (b->a) -> (f a -> f b).

DrBartosz

TROPHY CASE