Search code examples
haskelltypesfunctional-programmingelmtype-theory

Are there useful applications for the Divisible Type Class?

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.

Solution

  • 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.