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 :)

## No comments:

Post a Comment