Murat Kasimov

More about me

Я language (β)

/Я language (β)/Articles/Factoring through objects/

In general, when it's said "factoring through" it means that some morphish took an implicit roundabout which depends on exact object and unique morphism from/into it.

As an example, let's take a look at ho operator where both categories and functor are Arrows:

> `ho` : i `AR` a `AR_____` a `AR` o `AR____` i `AR` o

We can use these morphisms from ASCII package for an improvised example:

> x : Latin `AR__` Letter > xx : Letter `AR_` Glyph > xxx : Glyph `AR_` ASCII

Challenge: what constructors in ASCII package do x/xx/xxx morphisms correspond to?

In this case you can use this ho operator as left-to-right Arrow composition:

> x `ho` xx : Latin `AR_` Glyph > xx `ho` xxx : Letter `AR_` ASCII > x `ho` xx `ho` xxx : Latin `AR_` ASCII

If you want to use right-to-left composition with same morphisms you can use ha operator:

> xx `ha` x : Latin `AR_` Glyph > xxx `ha` xx : Letter `AR_` ASCII > xxx `ha` xx `ha` x : Latin `AR_` ASCII

So far so good. Now let's slightly change xx morphism so that it returns Alone Glyph:

> xx : Letter `AR_` Glyph > xx' : Letter `AR_` Alone Glyph

There is still a way to compose morphisms - we can use the fact that Alone is a covariant functor:

> `yo` : Alone Glyph `AR_____` Glyph `AR_` ASCII `AR____` Alone ASCII

However it comes at cost of putting ASCII into Alone:

> xx' `ho'yo` xxx : Letter `AR_` Alone ASCII

Structurally Alone Glyph and Glyph are the same but types are different, Alone here is just a wrapper:

> Alone : i `AR__` Alone i

We can wrap and unwrap things using structural subtyping relations:

: Supertype ( Alone Glyph ) ~ ( Glyph ) > `st` : Alone Glyph `AR_` Glyph

How to use this subtyping relation? Just compose ho and st operators:

> `ho` : i `AR` a `AR_____` a `AR` o `AR____` i `AR` o > `ho'st` : i `AR` a `AR_____` Supertype a `AR` o `AR____` i `AR` o

So that xx' output and xxx input match now:

> xx' `ho'st` xxx : Letter `AR_` ASCII

Congratulations, we just mapped second parameter of xx' covariantly (Alone Glyph) factoring through its Supertype!

You also can factor through Supertype contravariantly by the way:

> `ha` : a `AR` i `AR_____` o `AR` a `AR____` o `AR` i > `ha'st` : a `AR` i `AR_____` Supertype o `AR` a `AR____` o `AR` i

I recommend you to take a second and try to understand what's going on here, just substitute type parameters:

> xx : Letter `AR_` Glyph > xxx : Glyph `AR_` ASCII > xxx `ha'st` xx : Alone Letter `AR_` Glyph

If you think about it, factoring through subtyping relation is a case where notion of variance in Haskell and Scala are intersecting.

Alright, another case. Latin type doesn't contain information about case, and our morphism x just assigns all characters to uppercase:

> x `ha` A `har` Unit = Upper `ha` A `har` Unit

On, and we can factor through subtyping relation here as well to avoid explicitly applying to Unit since it's trivial:

> `st` : Unit `AR` i `AR_____` i > x `har'st` A = Upper `har'st` A

Let's say that at some point we would not be interested in x output so that we want to replace it with some other value:

> x `ho` ??? `har'st` A = Lower `har'st` B

The most obvious solution is to use lambda syntax to ignore an input:

> x `ho` ( \_ -> Lower `har'st` B ) `har'st` A = Lower `har'st` B

But it works only for Arrows, requires parentheses and you have to consume all input... Happy we, there is a better way:

> x `ho'ut` ( Lower `har'st` B ) `har'st` A = Lower `har'st` B

What we are doing here is called factoring through Unit. But why exactly Unit? We'll get to the answer soon.

> `ho'ut` : i `AR` a `AR_____` o `AR____` i `AR` o > `ho` : i `AR` a `AR_____` a `AR` o `AR____` i `AR` o

Now look at those type declarations above. How can we transform first line into second one?

> terminal : a `AR____` Unit > subtype : o `AR_____` Unit `AR` o > subtype `ho'ha` terminal : o `AR_____` a `AR` o

Because it's a terminal object in Arrow category we always have morphisms to Unit per each object.

Just in case if it's not obvious - we can replace output with any object, this type of functions also called constant ones:

> x `ho'ut` ( Digit `har'st` One ) `har'st` A = Digit `har'st` One > xx `ho'ut` ( Digit `har'st` One ) `har'st` Upper `ha` A = Digit `har'st` One > xxx `ho'ut` ( Digit `har'st` One ) `har'st` Letter `ha` Upper `ha` A = Digit `har'st` One

I actually lied in a previous paragraph - there is one object we can not replace output with, it's called Void and it doesn't have any value. Therefore it's tricky to work with it but not impossible:

> `ho'vt` : i `AR` Void `AR_____` Unit `AR____` i `AR` o > `ho` : i `AR` a `AR_____` a `AR` o `AR____` i `AR` o

