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
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?
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.
Prism' s a is only inhabited for some combinations of
a but not others, I thought a good choice for my
C typeclass might be a proof that there exists a prism from
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.
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
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
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?
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".
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 :)