Are there useful applications for the Divisible Type Class?

Question

I've lately been working on an API in Elm where one of the main types is contravariant. So, I've googled around to see what one can do with contravariant types and found that the Contravariant package in Haskell defines the Divisible type class.

It is defined as follows:

class Contravariant f => Divisible f where
  divide  :: (a -> (b, c)) -> f b -> f c -> f a
  conquer :: f a 

It turns out that my particular type does suit the definition of the Divisible type class. While Elm does not support type classes, I do look at Haskell from time to time for some inspiration.

My question: Are there any practical uses for this type class? Are there known APIs out there in Haskell (or other languages) that benefit from this divide-conquer pattern? Are there any gotchas I should be aware of?

Thank you very much for your help.

Answer 1

One example:

Applicative is useful for parsing, because you can turn Applicative parsers of parts into a parser of wholes, needing only a pure function for combining the parts into a whole.

Divisible is useful for serializing (should we call this coparsing now?), because you can turn Divisible serializers of parts into a serializer of wholes, needing only a pure function for splitting the whole into parts.

I haven't actually seen a project that worked this way, but I'm (slowly) working on an Avro implementation for Haskell that does.

When I first came across Divisible I wanted it for divide, and had no idea what possible use conquer could be other than cheating (an f a out of nowhere, for any a?). But to make the Divisible laws check out for my serializers conquer became a "serializer" that encodes anything to zero bytes, which makes a lot of sense.

Answer 2

Here's a possible use case.

In streaming libraries, one can have fold-like constructs like the ones from the foldl package, that are fed a sequence of inputs and return a summary value when the sequence is exhausted.

These folds are contravariant on their inputs, and can be made Divisible. This means that if you have a stream of elements where each element can be somehow decomposed into b and c parts, and you also happen to have a fold that consumes bs and another fold that consumes cs, then you can build a fold that consumes the original stream.

The actual folds from foldl don't implement Divisible, but they could, using a newtype wrapper. In my process-streaming package I have a fold-like type that does implement Divisible.

divide requires the return values of the constituent folds to be of the same type, and that type must be an instance of Monoid. If the folds return different, unrelated monoids, a workaround is to put each return value in a separate field of a tuple, leaving the other field as mempty. This works because a tuple of monoids is itself a Monoid.

Answer 3

I'll examine the example of the core data types in Fritz Henglein's generalized radix sort techniques as implemented by Edward Kmett in the discrimination package.

While there's a great deal going on there, it largely focuses around a type like this

data Group a = Group (forall b . [(a, b)] -> [[b]])

If you have a value of type Group a you essentially must have an equivalence relationship on a because if I give you an association between as and some type b completely unknown to you then you can give me "groupings" of b.

groupId :: Group a -> [a] -> [[a]]
groupId (Group grouper) = grouper . map (\a -> (a, a))

You can see this as a core type for writing a utility library of groupings. For instance, we might want to know that if we can Group a and Group b then we can Group (a, b) (more on this in a second). Henglein's core idea is that if you can start with some basic Groups on integers—we can write very fast Group Int32 implementations via radix sort—and then use combinators to extend them over all types then you will have generalized radix sort to algebraic data types.

---

So how might we build our combinator library?

Well, f :: Group a -> Group b -> Group (a, b) is pretty important in that it lets us make groups of product-like types. Normally, we'd get this from Applicative and liftA2 but Group, you'll notice, is Contravaiant, not a Functor.

So instead we use Divisible

divided :: Group a -> Group b -> Group (a, b)

Notice that this arises in a strange way from

divide :: (a -> (b, c)) -> Group b -> Group c -> Group a

as it has the typical "reversed arrow" character of contravariant things. We can now understand things like divide and conquer in terms of their interpretation on Group.

Divide says that if I want to build a strategy for equating as using strategies for equating bs and cs, I can do the following for any type x

1. Take your partial relation [(a, x)] and map over it with a function f :: a -> (b, c), and a little tuple manipulation, to get a new relation [(b, (c, x))].

2. Use my Group b to discriminate [(b, (c, x))] into [[(c, x)]]

3. Use my Group c to discriminate each [(c, x)] into [[x]] giving me [[[x]]]

4. Flatten the inner layers to get [[x]] like we need

   instance Divisible Group where
     conquer = Group $ return . fmap snd
     divide k (Group l) (Group r) = Group $ \xs ->
       -- a bit more cleverly done here...
       l [ (b, (c, d)) | (a,d) <- xs, let (b, c) = k a] >>= r
   

We also get interpretations of the more tricky Decidable refinement of Divisible

class Divisible f => Decidable f where
  lose   :: (a -> Void) -> f a
  choose :: (a -> Either b c) -> f b -> f c -> f a

instance Decidable Group where
  lose   :: (a -> Void) -> Group a
  choose :: (a -> Either b c) -> Group b -> Group c -> Group a

These read as saying that for any type a of which we can guarantee there are no values (we cannot produce values of Void by any means, a function a -> Void is a means of producing Void given a, thus we must not be able to produce values of a by any means either!) then we immediately get a grouping of zero values

lose _ = Group (\_ -> [])

We also can go a similar game as to divide above except instead of sequencing our use of the input discriminators, we alternate.

---

Using these techniques we build up a library of "Groupable" things, namely Grouping

class Grouping a where
  grouping :: Group a

and note that nearly all the definitions arise from the basic definition atop groupingNat which uses fast monadic vector manipuations to achieve an efficient radix sort.