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?
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.
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 ofy
, thenMinus x y
isVoid
It’s incorrect in both ways:
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.