I bet you have questions... Okay, Void is an initial object but what Unit is doing here? We do exactly the same thing:

> initial : Void `AR____` i > subtype : Unit `AR_____` Void `AR` o > subtype `ho'ha` initial : Unit `AR_____` Void `AR` o

Even more questions! It doesn't seem we actually map everything, initial is equivalent to identity here... The reason for that is weirdness of Void - there is no other candidate object for mapping. Even if it looks like we don't map everything - we still do and it's useful nevertheless, especially for handling representing objects (about it a bit later).

Another point you might wondering about - why do we have exactly these subtyping relations?

: Supertype ( Unit `AR` o ) ~ ( o ) : Supertype ( Void `AR` o ) ~ ( Unit )

Challenge: Unit is 1, Void is 0, Arrow is exponential. What and x⁰ are equal to?

There is another class of objects we can factor through and they consist of other objects. Let's start with products:

> `hop` : a `AR_` o `AR_____` a `AR_` oo `AR_____` a `AR_` o `P` oo

Products have their counterparts - Sums, also known as coproducts - that tells that that morphisms should be flipped:

> `has` : o `RA_` a `AR_____` o `RA_` aa `AR_____` o `RA_` a `S` aa

If you look at types it becomes obvious - factoring through products means that we construct objects from one source object:

> ( A `hop` Lower `ha` B `hop` Letter `ha` Upper `ha` C ) : Unit `AR_` Latin `P` Letter `P` Glyph

In contrast, factoring through Sums means that we deconstruct objects into one target object:

> ( Glyph `ha` Letter `ha` Upper `has` Glyph `ha` Letter `has` Glyph ) : Latin `S` Letter `S` Glyph `AR_` ASCII

Alright, it seems like we covered all objects we can factor through: Supertype, Unit, Void, Product, Sum. Time for examples!

We can initialise Maybe value with Unit and Void objects:

> ( _ : Unit `AR` o ) `ryo` Enter @ Maybe > ( _ : Void `AR` o ) `ryo` Enter @ Maybe

In case of Unit it's easy - many constructors are morphisms with Unit domain (except Unit itself, it's the only one nullary constructor):

> K `ryo` Enter @ Maybe @ Latin > Six `ryo` Enter @ Maybe @ Digit > Tab `ryo` Enter @ Maybe @ Caret

But what if we have some object but we need to provide a morphism? Just ignore the input i.e. use constant function:

> Pass `ho__'ut` True `har` Unit `ryo` Enter @ Maybe @ Boolean

To make it more compact, we can factor through not only Unit but also make another turn on Supertype - since we apply to Unit here:

> Pass `ho'ut'st` True `ryo` Enter @ Maybe @ Boolean

Due to laziness we can ignore Void as well:

> Null `ho'ut'st` True `ryo` Enter @ Maybe @ Boolean

The problem with the latter is that we are providing value from Void - it successfully compiles but doesn't make sense since this value is not going to be presented in functor we are co-representing, this type of functions are also known as absurd:

> ( Pass `ho'ut'st` True `ryo` Enter @ Maybe ) = Exist `har'st` True > ( Null `ho'ut'st` True `ryo` Enter @ Maybe ) = Empty `har__` Unit

But wait, we already have a way to eliminate Void:

> `ho'vt` : i `AR` Void `AR_____` Unit `AR____` i `AR` o

We just need to substitute type parameters for our case...

> `ho'vt` : Void `AR` Void `AR_____` Unit `AR____` Void `AR` Boolean

Both these options have the same result - it's impossible to evaluate therefore impossible to get any Boolean out of it:

> ( Null `ho'ut'st` True ) : Void `AR` Boolean > ( Null `ho'vt` Unit ) : Void `AR` Boolean

Okay, last example. We covered Maybe and Booleans a bit here - both of them are structurally Sums i.e:

: Supertype ( Maybe i ) ~ ( Unit `S` i ) : Supertype ( Boolean ) ~ ( Unit `S` Unit )

We have a nice way to work with Sums if they are in contravariant position i.e. do a case splitting. So that it's possible to compose factoring through Supertype and Sums:

> ( Upper `ha` N `st'has` Lower ) : Maybe Latin `AR_` Letter > ( Upper `ha` N `st'has` Lower `ha` Y ) : Boolean `AR` Letter

Syntactically it's not pattern matching since we rely on parameter positioning, but it does the same job:

> ( Upper `ha` N `st'has` Lower `har'st` Empty ) = Upper `har'st` N > ( Upper `ha` N `st'has` Lower `har'st` Exist `ha` X ) = Lower `har'st` X > ( Upper `ha` N `st'has` Lower `ha` Y `har'st` False ) = Upper `har'st` N > ( Upper `ha` N `st'has` Lower `ha` Y `har'st` True ) = Lower `ha` Y

We even can convert these types (Maybe and Booleans) interchangeably:

> ( False `st'has` True ) : Maybe Unit `AR_` Boolean > ( Empty `st'has` Exist ) : Boolean `AR_` Maybe Unit

Challenge: can you recognise colimit here?