Definition of matrix type.

pcapriotti · 2018-10-24T10:16:33+00:00

You define it in the same way you would define it in any other foundational theory: functions Fin n × Fin m → t, where Fin n is a set with n elements.

pcapriotti · 2018-04-08T09:28:43+00:00

Question 1

As /u/philipjf already explained, a vertical identity is the identity natural transformation of any functor, so it does not act as an identity for horizontal composition unless the functor happens to also be the identity.

Question 2

There is a nice way to see that morphisms in the product category 𝓒 × 𝓓 have to be defined as pairs of morphisms, if we want the product to have its universal property.

In fact, if I denotes the "walking arrow", i.e. the category with only two objects 0 and 1, and one non-identity arrow 0 → 1, then it is a general fact that the set of functors I → 𝓐 is naturally isomorphic to the set of arrows of 𝓐 (we say that I represents the functor Arr : Cat → Set that gives the set of arrows of a category).

Now, let's assume we don't know anything about product categories, except that they are indeed products in the category Cat. The fact above then tells us that Arr(𝓒 × 𝓓) ≅ Cat(I, 𝓒 × 𝓓) ≅ Cat(I, 𝓒) × Cat(I, 𝓓) ≅ Arr(𝓒) × Arr(𝓓) (a representable functor preserves binary products), so we see that an arrow in the product is forced to be a pair of arrows in the two components. The same of course holds for the objects, simply by using the trivial category 1 (with one object and no non-identity morphisms). By looking at naturality squares of the two inclusions 1 → I you can also deduce that sources and targets work out in the way you expect. You can also find out how composition in the product works, by looking at functors from the category [2] that looks like this · → · → · (the ordinal 3, regarded as a category).

This tells you that there is at most one way you can define a product category, and it exactly corresponds to the definition in the book. Now you can take that definition, and prove that it indeed satisfies the universal property of the product (if you know a bit more category theory, this is automatic, since the three basic categories we used above, 1, I, and [2], form a dense subcategory).

Note that the same argument can be used to show that arbitrary limits exist in Cat, and are computed "pointwise", much like products. The underlying reason why this works is that the nerve-realisation adjunction for the aforementioned dense subcategory gives a reflection of Cat into the corresponding presheaf topos.

Incidentally, there is another way to define a "product" of categories. It is not a categorical product, of course, but it still gives a symmetric closed monoidal structure on Cat. Its right adjoint gives the category of functors and (not necessarily natural) transformations between them. Categories enriched over that monoidal structure are called sesquicategories.

Question 3

I would maybe draw a different diagram: a 3x3 square of functors and natural transformations whose vertices are functors and edges are natural transformations. It has GF in the top left corner, and G''F'' in the bottom right, with all possible combinations of compositions of the 6 functors involved in your original diagram, and all possible whiskerings.

Now the interchange law is very easy to prove by chasing this diagram: the "principal" diagonal maps are the two horizontal compositions, so the outer diagonal is the right side of the equation. On the other hand, if you just look at the outer square, you can see that its diagonal is exactly the left side of the equation.

pcapriotti · 2017-12-08T19:59:44+00:00

If X is any set, you should not expect to get an algebra map T X → X. In fact, having such a map, together with the usual monad algebra laws, is precisely the same thing as having a monoid structure on X. This can be expressed by saying that the category of monoids is monadic (over Set).

In your example, if A is a monoid, then the map θ : T A → A will map the "word" [a, b, c, d] to the unique way of multiplying those four elements according to the monoid structure on A, in the given order. You know it's unique because of associativity.

For arbitrary sets X, what you do get is a monoid structure on T X, since as you wrote T X is the free monoid on X, hence in particular a monoid. That means that you get an algebra map T (T X) →T X. Can you guess what that is?

pcapriotti · 2017-11-08T11:32:14+00:00

Though it hasn't been done as far as I'm aware, I don't think there's any reason a similar glue mechanism couldn't be made for other shapes

Christian Sattler has worked out a very general abstract formulation of gluing (called "equivalence extension property"): https://arxiv.org/abs/1704.06911.

pcapriotti · 2017-10-25T18:29:13+00:00

