Tipos asociados y elementos de contenedor

Question

Creo que he pedido esto en Haskell-Cafe en algún momento, pero maldita sea si puedo encontrar la respuesta ahora ... Así que lo vuelvo a pedir aquí, así que espero que en el futuro pueda encontrar la respuesta!

Haskell es fantástico en el tratamiento del polimorfismo paramétrico. Pero el problema es que no todo es paramétrico. Como ejemplo trivial, supongamos que queremos extraer el primer elemento de datos de un contenedor. Para un tipo paramétrico, eso es trivial:

 
class HasFirst c where 
    first :: c x -> Maybe x 

instance HasFirst [] where 
    first [] = Nothing 
    first (x:_) = Just x 

Ahora tratar de escribir una instancia para ByteString. No puedes. Su tipo no menciona el tipo de elemento. Tampoco puede escribir una instancia para Set, porque requiere una restricción Ord, pero el encabezado de clase no menciona el tipo de elemento, por lo que no puede restringirlo.

tipos asociados proporcionan una clara forma de solucionar estos problemas por completo:

 
class HasFirst c where 
    type Element c :: * 
    first :: c -> Maybe (Element c) 

instance HasFirst [x] where 
    type Element [x] = x 
    first [] = Nothing 
    first (x:_) = Just x 

instance HasFirst ByteString where 
    type Element ByteString = Word8 
    first b = b ! 0 

instance Ord x => HasFirst (Set x) where 
    type Element (Set x) = x 
    first s = findMin s 

Ahora tenemos un nuevo problema, sin embargo. Considere la posibilidad de tratar de "arreglar" Functor para que funcione para todos los tipos de contenedores:

 
class Functor f where 
    type Element f :: * 
    fmap :: (Functor f2) => (Element f -> Element f2) -> f -> f2 

Esto no funciona en absoluto. Dice que si tenemos una función del tipo de elemento de f para el tipo de elemento de f2, podemos convertir un f en un f2. Hasta aquí todo bien. Sin embargo, aparentemente hay de ninguna manera para exigir que f y f2 sean el mismo tipo de contenedor.

Bajo el Functor definición existente, tenemos

 
fmap :: (x -> y) -> [x] -> [y] 
fmap :: (x -> y) -> Seq x -> Seq y 
fmap :: (x -> y) -> IO x -> IO y 

Pero tenemos no tienen fmap :: (x -> y) -> IO x -> [y]. Eso es completamente imposible. Pero la definición de clase anterior lo permite.

¿Alguien sabe cómo explicarle al sistema de tipo qué en realidad significa?

Editar

Los trabajos anteriores mediante la definición de una forma de calcular un tipo de elemento de un tipo de contenedor. ¿Qué pasa si tratas de hacerlo al revés? ¿Define una función para calcular un tipo de contenedor a partir de un tipo de elemento? ¿Funciona eso más fácil?

Answer 1

Bueno, el problema es que no está claro lo que se supone que significa el Functor revisado. Por ejemplo, considere ByteString. Un ByteString solo se puede asignar reemplazando cada elemento Word8 con un elemento del mismo tipo. Pero Functor es para estructuras paramétricas mappable. En realidad, hay dos nociones conflictivas de mapeo aquí:

• Mapeo rígido (es decirtransformando cada elemento de una estructura sin cambiar su tipo)
• mapeo paramétrico (es decir, la transformación de cada elemento de una estructura de cualquier tipo)

Por lo tanto, en este caso, no se puede explicar al sistema de tipos lo quieres decir, porque no tiene mucho sentido. Puede, sin embargo, cambia lo que quiere decir :)

mapeo rígido es fácil expresar con las familias de tipo:

class RigidMap f where 
    type Element f :: * 
    rigidMap :: (Element f -> Element f) -> f -> f 

En cuanto a la cartografía paramétrica, hay varias formas de hacerlo. La forma más simple sería retener el actual Functor tal como está. En conjunto, estas clases cubren estructuras como ByteString, [], Seq, y así sucesivamente. Sin embargo, todos caen en Set y Map, debido a la restricción Ord en los valores. Felizmente, la extensión constraint kinds llegando GHC 7.4 permite a solucionar este problema:

