Issues with subtractive types

I tried to expand on my earlier attempt at understanding root types, but I hit several obstacles. Here is a summary of those obstacles, in case future-me or someone else feels like trying again.

Goals

The conversation began with Naperian types, and the way in which they satisfy the same laws as mathematical logarithms, except at the type level. For example, the law log_b xy = log_b x + log_b y would translate to a function of type

logProduct :: Log b (a1, a2) -> Either (Log b a1) (Log b a2)

where, as usual, pairs represent multiplication and Either represents a sum. We would also expect a function with the converse type, and we would expect the two functions to form an isomorphism.

My goal would be to find implementations for Log and the other inverse types such that the corresponding isomorphisms exist and are useful. As the rest of the post will demonstrate, "exists" is already quite a strong requirement.

I should mention before moving on that yes, I am familiar with "The Two Dualities of Computation: Negative and Fractional Types", and I am intentionally using a different approach. Their non-deterministic invertible language in quite interesting, but ultimately too weird for me.

I would prefer to find a way to implement negative and fractional stuff as Haskell datatypes, or failing that, to understand why it can't be done. Today's post is about the latter: if negative and fractional types can exist in Haskell, then identities such as 0 ↔ x + -x wouldn't be valid for all types x, like they are in that paper.

Naïve definitions

Since subtraction is the inverse of addition, I tried to define a subtractive type and the other inverses types in term of the types we already have.

type a :+: b = Either a b
type a :*: b = (a, b)

data ab :-: b where
  MkSub :: a -> (a :+: b) :-: b

data ab :/: b where
  MkDiv :: a -> (a :*: b) :/: b

data Log b a where
  MkLog :: p -> Log b (p -> b)

data Root n a where
  MkRoot :: b -> Root n (n -> b)

One obvious problem with those definitions is that they don't support any of the math identities, except for the ones used in the definitions themselves: x + y - y = x, etc. For most types a, the type a :-: b isn't even inhabited, so while we might be able to implement absurd-style isomorphisms, the result would be completely useless.

Isomorphisms to the rescue

In the reddit comment linked at the top of this post, I worked around the problem via the hypothesis that maybe we shouldn't expect math identities to correspond to type isomorphisms so directly. Instead, I postulated an extra operator which would lift an isomorphism between a and a' to an isomorphism between a :-: b and a' :-: b, and similarly for the right-hand side and for the other type operators. It worked well enough, but since this transformation isn't constructive, we still don't get useful isomorphic functions at the end.

So, can we make the transformation constructive? Something like this:

data a :-: b where
  MkSub :: r -> Iso a (r :+: b) -> a :-: b

data a :/: b where
  MkDiv :: r -> Iso a (r :*: b) -> a :/: b

data Log b a where
  MkLog :: p -> Iso a (p -> b) -> Log b a

data Root n a where
  MkRoot :: b -> Iso a (n -> b) -> Root n a

By using id as the Iso, we can construct the same inhabitants as with the previous definitions. In addition, we can now constructively lift an isomorphism on the left- or right-hand side to an isomorphism on the whole type. The code for doing this is a bit longer than I'd like, but the idea is that since isomorphisms can already be lifted to either side of a (:+:), (:*:), or (->), we should therefore be able to concatenate an isomorphism for the left- or right-hand side with the existing Iso. For example:

