type constraint haskell

Clases de tipos y sobrecarga, ¿cuál es la conexión?

Question

Actualmente estoy tratando de envolver mi cabeza en torno a las clases de tipos y las instancias y todavía no entiendo muy bien cuál es su punto. Tengo dos preguntas al respecto hasta ahora:

1) ¿Por qué es necesario tener una clase de tipo en una firma de función cuando la función usa alguna función de esa clase de tipo? Ejemplo:

f :: (Eq a) => a -> a -> Bool
f a b = a == b

Por qué poner (Eq a) en la firma. Si == no está definido para a entonces ¿por qué no lanzar el error cuando se encuentra con a == b ? ¿Cuál es el punto de tener que declarar la clase de tipo adelante?

2) ¿Cómo se relacionan las clases de tipos y la sobrecarga de funciones?

No es posible hacer esto:

data A = A
data B = B

f :: A -> A
f a = a

f :: B -> B
f b = b

Pero es posible hacer esto:

data A = A
data B = B

class F a where
  f :: a -> a

instance F A where
  f a = a

instance F B where
  f b = b

¿Qué pasa con eso? ¿Por qué no puedo tener dos funciones con el mismo nombre pero que operen en diferentes tipos? Viniendo de C ++, me parece muy extraño. Pero probablemente tengo conceptos erróneos acerca de lo que realmente son estas cosas. Pero una vez que los envuelvo en estos tipos de instancia de clase de tipo puedo.

Siéntase libre de lanzarme categorías o tipos de palabras teóricas también, ya que estoy aprendiendo sobre estos temas en paralelo al aprendizaje de Haskell y sospecho que hay una base teórica en esto para que Haskell haga las cosas aquí.

Answer 1

En resumen: porque así fue como se diseñó Haskell .

Por qué poner (Eq a) en la firma. Si == no está definido para a, entonces ¿por qué no lanzar el error cuando se encuentra con a == b ?

¿Por qué ponemos los tipos en la firma de un programa de C ++ (y no solo en algún lugar como una afirmación en el cuerpo)? Porque así es como está diseñado C ++. Normalmente, un concepto sobre qué lenguajes de programación se construyen es " hacer explícito lo que debe ser explícito ".

No se dice que un módulo de Haskell sea de código abierto. Eso significa que solo tenemos la firma disponible. Esto significaría que cuando, por ejemplo, escribamos:

Prelude> foo A A

<interactive>:4:1: error:
    • No instance for (Eq A) arising from a use of ‘foo’
    • In the expression: foo A A
      In an equation for ‘it’: it = foo A A

Frecuentemente escribiríamos foo aquí con tipos que no tienen clase de clase Eq . Como resultado, obtendríamos muchos errores que solo se descubren en tiempo de compilación (o si Haskell era un lenguaje dinámico, en tiempo de ejecución). La idea de poner Eq a en la firma de tipo es que podemos buscar la firma de foo por adelantado, y así asegurarnos de que los tipos sean una instancia de la clase de tipos.

Tenga en cuenta que no tiene que escribir firmas de tipo usted mismo: Haskell normalmente puede obtener la firma de una función, pero una firma debe incluir toda la información necesaria para llamar y usar una función de manera efectiva. Al agregar restricciones de tipo, aceleramos el desarrollo.

¿Qué pasa con eso? ¿Por qué no puedo tener dos funciones con el mismo nombre pero operando en diferentes tipos?

De nuevo: así es como está diseñado Haskell. Las funciones en los lenguajes de programación funcionales son " ciudadanos de primera clase ". Significa que estos usualmente tienen un nombre y queremos evitar los choques de nombres tanto como sea posible. Al igual que las clases en C ++, normalmente tienen un nombre único (excepto los espacios de nombres).

Digamos que definirías dos funciones diferentes:

incr :: Int -> Int
incr = (+1)

incr :: Bool -> Bool
incr _ = True

bar = incr

Entonces, ¿qué bar tendría que seleccionar? Por supuesto, podemos hacer que los tipos sean explícitos (es decir, incr :: Bool -> Bool ), pero generalmente queremos evitar ese trabajo, ya que introduce mucho ruido.

Otra buena razón por la que no lo hacemos, es porque normalmente una clase de tipos no es solo una colección de funciones: agrega contratos a estas funciones. Por ejemplo, la clase de clase Monad tiene que satisfacer ciertas relaciones entre las funciones. Por ejemplo (>>= return) debe ser equivalente con id . En otras palabras, la clase de tipos:

