online - haskell shampoo

¿Por qué las restricciones en los datos son algo malo?

Question

Sé que esta pregunta ha sido formulada y contestada muchas veces, pero aún no entiendo realmente por qué poner restricciones a un tipo de datos es algo malo.

Por ejemplo, tomemos Data.Map ka . Todas las funciones útiles que involucran un Map necesitan una restricción Ord k . Así que hay una restricción implícita en la definición de Data.Map . ¿Por qué es mejor mantenerlo implícito en lugar de dejar que el compilador y los programadores sepan que Data.Map necesita una clave ordenable?

Además, especificar un tipo final en una declaración de tipo es algo común, y uno puede verlo como una forma de "super" restringir un tipo de datos.

Por ejemplo, puedo escribir

data User = User { name :: String }

y eso es aceptable. Sin embargo, es que no es una versión restringida de

data User'' s = User'' { name :: s }

Después de todas, el 99% de las funciones que escribiré para el tipo de User no necesita una String y las pocas que probablemente solo necesiten ser IsString y Show .

Entonces, ¿por qué la versión laxa del User considera mala:

data (IsString s, Show s, ...) => User'''' { name :: s }

¿Mientras que tanto el User como el User'' son considerados buenos?

Estoy preguntando esto, porque muchas veces siento que estoy restringiendo innecesariamente mis definiciones de datos (o incluso funciones), solo para no tener que propagar restricciones.

Actualizar

Por lo que entiendo, las restricciones de tipo de datos solo se aplican al constructor y no se propagan. Entonces, mi pregunta es, ¿por qué las restricciones de tipo de datos no funcionan como se espera (y se propagan)? De todos modos, es una extensión, ¿por qué no tener una nueva extensión que haga los data correctamente, si la comunidad lo consideró útil?

Answer 1

Restricciones

El problema es que las restricciones no son una propiedad del tipo de datos, sino del algoritmo / función que opera en ellas. Diferentes funciones pueden necesitar restricciones diferentes y únicas.

Un ejemplo de Box

Como ejemplo, supongamos que queremos crear un contenedor llamado Box que contiene solo 2 valores.

data Box a = Box a a

Lo queremos:

• ser visible
• Permitir la clasificación de los dos elementos mediante sort

¿Tiene sentido aplicar la restricción de Ord y Show en el tipo de datos? No, porque el tipo de datos en sí mismo solo se puede mostrar o ordenar y, por lo tanto, las restricciones están relacionadas con su uso, no con su definición.

instance (Show a) => Show (Box a) where
show (Box a b) = concat ["''", show a, ", ", show b, "''"]
instance (Ord a) => Ord (Box a) where
compare (Box a b) (Box c d) =
let ca = compare a c
cb = compare b d
in if ca /= EQ then ca else cb

El caso Data.Map

Las restricciones Ord Data.Map sobre el tipo son realmente necesarias solo cuando tenemos> 1 elementos en el contenedor. De lo contrario, el contenedor es utilizable incluso sin una clave Ord . Por ejemplo, este algoritmo:

transf :: Map NonOrd Int -> Map NonOrd Int
transf x =
if Map.null x
then Map.singleton NonOrdA 1
else x

Demo en vivo

funciona bien sin la restricción Ord y siempre produce un mapa no vacío.

Answer 2

El uso de DataTypeContexts reduce la cantidad de programas que puede escribir. Si la mayoría de esos programas ilegales no tienen sentido, podría decir que vale la pena el costo de tiempo de ejecución asociado con el paso de ghc en un diccionario de clase de tipo que no se usa. Por ejemplo, si tuviéramos

data Ord k => MapDTC k a

entonces la transferencia de @ jefffrey es rechazada. Pero probablemente deberíamos tener transf _ = return (NonOrdA, 1) lugar.

En cierto sentido, el contexto es documentación que dice "cada Mapa debe tener claves ordenadas". Si observa todas las funciones en Data.Map obtendrá una conclusión similar: "Cada mapa útil tiene claves ordenadas". Mientras que usted puede crear mapas con claves desordenadas usando

mapKeysMonotonic :: (k1 -> k2) -> Map k1 a -> Map k2 a
singleton :: k2 a -> Map k2 a

Pero en el momento en que intentes hacer algo útil con ellos, acabarás con No instance for Ord k2 un poco más tarde.

Answer 3

TL; DR:
Utilice GADTs para proporcionar contextos de datos implícitos.
No utilice ningún tipo de restricción de datos si podría hacerlo con instancias de Functor, etc.
El mapa es demasiado viejo para cambiarlo a GADT de todos modos. Desplácese hasta la parte inferior si desea ver la implementación del User con GADTs

Usemos un estudio de caso de una bolsa en la que lo único que nos importa es cuántas veces hay algo en ella. (Como una secuencia desordenada. Casi siempre necesitamos una restricción Eq para hacer algo útil con ella.

Usaré la implementación de la lista ineficiente para no enturbiar las aguas sobre el tema Data.Map.

GADTs - la solución al problema de restricción de datos

La manera fácil de hacer lo que está buscando es usar un GADT:

Observe a continuación cómo la restricción Eq no solo lo obliga a usar tipos con una instancia Eq al crear GADTBags, sino que proporciona esa instancia implícitamente donde aparece el constructor GADTBag . Es por eso que count no necesita un contexto Eq , mientras que countV2 sí lo hace, no usa el constructor:

{-# LANGUAGE GADTs #-}
data GADTBag a where
GADTBag :: Eq a => [a] -> GADTBag a
unGADTBag (GADTBag xs) = xs
instance Show a => Show (GADTBag a) where
showsPrec i (GADTBag xs) = showParen (i>9) (("GADTBag " ++ show xs) ++)
count :: a -> GADTBag a -> Int -- no Eq here
count a (GADTBag xs) = length.filter (==a) $ xs -- but == here
countV2 a = length.filter (==a).unGADTBag
size :: GADTBag a -> Int
size (GADTBag xs) = length xs

ghci> count ''l'' (GADTBag "Hello")
2
ghci> :t countV2
countV2 :: Eq a => a -> GADTBag a -> Int

Ahora no necesitábamos la restricción de Ecualización cuando encontramos el tamaño total de la bolsa, pero de todos modos no se desordenó nuestra definición. (Podríamos haber usado size = length . unGADTBag también.)

Ahora hagamos un funtor:

instance Functor GADTBag where
fmap f (GADTBag xs) = GADTBag (map f xs)

oops

DataConstraints_so.lhs:49:30:
Could not deduce (Eq b) arising from a use of `GADTBag''
from the context (Eq a)

Eso no se puede arreglar (con la clase Functor estándar) porque no puedo restringir el tipo de fmap , pero es necesario para la nueva lista.

Versión de restricción de datos

¿Podemos hacer lo que le pedimos? Bueno, sí, excepto que tienes que seguir repitiendo la restricción Eq donde sea que uses el constructor:

{-# LANGUAGE DatatypeContexts #-}
data Eq a => EqBag a = EqBag {unEqBag :: [a]}
deriving Show
count'' a (EqBag xs) = length.filter (==a) $ xs
size'' (EqBag xs) = length xs -- Note: doesn''t use (==) at all

Vayamos a Ghci para descubrir algunas cosas menos bonitas:

ghci> :so DataConstraints
DataConstraints_so.lhs:1:19: Warning:
-XDatatypeContexts is deprecated: It was widely considered a misfeature,
and has been removed from the Haskell language.
[1 of 1] Compiling Main ( DataConstraints_so.lhs, interpreted )
Ok, modules loaded: Main.
ghci> :t count
count :: a -> GADTBag a -> Int
ghci> :t count''
count'' :: Eq a => a -> EqBag a -> Int
ghci> :t size
size :: GADTBag a -> Int
ghci> :t size''
size'' :: Eq a => EqBag a -> Int
ghci> 

Por lo tanto, nuestra función de cuenta de EqBag requiere una restricción de ecuación, que creo que es perfectamente razonable, pero nuestra función de tamaño también requiere una, que es menos bonita. Esto se debe a que el tipo del constructor EqBag es EqBag :: Eq a => [a] -> EqBag a , y esta restricción debe agregarse cada vez.

Tampoco podemos hacer un funtor aquí:

instance Functor EqBag where
fmap f (EqBag xs) = EqBag (map f xs)

por exactamente la misma razón que con el GADTBag

Bolsas sin restricciones

data ListBag a = ListBag {unListBag :: [a]}
deriving Show
count'''' a = length . filter (==a) . unListBag
size'''' = length . unListBag
instance Functor ListBag where
fmap f (ListBag xs) = ListBag (map f xs)

Ahora los tipos de conteo '''' y show '''' son exactamente como esperamos, y podemos usar clases de constructor estándar como Functor:

ghci> :t count''''
count'''' :: Eq a => a -> ListBag a -> Int
ghci> :t size''''
size'''' :: ListBag a -> Int
ghci> fmap (Data.Char.ord) (ListBag "hello")
ListBag {unListBag = [104,101,108,108,111]}
ghci> 

Comparacion y conclusiones

La versión de GADT propaga automágicamente la restricción Eq en todos los lugares donde se usa el constructor. El comprobador de tipos puede confiar en que haya una instancia de Eq, porque no puede utilizar el constructor para un tipo que no sea de EQ.

La versión de DatatypeContexts obliga al programador a propagar manualmente la restricción Eq, lo cual está bien para mí si lo desea, pero está en desuso porque no le da nada más que el GADT y fue visto por muchos como inútil y molesto.

La versión sin restricciones es buena porque no le impide crear instancias de Functor, Monad, etc. Las restricciones se escriben exactamente cuando se necesitan, ni más ni menos. Data.Map usa la versión sin restricciones en parte porque sin restricciones generalmente se considera la más flexible, pero también en parte porque precede a los GADT por algún margen, y debe haber una razón convincente para romper potencialmente el código existente.

¿Qué hay de tu excelente ejemplo de User ?

Creo que es un gran ejemplo de un tipo de datos de un solo propósito que se beneficia de una restricción en el tipo, y le recomiendo que use un GADT para implementarlo.

(Dicho esto, a veces tengo un tipo de datos de un solo propósito y termino haciéndolo sin restricciones polimórficas solo porque me encanta usar Functor (y Aplicativo), y preferiría usar fmap de mapBag porque siento que es más claro).

{-# LANGUAGE GADTs #-}
import Data.String
data User s where
User :: (IsString s, Show s) => s -> User s
name :: User s -> s
name (User s) = s
instance Show (User s) where -- cool, no Show context
showsPrec i (User s) = showParen (i>9) (("User " ++ show s) ++)
instance (IsString s, Show s) => IsString (User s) where
fromString = User . fromString

Tenga en fromString que fromString sí construye un valor de tipo User a , necesitamos el contexto explícitamente. Después de todo, User :: (IsString s, Show s) => s -> User s con el constructor User :: (IsString s, Show s) => s -> User s . El constructor del User elimina la necesidad de un contexto explícito cuando hacemos un patrón de coincidencia (destrucción), porque ya impuso la restricción cuando la usamos como un constructor.

No necesitábamos el contexto Mostrar en la instancia Mostrar porque usamos (User s) en el lado izquierdo en una coincidencia de patrón.