class RFunctor f where 
    type Element f a :: Constraint 
    type Element f a =() -- default empty constraint 
    fmap :: (Element f a, Element f b) => (a -> b) -> f a -> f b 

Aquí, estamos diciendo que cada caso debe tener una clase de tipos asociado restricción. Por ejemplo, la instancia de Set tendrá Element Set a = Ord a, para indicar que Set s solo se puede construir si hay una instancia Ord disponible para ese tipo. Se acepta todo lo que pueda aparecer a la izquierda de =>. Podemos definir nuestros casos anteriores exactamente como estaban, pero también podemos hacer Set y Map:

instance RFunctor Set where 
    type Element Set a = Ord a 
    fmap = Set.map 

instance RFunctor Map where 
    type Element Map a = Ord a 
    fmap = Map.map 

Sin embargo, es bastante molesto tener que utilizar dos interfaces separadas para la asignación rígida y mapeo paramétrico restringido. De hecho, ¿no es esto último una generalización de lo primero? Tenga en cuenta la diferencia entre Set, que solo puede contener instancias de Ord y ByteString, que solo pueden contener Word8 s. ¿Seguramente podemos expresar eso como una restricción más?

aplicamos el mismo truco hecho a HasFirst (es decir, dar ejemplos para toda la estructura y el uso de una familia tipo para exponer el tipo de elemento), e introducir una nueva familia restricción asociada:

class Mappable f where 
    type Element f :: * 
    type Result f a r :: Constraint 
    map :: (Result f a r) => (Element f -> a) -> f -> r 

La idea aquí es que Result f a r expresa las restricciones que necesita en el tipo de valor (como Ord a) y también limita el tipo de contenedor resultante, sin embargo, necesita hacerlo; presumiblemente, para asegurarse de que tiene el tipo de un mismo tipo de contenedor de a s. Por ejemplo, Result [a] b r presumiblemente requerirá que r sea [b], y Result ByteString b r requerirá que b sea , y r sea ByteString.

Las familias de tipo ya nos dan lo que necesitamos expresar "aquí": una restricción de igualdad de tipo. Podemos decir (a ~ b) => ... para requerir que a y b sean del mismo tipo. Podemos, por supuesto, usar esto en las definiciones de familia de restricción. Entonces, tenemos todo lo que necesitamos; en las instancias:

instance Mappable [a] where 
    type Element [a] = a 
    type Result [a] b r = r ~ [b] 
    -- The type in this case works out as: 
    -- map :: (r ~ [b]) => (a -> b) -> [a] -> r 
    -- which simplifies to: 
    -- map :: (a -> b) -> [a] -> [b] 
    map = Prelude.map 

instance Mappable ByteString where 
    type Element ByteString = Word8 
    type Result ByteString a r = (a ~ Word8, r ~ ByteString) 
    -- The type is: 
    -- map :: (b ~ Word8, r ~ ByteString) => (Word8 -> b) -> ByteString -> r 
    -- which simplifies to: 
    -- map :: (Word8 -> Word8) -> ByteString -> ByteString 
    map = ByteString.map 

instance (Ord a) => Mappable (Set a) where 
    type Element (Set a) = a 
    type Result (Set a) b r = (Ord b, r ~ Set b) 
    -- The type is: 
    -- map :: (Ord a, Ord b, r ~ Set b) => (a -> b) -> Set a -> r 
    -- (note the (Ord a) constraint from the instance head) 
    -- which simplifies to: 
    -- map :: (Ord a, Ord b) => (a -> b) -> Set a -> Set b 
    map = Set.map 

Perfecto! Podemos definir instancias para cualquier tipo de contenedor que deseemos, rígidas, paramétricas o paramétricas, pero restringidas, y los tipos funcionan perfectamente.

Descargo de responsabilidad: Todavía no he probado GHC 7.4, así que no sé si algo de esto realmente compila o funciona, pero creo que las ideas básicas son buenas.

Answer 2

Quiere constraint kinds, disponible en ghc 7.4.