¿Hay aplicaciones útiles para la clase de Tipo Divisible?

Examinaré el ejemplo de los tipos de datos principales en las técnicas de ordenación radix generalizada de Fritz Henglein implementadas por Edward Kmett en el paquete discrimination.

Si bien hay mucho que hacer allí, en gran medida se centra en un tipo como este{[58]]}

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

Si tienes un valor de tipo Group a esencialmente debes tener una relación de equivalencia en a porque si te doy una asociación entre a s y algún tipo b completamente desconocido para ti entonces puedes darme "agrupaciones" de b.

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

Puede ver esto como un tipo de núcleo para escribir una biblioteca de utilidades de agrupaciones. Por ejemplo, podríamos querer saber que si podemos Group a y Group b luego podemos Group (a, b) (más sobre esto en un segundo). La idea central de Henglein es que si puedes comenzar con algunas Groups básicas en enteros - podemos escribir implementaciones muy rápidas Group Int32 a través de radix sort-y luego usar combinadores para extenderlas sobre todos los tipos, entonces tendrás una tipos de datos algebraicos.

Entonces, ¿cómo podríamos construir nuestra biblioteca combinadora?

Bueno, f :: Group a -> Group b -> Group (a, b) es bastante importante ya que nos permite hacer grupos de tipos similares a productos. Normalmente, obtendríamos esto de Applicative y liftA2 pero Group, te darás cuenta, es Contravaiant, no un Functor.

Así que en su lugar usamos Divisible

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

Observe que esto surge de una manera extraña de{[58]]}

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

Ya que tiene el típico carácter de "flecha invertida" de las cosas contravariantes. Ahora podemos entender cosas como divide y conquer en términos de su interpretación en Group.

Divide dice que si quiero construir una estrategia para igualar a s usando estrategias para igualar b s y c s, puedo hacer lo siguiente para cualquier tipo x

1. Toma tu relación parcial [(a, x)] y mapéala con una función f :: a -> (b, c), y una pequeña manipulación de tupla, para obtener una nueva relación [(b, (c, x))].

2. Usa mi Group b para discriminar [(b, (c, x))] en [[(c, x)]]

3. Usa mi Group c para discriminar cada [(c, x)] en [[x]] dándome [[[x]]]

4. Aplanar las capas internas para obtener [[x]] como necesitamos

   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
   

También tenemos interpretaciones de lo más complicado Decidable refinamiento de 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

Estos se leen como diciendo que para cualquier tipo a del cual podemos garantizar que no hay valores (no podemos producir valores de Void por ningún medio, una función a -> Void es un medio de produciendo Void dado a, por lo tanto no debemos ser capaces de producir valores de a por ningún medio tampoco!) entonces inmediatamente obtenemos una agrupación de valores cero

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

También podemos ir a un juego similar a divide anterior, excepto que en lugar de secuenciar nuestro uso de los discriminadores de entrada, alternamos.

Usando estas técnicas construimos una biblioteca de cosas "Group capaces", a saber Grouping

class Grouping a where
  grouping :: Group a

Y tenga en cuenta que casi todas las definiciones surgen de la definición básica atop groupingNat que utiliza manipulaciones vectoriales monádicas rápidas para lograr una clasificación radix eficiente.