Я ☞ Articles ☞ Sequentional subtraction on types

Previously: Reinventing records and variants

Subtraction as addition inverse

As we already know that there are two main ways to combine types - Product and Sum. However, I didn’t tell you about another one - Minus.

Subtraction (which is signified by the minus sign, –) is one of the four arithmetic operations along with addition, multiplication and division. Subtraction is an operation that represents removal of objects from a collection.

The next reasonable question would be: how is that implemented? Instead of answering to this question directly, I would start with some arithmetical properties:

A `S` B `M` B ===> A
A `S` B `M` A ===> B
 
A `M` A ===> Void
B `M` B ===> Void

Some of you may recognize invertibility and additive identity (Void) here.

Keeping properties above in mind we are ready to finally implement it:

type family Minus r e where
 Minus (e `S` ee) e = ee
 Minus (ee `S` e) e = ee
 Minus (ee `S` eee) e = ee `M` e `S` eee
 Minus e e = Void

Case splitting composition

In previous chapter the usage of Minus has been demonstrated with on expression:

on: entire `AR_` entire `M` target `S` target

Let’s take ASCII type structure as an example - our imaginary task here is to focus on Digit. In order to get there, we need to get through Glyph case:

on @Glyph: ASCII `AR_` ASCII `M` Glyph `S` Glyph
on @Digit: Glyph `AR_` Glyph `M` Digit `S` Digit

We can compose these, but we would get a monstrous result type:

on @Glyph `ho'ho` on @Symbol: ASCII `AR_` ASCII `M` Glyph `S` (Glyph `M` Digit `S` Digit)

In order to get access to Digit here, we need got get trough layers of wrapped functors (Arrow and Sum):

on @Glyph `ho'ho` on @Symbol `ho` f
on @Glyph `ho'ho` on @Symbol `ho'ho` ff
on @Glyph `ho'ho` on @Symbol `ho'ho'ho` fff
on @Glyph `ho'ho` on @Symbol `ho'ho'ho'ho` ffff
 
f: ((ASCII `M` Glyph) `S` ((Glyph `M` Digit) `S` Digit)) `AR__` r
ff: (Glyph `S` ((Glyph `M` Digit) `S` Digit)) `AR__` r
fff: ((Glyph `M` Digit) `S` Digit) `AR__` r
fff: Digit `AR__` r

I intentionally put parentheses everywhere so that even if you are not get used to the fact that all operators are left-associative.

We can make our life a bit easier if we use Sum associativity property and rearrange parentheses using the fact that Sum (Sum e ee) eee is a supertype of Sum e (Sum ee eee):

on @Glyph `ho'ho` on @Symbol `ho'he` f
on @Glyph `ho'ho` on @Symbol `ho'he'ho` ff
 
f: ((ASCII `M` Glyph) `S` (Glyph `M` Digit)) `S` Digit `AR__` r
ff: Digit `AR__` r

Despite the fact the code snippets above is a great example of extreme composability, you could imagine how hard would it be to reason over it without typed holes.

Is there a way to compose?

By looking at these expressions you may ask…

on @Glyph: ASCII `AR_` ASCII `M` Glyph `S` Glyph
on @Digit: Glyph `AR_` Glyph `M` Digit `S` Digit

… “isn’t there a way to compose them in the same way we compose functions?“. So did I!

type Matcher origin target = origin `AR_` origin `M` target `S` target

Using a type alias above our type signatures look unified:

on @Glyph: Matcher ASCII Glyph
on @Digit: Matcher Glyph Digit

What you want to get here is to compose these on expressions so that we can get this as a result:

on @Glyph: Matcher ASCII Digit

However, it’s impossible! The reason is that subtraction neither associative nor transitive:

type ASCII = Caret `S` Glyph
type Glyph = Letter `S` Digit `S` Symbol
 
ASCII `M` Glyph ===> Caret
Glyph `M` Digit ===> Letter `S` Symbol
 
ASCII `M` Glyph `M` ===> Caret
 
ASCII `M` Digit ===> ???

But we still have good cards in the game.

Unifying approach: ignorance

Since Minus is not very composable, let’s just dim it!

on @Glyph: ASCII `AR_` ASCII `M` Glyph `S` Glyph
 
on @Glyph `ho` dim: ASCII `AR_` Unit `S` Glyph

So that we can wrap it as Maybe and use yok operators for effect composition:

... x = intro @Maybe x
 `yok___` Check `ha` Maybe `ha` dim `ha` on @Glyph
 `yok___` Check `ha` Maybe `ha` dim `ha` on @Digit

Unifying approach: completion

What if instead of ignoring the subtraction difference we would complete it up to a common type? In our case it’s ASCII:

on @Glyph: ASCII `AR_` ASCII `M` Glyph `S` Glyph
on @Digit: Glyph `AR_` Glyph `M` Digit `S` Digit
 
on @Glyph `ho'yoi` Caret: ASCII `AR_` ASCII `S` Glyph
on @Digit `ho'yoi` Digit: Glyph `AR_` ASCII `S` Glyph

However, in order to do that we need to compute the difference:

type ASCII = Caret `S` Glyph
type Glyph = Letter `S` Digit `S` Symbol
 
ASCII `M` Glyph ===> Caret
Glyph `M` Digit ===> Letter `S` Symbol

Constructor names match corresponded types:

... x = intro @(Error ASCII) x
 `yok___` on @Glyph `ho___'yoi` Caret
 `yok___` on @Digit `ho___'yoi` Glyph `ha__` Letter `la` Symbol