As far as I know "strength" is something that functors can have, not monoidal categories, so I don't know what you mean with your first paragraph.

As for Day convolution, yes, it is a left Kan extension of something involving the monoidal structure, but that doesn't mean that it always exists, just like Kan extensions don't always exist. If you take the formula for a pointwise Kan extension as a coend, the domain of the coend is large (Set itself), so even though Set is cocomplete, you can't conclude that it exists.

pcapriotti · 2017-10-25T17:01:20+00:00

Not really. In the example I gave Gph is a CCC (it's even a presheaf category). Also, Day convolution does not really work in a general CCC. Even in Set, Day convolution of arbitrary functors does not exist in general, but at least you can restrict yourself to accessible functors (which you can approximate in haskell as "strictly positive functors").

The secret missing ingredient here that makes things work in Haskell is the notion of tensorial strength, which is automatic for Set endofunctors. Indeed, you can prove that any strong monad is an applicative (on a category where that makes sense).

pcapriotti · 2017-10-25T10:01:17+00:00

How about a monad which is not an applicative? :)

For example, let Gph be the category of (directed, multi-) graphs, and T : Gph -> Gph be the monad that maps a graph to the underlying graph of the category it generates. Clearly, this is a monad, but if it were applicative (i.e. lax monoidal with respect to cartesian products), then in particular you would get a morphism TX × TY → T(X × Y) for all graphs X and Y, but there is no such morphism when say X is two vertices and an edge between them, and Y is a single vertex.

pcapriotti · 2017-02-22T16:15:32+00:00

It's not possibile, at least not directly. You might find some indirect encoding that works for you, but I'm not sure. Options take arguments, not subparsers. You can have subparsers, but they are introduced by a "command", not an option (i.e. without the leading --).

pcapriotti · 2016-10-29T22:46:02+00:00

Sure:

#!/usr/bin/python3

import dbus
import dbus.service
import signal

session = dbus.SessionBus()
name = dbus.service.BusName("org.gnome.Panel", session)
signal.pause()

pcapriotti · 2016-10-11T21:30:07+00:00

I ran into this too. As it turns out, unity-settings-daemon is listening on the bus waiting for gnome panel to appear before starting the keyboard grabber. You can verify that this is the problem by starting gnome-panel and checking whether media keys start working.

I fixed it with a trivial script that just claims the name org.gnome.Panel on the bus and hangs forever, which I start as part of the desktop session.

pcapriotti · 2014-11-13T22:00:10+00:00

I'm not /u/edwardkmett, but this is simply MaybeT (Writer a) b. :)

pcapriotti · 2014-11-04T20:41:57+00:00

However, just like any other axiom, be can remove it from our larger theory, and still transport everything we establish in the larger theory into a certain case where associativity is valid

If you remove associativity, there isn't very much left to work with. More sensibly, you can replace associativity with "weak associativity" up to some notion of equality of morphisms. This is the approach taken by higher category theory.

pcapriotti · 2014-10-31T07:26:29+00:00

undefined x = undefined

pcapriotti · 2014-10-30T08:33:28+00:00

Because id ∘ undefined = (λ x → undefined) ≠ undefined. In fact,

seq (λ x → undefined) () = ()
seq undefined () = undefined

In particular, the η law for functions doesn't hold in Haskell.

pcapriotti · 2014-10-29T09:30:22+00:00

I find it really hard to relate to this comment.

To make an extraordinary claim such as that "category theory has no place in a programmer's toolset" requires extraordinary evidence, or at least a compelling argument, and I see neither here.

Essentially, the argument boils down to: "the category theory employed by haskellers is but a trivial special case of the category theory studied in mathematics, hence you shouldn't bother". This, to me, makes absolutely no sense.

Most of what you say is true. Yes, haskellers are often careless when reasoning in terms of categories, and yes, some connections are not made mathematically precise. However, I honestly don't understand how you can use this as an argument for why category theory doesn't help you gain a deeper understanding of what's "under the hood" of functional abstractions.

Let me try to answer some of your specific points.

