functions - syntax record haskell

Dependencias funcionales en Haskell

Question

Estoy tratando de entender las dependencias funcionales, pero no estoy logrando nada por mi cuenta. En el documento "Monad Transformers Step by Step", el autor da estas dos definiciones de clases de tipos:

class (Monad m) => MonadError e m | m -> e where
    throwError :: e -> m a
    catchError :: m a -> (e -> m a) -> m a

class (Monad m) => MonadReader r m | m -> r where
    ask :: m r
    local :: (r -> r) -> m a -> m a

Según entiendo algo del material que encontré en línea, significa que la variable de tipo e está determinada por m . Simplemente no entiendo lo que eso significa. ¿Cómo está determinado? ¿Alguien puede arrojar algo de luz con una teoría mínima al principio, y luego vincular la teoría más pesada?

Gracias

Answer 1

Cuando Haskell está tratando de resolver MonadError em it, de forma predeterminada, explora los parámetros MonadError em buscando juntos cualquier par que tenga una instancia. Esto es especialmente difícil si no tenemos una e en ninguna parte de la firma de tipo fuera de la restricción misma

unitError :: MonadError e m => m ()
unitError = return ()

La dependencia funcional dice que una vez que hemos resuelto m , solo puede haber una e que funcione. Eso permite que compile el fragmento anterior, ya que le asegura a Haskell que hay suficiente información para que tenga un tipo no ambiguo.

Sin la dependencia funcional, Haskell se quejaría de que unitError es ambiguo porque podría ser válido para cualquier tipo e y no tenemos forma de saber qué es ese tipo: la información de alguna manera se ha evaporado en el aire.

Para MonadError la dependencia funcional generalmente significa que la mónada misma está parametrizada por el tipo de error. Por ejemplo, aquí hay una instancia

instance MonadError e (Either e) where
  thowError = Left
  catchError (Left e)  f = f e
  catchError (Right a) _ = Right a

Donde e ~ e y m ~ Either e y vemos que m identifica una única e que puede ser válida.

Las dependencias funcionales son "casi" equivalentes a las familias de tipos también. Tipo Las familias a veces son un poco más fáciles de digerir. Por ejemplo, aquí hay una clase MonadError, estilo TypeFamilies

{-# LANGUAGE TypeFamilies #-}

class MonadError m where
  type Err m
  throwError :: Err m -> m a
  catchError :: m a -> (Err m -> m a) -> m a

instance MonadError (Either e) where
  type Err (Either e) = e
  throwError = Left
  catchError (Left e) f  = f e
  catchError (Right a) _ = Right a

Aquí, Err es una función de tipo que lleva un m a su tipo particular de error e la noción de si hay exactamente una e igual a Err m para cualquier m proviene naturalmente de nuestra comprensión de las funciones.

Answer 2

Cuando tiene una clase de tipo multiparámetro, de forma predeterminada, las variables de tipo se consideran de forma independiente. Entonces cuando el tipo inferencer está tratando de averiguar qué instancia de

class Foo a b

para elegir, tiene que determinar a y b independiente, luego ir a mirar para ver si existe la instancia. Con dependencias funcionales, podemos reducir esta búsqueda. Cuando hacemos algo como

class Foo a b | a -> b

Estamos diciendo "Miren, si determinan lo que es, entonces hay un único b por lo que existe el Foo ab , así que no se molesten en tratar de inferir b , simplemente busquen la instancia y tipeen eso". Esto permite que el tipo inferencer sea mucho más efectivo y ayuda a la inferencia en varios lugares.

Esto es particularmente útil con el polimorfismo de retorno, por ejemplo

class Foo a b c where
  bar :: a -> b -> c

Ahora no hay forma de inferir

  bar (bar "foo" ''c'') 1

Porque no tenemos forma de determinar c . Incluso si solo escribimos una instancia para String y Char , debemos suponer que alguien podría / vendrá y agregará otra instancia más adelante. Sin fundeps tendríamos que especificar el tipo de devolución, que es molesto. Sin embargo, podríamos escribir

class Foo a b c | a b -> c where
  bar :: a -> b -> c

Y ahora es fácil ver que el tipo de retorno de la bar "foo" ''c'' es único y, por lo tanto, deducible.

Answer 3

Significa que el sistema de tipos siempre podrá determinar el tipo ( e o r ) del tipo m .

Hagamos nuestro propio ejemplo:

class KnowsA a b | b -> a where
    known :: b -> a

Siempre debemos poder determinar a desde b

data Example1 = Example1 deriving (Show)

instance KnowsA Int Example1 where
    known = const 1 

El sistema de tipos sabe que para esta instalación, siempre que tenga un Example1 , el tipo de a será Int . ¿Cómo lo sabe? No nos permite tener otra instancia con otro tipo.

Si agregamos

instance KnowsA [Char] Example1 where
    known = const "one"

Recibimos un error:

    Functional dependencies conflict between instance declarations:
      instance KnowsA Int Example1
      instance KnowsA [Char] Example1

Pero podemos agregar otra instancia con un tipo diferente para a si tenemos un tipo diferente para b

data Example2 = Example2 deriving (Show)

instance KnowsA [Char] Example2 where
    known = const "two"

main = do
    print . known $ Example1
    print . known $ Example2

Esto previsiblemente produce

1
"two"