Prisms lead to typeclasses for subtractive types

In my last post, I identified some issues with subtractive types, namely that math identities such as ∀ a. a + -a = 0, once they are translated into Haskell, would not be valid for all a. More precisely, the existence of a function of type

cancelSub :: forall a. (a :+: Negative a) -> Zero

would make it easy to implement a contradiction, regardless of the way in which we represent Negative a:

type a :+: b = Either a b
type Zero = Void

contradiction :: Void
contradiction = cancelSub (Left ())

I concluded by blaming the unconstrained forall. That is, I was hoping that the identity could be saved by finding some typeclass C such that C a => (a :+: Negative a) -> Void would be inhabited, or something along those lines. But what should C look like?

Prisms

Earlier today, I was re-listening to Edward Kmett on Lenses, in the first Haskell Cast episode. While explaining Prisms at 38:30, Kmett explained that a Lens' s a splits an s into a product consisting of an a and of something else, and that correspondingly, a Prism' s a splits an s into a sum consisting of an a and of something else. It occurred to me that the first "something else" should be s :/: a, while the second "something else" should be s :-: a.

Since Prism' s a is only inhabited for some combinations of s and a but not others, I thought a good choice for my C typeclass might be a proof that there exists a prism from s to a.

cancelSub :: HasPrism a (Negative a)
          => (a :+: Negative a) -> Void

That is, instead of restricting which types can be negated, let's restrict which types are allowed to appear together on the left- and right-hand sides of a subtractive type.

Four typeclasses

All right, so what should the HasPrism typeclass look like? In the podcast, Kmett explains that we can "construct the whole thing out of the target of a prism", and that we can pattern-match on the whole thing to see if it contains the target. In other words:

class HasPrism s a where
    construct :: a -> s
    match :: s -> Maybe a

This Maybe a discards the case I am interested in, the s :-: a. Let's ask the typeclass to provide a representation for this type, so we can give a more precise type to match.

class HasPrism s a where
    type s :-: a
    constructLeft :: a -> s
    constructRight :: (s :-: a) -> s
    match :: s -> Either a (s :-: a)

Our typeclass now has three methods, for converting back and forth between s and its two alternatives. We can combine those three methods into a single bijection, and with this final transformation, we obtain a form which is easily transferable to the other inverse types:

class Subtractable a b where
    type a :-: b
    asSub :: Iso a ((a :-: b) :+: b)

class Divisible a b where
    type a :/: b
    asDiv :: Iso a ((a :/: b) :*: b)

class Naperian b a where
    type Log b a
    asLog :: Iso a (Log b a -> b)

class Rootable n a where
    type Root n a
    asRoot :: Iso a (n -> Root n a)

Routing around the contradiction

The real test for these new definitions is whether they allow us to define constructive versions of the math identities for subtraction, division, logarithms and roots. Once annotated with the proper type class constraint, does cancelSub still lead to a contradiction? If not, can it be implemented?

It can!

type Negative a = Zero :-: a

cancelSub :: forall a. Subtractable Zero a
          => Iso (a :+: Negative a) Zero
         -- a :+: Negative a
cancelSub = swap
         -- Negative a :+: a
        >>> inverse iso
         -- Zero
  where
    iso :: Iso Zero (Negative a :+: a)
    iso = asSub

The math version of the constrained type is still ∀ a. a + -a = 0, but with a new proviso "whenever -a exists". It's still the same identity, it's just that with real numbers, -a always exists, so the proviso does not usually need to be spelled out.

In the world of types, Negative a does not always exist. If fact, there's only one possible instance of the form Subtractable Zero a:

instance Subtractable Zero Zero where
    type Zero :-: Zero = Zero
    
    asSub :: Iso Zero ((Zero :-: Zero) :+: Zero)
    asSub = Iso Right (either id id)

In other words, in the world of types, the proviso "whenever -a exists" simply means "when a = 0".

Other identities

I wish I could say that all the other identities become straightforward to implement once we add the appropriate typeclass constraints, but alas, this is not the case. I plan to discuss the remaining issues in a subsequent post.

For now, I am content to celebrate the fact that at least one contradiction has been slain :)