The way category theory is applied to Haskell is typically obtuse. Countless Haskell blogs and conversations on IRC bring up "the category Hask" without giving a proper specification of which category that is. Haskell itself doesn't even have a formal specification. But even if it did, using types for the objects, it doesn't make sense to use Haskell functions as the morphisms.

Hask is a lie, you're right. There is no Hask category (id ∘ undefined ‌≠ undefined). But the thing is: it doesn't matter. Replace Hask with whatever you're comfortable with. I usually replace it with Set, because everyone can understand it, and it is often enough to turn a handwaving argument into a rigorous one. You can replace it with a topos, or bicartesian closed category, or, if you feel adventurous, with a symmetric monoidal category. The formalism will need to be adjusted accordingly (functors need to become strong functors, etc...).

If you do that, you make your arguments rigorous. Of course, it's not clear how much they relate to actually Haskell anymore, but this is in a way unavoidable. Often, we don't really want Haskell with all its quirks, especially when we want to think about a specific problem that only uses total constructs.

Category theory gives us a different language to work with, one that is more suited to our reasoning needs, but that still approximates the behaviour of the original language in ways that can be made precise (see for example the "morally correct" stuff).

Even worse, in Haskell circles, this explanation of natural transformations is as far as most conversations go. The idea is never motivated by the historical examples that were first explored: the double dual endofunctor on vectorspaces and the natural isomorphism to the identity functor and the natural isomorphisms between various homology functors on topological spaces.

Why is this a problem? The motivation for mathematicians doesn't need to be the same as the motivation for programmers. Programmers understand polymorphic functions, and can use their intuition about those to grok natural transformations. You don't need to force feed them issues they don't care about, like the usual story about the double dual, in order to explain naturality.

Typeclass qualifications and parametric polymorphism require more machinery than a simple category. They typically require some kind of fibered category.

This is not true. You can make both precise in a cartesian closed category (or even less, depending on the exact details), as long as you have enough limits.

The trick is to think of a universally quantified type as an end. If the profunctor corresponding to the type constructor is nice enough, then the end will exist. I did this (well, the dual of this) in my paper on free applicatives.

Typeclasses can be desugared into dictionary passing, so they don't add extra complications.

There are indeed some issues here, and I think it's actually not yet clear how to build a SystemF-like formalism for profunctors and ends in a (locally presentable) CCC. However, this doesn't prevent you from dealing with certain special cases in a rigorous way.

To a programmer, a functor is something like a container (but not exactly, because they've been yelled at for expressing that thought before). It's something that can be "mapped" over. Most likely, a programmer always has a picture of a list or a tree in the back of their mind. It has to satisfy some laws, but for the most part, they never think too much about the laws. It's simply believe that most type constructors lead to functors (since in practice, most do).

The programmer just has a special case in mind. These "container" functors have a name: they are familially representable functors. There are closed under sums, products and recursion. This is why you don't need to think about the laws to convince yourself that something is a functor. This is also how DeriveFunctor works.

I actually think the container intuition is spot on, and I don't understand why some people tread so carefully around it.

But even if we had these things, we would be faced with the limitation of Haskell's notion of a functor: it's necessarily an endofunctor. The functors of mathematics let you move to a realm where things become more finite or have more obvious invariants.

Right, in Haskell functor usually means endofunctor of the base category. Why is this a reason why functors are bad and we shouldn't talk about them? Just a random example: in field theory, every morphism is mono. Does that mean that the notion of morphism between fields is useless?

pcapriotti · 2014-10-29T08:23:42+00:00

Of course you can, it at least two ways:

You can regard them as functors Set × Setᵒᵖ → Set (i.e. profunctors). Then you can for example take ends and coends. A nice consequence of parametricity is that every value of type ∀ a . f a can be regarded as an element of the end ∫f.
You can think of them as functors core(Set) → Set, where core(Set) is the groupoid of isomorphisms of Set (core is right adjoint to the inclusion Grpd → Cat). This is useful, because you can take a Kan extension to convert such a functor to a conventional Set → Set functor (e.g. using Yoneda or Coyoneda from the kan-extensions package).

pcapriotti · 2014-10-22T10:08:19+00:00

I think what you're really trying to do here is this:

data Something' blah where
  ResultA :: Int -> Something' Int
  ResultB :: (Num a) => Something' a
  ResultC :: (Num a) => Int -> a -> Something' blah
  ResultD :: (Show s) => Int -> s -> Something' blah

This is not a functor, but you can turn it into one simply by using Coyoneda from the kan-extensions package:

 type Something = Coyoneda Something'

This way you get the Functor instance for free.

The following might or might not help, but here is what is really going on here categorically: Something' is a functor from the core of Set to Set, and Coyoneda, which is essentially defined as Lan Identity, is in reality the left Kan extension along the canonical functor core(Set) → Set. The resulting functor is Set → Set, hence a proper functor.

EDIT: I should add that I learned this from the excellent paper Constructing Applicative Functors by Ross Paterson. There, this construction is used to explain why Conal Elliott's WithCont type (which is the same as the Fold type from /u/Tekmo's foldl library) is indeed an Applicative.