liftRightAdd :: forall a b b'
              . Iso b b'
             -> Iso (a :+: b) (a :+: b')
liftRightAdd isoB = ...

liftRightSub :: forall a b b'
              . Iso b b'
             -> Iso (a :-: b) (a :-: b')
liftRightSub isoB = Iso fwdS bwdS
  where
    fwdS :: a :-: b -> a :-: b'
    fwdS (MkSub r iso) = MkSub r (liftIso iso)
      where
        liftIso :: Iso a (r :+: b) -> Iso a (r :+: b')
        liftIso iso = liftRightAdd isoB . iso
    
    bwdS :: a :-: b' -> a :-: b
    bwdS (MkSub r iso) = MkSub r (liftIso iso)
      where
        liftIso :: Iso a (r :+: b') -> Iso a (r :+: b)
        liftIso iso = liftRightAdd (inverse isoB) . iso)

With those tools, we should be able to take a non-constructive transformation like the one I wrote in my reddit comment:

log_b(a1) + log_b(a2) ~ Either (Log b a1) (Log b a2)
                     ≈≈ Either (Log b (p1 -> b))
                               (Log b (p2 -> b))
                      ≈ Either p1 p2
                      ≈ Log b (Either p1 p2 -> b)
                     ≈≈ Log b (p1 -> b, p2 -> b)
                     ≈≈ Log b (a1, a2)
                      ~ log_b(a1*a2)

And translate it into a constructive version:

addLogs :: forall a1 a2 b. Iso (Log b a1 :+: Log b a2)
                               (Log b (a1 :*: a2))
          -- Log b (a1 :*: a2)
addLogs = liftRightLog (liftBothMul (inverse asExp1)
                                    (inverse asExp2))
          -- Log b ((p1 -> b) :*: (p2 -> b))
        . liftRightLog expSum
          -- Log b (p1 :+: p2 -> b)
        . inverse logExp
          -- p1 :+: p2
        . liftBothAdd logExp logExp
          -- Log b (p1 -> b) :+: Log b (p2 -> b)
        . liftBothAdd (liftRightLog asExp1)
                      (liftRightLog asExp2)
          -- Log b a1 :+: Log b a2
  where
    asExp1 :: Iso a1 (P1 -> b)
    asExp2 :: Iso a2 (P2 -> b)

expSum :: Iso (a1 :+: a2 -> b)
              ((a1 -> b) :*: (a2 -> b))
logExp:: Iso (Log b (p -> b))
             p

Success? Not so fast.

Impossible isomorphisms

In order to execute the above constructive proof, we must of course implement all the smaller isomorphisms on which it is based. Two of them, asExp1 and asExp2, seem pretty silly: can we really expect any type a1 to be isomorphic to a function of the form p1 -> b, for any type b of our choosing?

I had originally postulated that I could do this because in my original definition for Log b a1, log types were only inhabited when a1 had the required form p1 -> b. With the new Iso-based definition, I'm no longer sure I can do this, and even with the old definition, it was only ever justified to transform Log b a1 into Log b (p1 -> b), not to transform a naked a1 into p1 -> b.

However, if we simply pick p1 = Log b a1, then the math identity b^{log_b x} = x justifies the principle. Can we write a constructive version of this identity?

One direction is easy:

mkExpLog :: a -> (Log b a -> b)
mkExpLog x (MkLog p (Iso fwd _)) = fwd x p

But the other direction direction is impossible. It would allow us to implement unsafeCoerce!

unExpLog :: (Log b a -> b) -> a

unsafeCoerce' :: b -> a
unsafeCoerce' = unExpLog . const

Similar issues occur with identities from the other inverse types. With a constructive version of the identity x - x = 0, for example, we can construct an inhabitant for the empty type:

unSubSelf :: a :-: a -> Void

subSelf :: [()] :-: [()]
subSelf = MkSub () (Iso fwdL bwdL)
  where
    fwdL :: [()] -> () :+: [()]
    fwdL []      = Left ()
    fwdL (():xs) = Right xs
    
    bwdL :: () :+: [()] -> [()]
    bwdL (Left  ()) = []
    bwdL (Right xs) = ():xs

bottom :: Void
bottom = unSubSelf subSelf

The fact that a recursive type is used in this counter-example hints at an explanation of the issue. The identity x - x = 0 is certainly true in math, for any number x. So at least for types with exactly x inhabitants, we would expect the isomorphism to hold. But in this case, the type [()] has infinitely-many inhabitants, and as we know from math, ∞ - ∞ is not zero, it's an indeterminate form.

Here is another implementation of the empty type, based on the identities x / x = 1 and x / y = x * (1/y):

mkDivSelf :: () -> a :/: a
mkTimesReciprocal :: a :/: b
                  -> a :*: (() :/: b)

divZero :: Void :/: Void
divZero = mkDivSelf ()

bottom' :: Void
bottom' = fst (mkTimesReciprocal divZero)

I haven't managed to derive a contradiction from any of the root identities, but they seem just as impossible to implement.

Restricted isomorphisms

Okay, so the indeterminate forms ∞ - ∞ and 0 / 0 both led to contradictions. In math, we work around the problem by saying that the division identities are only valid when the denominator is non-zero, and we don't even bother mentioning infinity because it's usually not a member of our universe of discourse, the real numbers for example.

In the world of types, instead of forbidding particular elements such as zero, it's much more common to require a witness proving that the types under consideration are valid for the current operation. In Agda, this would be a predicate on Set, while in Haskell, it would be a typeclass constraint. So, if future me is reading this and wants to continue exploring the world of inverse types, I leave him with the following recommendation: try looking for typeclass constraints under which the identities don't lead to contradictions, or even better, under which they can actually be implemented.