class Monad m where
    (>>=) :: m a -> (a -> m b) -> m b
    return :: a -> m a

No describe dos funciones independientes (>>=) y return : este es un conjunto de funciones. Los tiene ambos (generalmente con algunos contratos entre el >>= y return específico), o ninguno de estos en absoluto.

Answer 2

Esto solo responde a la pregunta 1 (directamente, al menos).

La firma de tipo f :: a -> a -> Bool es una abreviatura de f :: forall a. a -> a -> Bool f :: forall a. a -> a -> Bool . f no funcionaría realmente para todos los tipos a si solo funcionara para los s que tienen (==) definido. Esta restricción a los tipos que tienen (==) se expresa utilizando la restricción (Eq a) en f :: forall a. (Eq a) => a -> a -> Bool f :: forall a. (Eq a) => a -> a -> Bool .

"Para todos" / la cuantificación universal está en el núcleo del polimorfismo (paramétrico) de Haskell y, entre otras cosas, proporciona las propiedades poderosas e importantes de la parametricity .

Answer 3

Estoy de acuerdo con gran parte de la respuesta de Willem Van Onsem , pero creo que pasa por alto una de las principales ventajas de las clases de tipos sobre la sobrecarga verdaderamente ad hoc: la abstracción . Imagine que utilizamos una sobrecarga ad-hoc en lugar de clases de tipos para definir las operaciones de Monad:

-- Maybe
pure :: a -> Maybe a
pure = Just

(>>=) :: Maybe a -> (a -> Maybe b) -> Maybe b
Just x >>= f = f x
Nothing >>= _ = Nothing

-- Either
pure :: a -> Either e a
pure = Right

(>>=) :: Either e a -> (a -> Either e b) -> Either e b
Right x >>= f = f x
Left err >>= _ = Left err

Ahora, sabemos que cada mónada se puede expresar en términos de pure y >>= , como se fmap anteriormente, pero también sabemos que se pueden expresar de manera equivalente mediante fmap , pure y join . Por lo tanto, deberíamos poder implementar una función de join que funcione en cualquier mónada:

join x = x >>= id

Sin embargo, ahora tenemos un problema. ¿Cuál es el tipo de join ?

Claramente, join tiene que ser polimórfico, ya que funciona en cualquier mónada por diseño. Pero dándole la firma tipo para todos forall m a. m (ma) -> ma forall m a. m (ma) -> ma obviamente estaría mal, ya que no funciona para todos los tipos, solo los monádicos. Por lo tanto, necesitamos algo en nuestro tipo que exprese la necesidad de la existencia de alguna operación (>>=) :: ma -> (a -> mb) -> mb , que es exactamente lo que proporciona la restricción typeclass.

Teniendo en cuenta esto, queda claro que la sobrecarga ad-hoc hace posible la sobrecarga de nombres, pero es imposible abstraerse sobre esos nombres sobrecargados porque no hay garantía de que las diferentes implementaciones estén relacionadas de ninguna manera. Podría definir mónadas sin clases de tipos, pero luego no podría definir la join , when , a unless , mapM , la sequence y todas las demás cosas agradables que obtiene de forma gratuita cuando define solo dos operaciones.

Por lo tanto, las clases de tipos son necesarias en Haskell para habilitar la reutilización del código y evitar enormes cantidades de duplicación. Pero, ¿podría tener tanto una sobrecarga de estilo de clase de tipos como una sobrecarga de nombres ad hoc, dirigida por el tipo? Sí , y de hecho, Idris lo hace. Pero la inferencia de tipos de Idris es muy diferente de la de Haskell, por lo que es más factible apoyarla que en Haskell por muchas de las razones de la respuesta de Willem.

Answer 4

Haskell sostiene dos axiomas (entre otros):

1. Cada variable es utilizable como una expresión por derecho propio;
2. Cada expresión tiene un tipo que especifica precisamente lo que se le permite hacer con ella.

Si tuvieras

f :: A -> A

y

f :: B -> B

entonces, de acuerdo con los principios adoptados en Haskell, f todavía sería una expresión válida, por sí misma, que aún tendría que tener un solo tipo. Si bien es posible hacerlo utilizando subtipos, se consideró mucho más complicado que la solución de clase de tipo.

Del mismo modo, la necesidad de Eq a en

(==) :: Eq a => a -> a -> Bool

proviene del hecho de que el tipo de == tiene que describir completamente lo que puede hacer con él. Si solo puede llamarlo a ciertos tipos, la firma de tipo debe reflejar eso.