Sequentional subtraction on types

It’s time to start learning arithmetics on types in Я. You definitely should know about sums and products, but what about subtraction? And what else should be there?

2 Likes
Minus (ee + eee) e = ee - e + eee

I find this equation problematic.
Even arithmetically, this is only valid if the result of ee - e can be negative. But what even is a negative type? I would expect

Minus (x + (e + y)) e = x + y

but if Minus x e has no match in the type family equations, then the identity above does not hold.

I would expect

 Minus (x + (e + y)) e = x + y

This is why we consider this operation as not transitive. It’s designed to look up for exact constructor, not recursively looking at all its member contents.

Type family declaration is not ideal though since it gives left biased preferences and it’s possible to get a type inside another type if it’s the left one.

Even arithmetically, this is only valid if the result of ee - e can be negative

Could you elaborate? I’m not sure I understand it here.

Consider the closest analogue on the term level: Subtraction of natural numbers. In order to be total, we must truncate:

minus :: Natural -> Natural -> Natural
x `minus` y = if x <= y then 0 else x-y

On the type level, this says: If type x is a sub-type of y, then Minus x y is Void.
Say we adopt your Minus definition. Consider

minus (2 + 5) 4
= minus 2 4 + 5 -- your structural recursion
= 0 + 5
= 5

which is distinct from minus 7 4 = 3.

How can a binary function be transitive? I know this attribute only of binary relations.

1 Like

A more stable definition, at least in my eyes, would be a type class that establishes a constructive sub-typing relationship. The witness would be a difference type. Suppose we have a category Iso where from each
Iso a b we can derive both a -> b and b -> a.

class SubTypeOf x y where
   type Minus y x :: Type
   split :: Iso (Either x (Minus y x)) y

This says: If there is some type z such that there exists an isomorphism between y and x + z then x is a sub-type of y. You obtain the embedding x -> y by extracting the function Either x z -> y from the Iso and pre-composing it with Left.

Likewise, consider

class HasField x y where
   type Div y x :: Type
   quot :: Iso (x,Div y x) y

This is essentially a Lens y x (see here), but one where the part of y that is untouched by the lens is explicitly given as the type Div y x. There you have your type-level quotients.

If type x is a sub-type of y, then Minus x y is Void

It’s incorrect in both ways:

  • In Я subtyping is a completely another thing.
  • But if by subtyping you mean that x is a member of y Sum - result is still Minus x y. It’s Void only if we Minus x x.

Pardon my harshness, I don’t care what subtyping is in Я. I care about set-theoretical, or type-theoretical, sub-types. If your Minus is not intended to be something like a set-theoretical difference, then that is fine. But in the blog post your are using it as such. Hence you should care about soundness to some extent.

I don’t care what subtyping is in Я

Hence you should care

Gotcha.