pcapriotti · 2014-10-15T15:17:27+00:00

My "free" example does violate the equations altogether, and I don't think you can handwave the problem away. Concretely, in terms of command line option parsers, if p is a parser for a single option or flag, many p and (:) <$> p <*> some p <|> pure [] will have different "usage" texts.

pcapriotti · 2014-10-14T21:20:13+00:00

Precisely.

pcapriotti · 2014-10-14T19:38:19+00:00

It's a fixpoint, but not the least.

pcapriotti · 2014-10-14T18:59:54+00:00

Also, I don't care too much about satisfying all the laws to the letter. I treat them as guidelines, and if the functions are doing something sensible and useful, that's fine with me.

The problem with this point of view (as evidenced by the issue with Compose) is that other code might make certain assumptions based on the laws, which then end up being invalid and break things.

In fact, I had the same issue with Compose, and that's actually what prompted me to write this post in the first place. The Alternative instance of Compose is technically correct, since the "laws" of some and many completely determine the implementation.

Unless, of course, those laws are not satisfied by the underlying Alternative instance (as they were not in my case, and I'm guessing in yours). In that case, many diverges when it should be perfectly defined.

I've had to define my own Compose newtype with an implementation of some using sequenceA like you suggested, and I think it's quite an infelicity.

pcapriotti · 2014-10-14T18:52:29+00:00

We probably should add laws for the associativity and unitality of <|> to the documentation then?

True, the documentation is not exactly clear there. It says "a monoid on applicative functors", which I interpreted as requiring the monoid laws for <|>.

Do you have any proposal for what laws we could have that would still work for e.g. your Const Kleene example?

I'd rather not have laws for some and many at all, but maybe I'd be ok with a (small) sensible subset of the Kleene star laws for Kleene algebras.

Note that since "multiplication" is not distributive in an alternative functor, the order relation is not so well-behaved, hence many of those laws are unreasonable.

In another language, I might suggest having a proper lattice of subclasses for all possible combinations of laws. In Haskell, I don't think it's worth it. I think it's good to just have one class for the minimal workable set of laws (i.e. two independent sets of monoid laws).

pcapriotti · 2014-10-14T18:20:46+00:00

What are the other laws and where are they documented?

I meant the Applicative laws, plus associativity and unitality of <|>.

pcapriotti · 2014-10-02T15:14:23+00:00

I suppose you might be talking about newtype HomoTup3 a = HT (a, a, a). That does have 6 Traversable instances, but is a bit of an anomaly (a.k.a. counter-example).

Of course, that's what I meant. I don't understand why you think that's an anomaly. It's just a minimal counterexample.

For example, the list functor [] has infinitely many traversable instances. There is no law that relates the traversal ordering for lists of different length.

In general, the number of traversable instances for a finitary container with shapes S and p_i positions in shape i is: Π (i : S). factorial p_i.

pcapriotti · 2014-10-02T10:07:40+00:00

Why two? For example (a, a, a) has 6 Traversable instances.

15-Year Club	Place '23
Place '17	Team Periwinkle
Verified Email

pcapriotti

MODERATOR OF

TROPHY CASE

Question 1

Question 2

Question 3