Soy relativamente nuevo en Haskell, así que perdóname si esto es realmente obvio.

Básicamente tengo dos Booly en base a ellos quiero elegir la implementación de 3 funciones diferentes. En el caso de que ambos bools sean iguales (por ejemplo, ambos True o ambos False), las funciones no deberían hacer nada. Luego hay una implementación diferente si uno u otro Bool es True.

Estas funciones implican restricciones, por lo que, por ejemplo, la primera función tiene una restricción Ord o Bounded en los parámetros. La segunda función tiene una restricción Num sobre los parámetros.

El problema que tengo es que no tengo ni idea de cómo hacer que el verificador de tipos esté bien con esta construcción. Vea a continuación un ejemplo mínimo que se queja cuando coincido con el patrón en el resultado:

f :: (Ord a, Bounded a) => a -> a -> a
f a b = if a > b then maxBound else minBound

g :: (Ord a, Bounded a) => a -> a -> a
g a b = if a > b then minBound else maxBound

a = True
b = False

test
  | a == b = (const, const, const)
  | a      = (f, (-), (+))
  | b      = (g, (+), (-))

(resF, _, _) = test

(_, resG, _) = test -- error  Could not deduce (Ord b0) arising from a use of ‘test’
                    -- from the context: Num b
                    -- Same error occurs for the last value in the tuple.

No estoy seguro de cómo la función con la mayoría de las restricciones resFestá completamente bien al ser asignada a una variable, pero se resGqueja ...

¡Se agradece cualquier ayuda!

El problema aquí es que tienes un tipo ambiguo . En primer lugar, verifiquemos la firma de tipo de testsegún lo inferido por GHC. Un buen truco que descubrí hace un tiempo es agregarlo test :: _a su programa y dejar que GHC nos dé su tipo inferido en un mensaje de error:

so.hs:13:9: error:
    • Found type wildcard ‘_’
        standing for ‘(b0 -> b0 -> b0, Integer -> Integer -> Integer,
                       Integer -> Integer -> Integer)’
      Where: ‘b0’ is an ambiguous type variable
      To use the inferred type, enable PartialTypeSignatures
    • In the type signature: test :: _
   |
13 | test :: _
   |         ^

Entonces, el tipo de testsegún lo inferido por GHC es (b0 -> b0 -> b0, Integer -> Integer -> Integer, Integer -> Integer -> Integer)(aunque debería haber una (Ord b0, Bounded b0)restricción adicional que GHC omite por alguna razón). Ahora, veamos resFy resG:

(resF, _, _) = test
(_, resG, _) = test

En la definición de resF, el b0parámetro de tipo termina usándose también fuera de esa expresión (en el tipo de resF :: b0 -> b0 -> b0), por lo que no es ambiguo. Sin embargo, en la definición de resG, b0solo se usa dentro de esa expresión, ¡así que podría ser cualquier cosa ! Dado que GHC no tiene absolutamente ninguna forma de determinar qué b0hay en esa declaración, se marca como ambigua, produciendo este error.

(Si eso no fue lo suficientemente claro, la idea es que si tiene una expresión con una variable de tipo ambiguo, y se refiere a esta variable en el lado izquierdo del =, entonces se desambigua, ya que la variable se está utilizando fuera del expresión. Sé que esta no es una explicación muy buena; no soy muy bueno con esta área de Haskell, así que si alguien más tiene una explicación mejor, ¡comenten!)

Entonces, ¿cómo se puede resolver este problema? Una forma es simplemente combinar resFy resG, por b0lo tanto , termina usándose en el exterior test:

(resF, resG, _) = test

Otra forma es agregar una firma de tipo que restrinja b0 :

(_, resG, _) = test :: (() -> () -> (), Integer -> Integer -> Integer, Integer -> Integer -> Integer)

Esta es la forma más común de sortear errores de tipo ambiguo, ya que funcionará en todas las circunstancias. En este caso, resulta ser mucho más largo, pero debería poder usarlo en más situaciones que la técnica anterior, que realmente solo funciona aquí.

Sin embargo, todavía hay algunos puntos sutiles aquí. En primer lugar, ¿por qué GHC informa que el segundo y tercer campo utilizan Integer, en lugar de permitir cualquier tipo? Esto se debe a la restricción de monomorfismo , que en determinadas situaciones especializa las variables de tipo automáticamente. Puede evitar esto agregando una firma de tipo:

test :: (Ord a, Bounded a, Num b, Num c) => (a -> a -> a, b -> b -> b, c -> c -> c)

¡Es por eso que se considera una buena práctica agregar firmas de tipo a todas las funciones!

Por supuesto, esto tiene la desventaja de hacer que el segundo y tercer campo también utilicen variables de tipo; por lo tanto, también se vuelven propensos a tipos ambiguos. Puede evitar esto vinculando los tres campos para permitir que estas variables de tipo se 'propaguen' en un sentido fuera de esa declaración:

(resF, resG, resH) = test

(Tenga en cuenta que 'propagar' es mi propio término, ¡no un término reconocido por Haskell!)

EDITAR: Entonces, resulta que esta estrategia no funciona. Se dan más detalles al final de esta respuesta, ya que es un poco detallada.

O puede agregar una firma de tipo nuevamente para restringir by c:

(resF, _, _) = test :: (Ord a, Bounded a) => (a -> a -> a, Int -> Int -> Int, Int -> Int -> Int)

El otro punto que quería hacer es con la definición de testsí mismo. En Haskell, es muy poco común usar variables globales como lo hace aquí; Por lo general, los agregaría como parámetros y testluego los pasaría desde afuera de esta manera:

test :: (Ord a, Bounded a, Num b, Num c)
     => Bool
     -> Bool
     -> (a -> a -> a, b -> b -> b, c -> c -> c)
test a b =
  | a == b = (const, const, const)
  | a      = (f, (-), (+))
  | b      = (g, (+), (-))

(resF, resG, resH) = test True False

Hacerlo de esta manera permite una mayor reutilización del código, ya testque ahora se puede usar varias veces con diferentes condiciones booleanas.

EDITAR:

Limitaciones de las tuplas polimórficas

No estoy seguro de que lo anterior sea incorrecto como tal, pero hay un factor importante que me perdí por completo. Si tiene algo de tipo (Constr1 a, Constr2 b) => (a, b), toda la tupla depende de ambos Constr1 a y Constr2 b ! Por lo tanto, no puede eliminar fácilmente una variable de tipo para aislar la otra. (Más detalles en esta excelente respuesta).

Sin embargo, ¡hay una solución! En test, cada campo es independiente entre sí. Por lo tanto, teóricamente debería ser posible cambiar el tipo al siguiente signo:

test :: Bool -> Bool
     -> ( forall a. (Ord a, Bouded a) => a -> a -> a
        , forall b. Num b => b -> b -> b
        , forall c. Num c => c -> c -> c
        )
test a b =
  | a == b = (const, const, const)
  | a      = (f, (-), (+))
  | b      = (g, (+), (-))

Ahora, en cierto sentido, todas las restricciones se han "introducido" en la tupla, por lo que ahora puede aislar un campo.

Por supuesto, nada es tan simple como eso, y si intenta ejecutar lo anterior, se encontrará con un error sobre 'polimorfismo impredicativo'. Las soluciones envuelven los campos en tipos de datos auxiliares:

newtype Wrapper1 = Wrapper1 (forall a. (Ord a, Bounded a) => a -> a -> a)
newtype Wrapper2 = Wrapper2 (forall b. Num b => b -> b -> b)

test :: (Wrapper1, Wrapper2, Wrapper2)
test
  | a == b = (Wrapper1 const, Wrapper2 const, Wrapper2 const)
  | a      = (Wrapper1 f    , Wrapper2 (-)  , Wrapper2 (+))
  | b      = (Wrapper1 g    , Wrapper2 (+)  , Wrapper2 (-))

(Wrapper1 resF, Wrapper2 resG, Wrapper2 resH) = test

(También deberá agregar {-# LANGUAGE RankNTypes #-}al principio del archivo para que esto se compile).

Y esto, ¡finalmente! - escribe correctamente.

Como ventaja adicional, resulta que este método incluso elimina los errores de tipo ambiguos. El siguiente tipo de código también se comprueba correctamente:

test
  | a == b = (Wrapper1 const, Wrapper2 const, Wrapper2 const)
  | a      = (Wrapper1 f    , Wrapper2 (-)  , Wrapper2 (+))
  | b      = (Wrapper1 g    , Wrapper2 (+)  , Wrapper2 (-))

(Wrapper1 resF, _, _) = test

Como mencioné anteriormente, no entiendo muy bien los tipos ambiguos, pero la razón de esto es probablemente porque toda la información sobre otras variables de tipo ha sido 'extraída' de los otros campos de la tupla, por lo que GHC sabe que puede ignorarla de manera segura. ellos ahora.

TL; Versión DR: porque GHC estará predeterminado Num b2y Num b3no (Ord b1, Bounded b1).

Este es un problema con el tipo predeterminado . Se testinfiere que el tipo de (Ord b1, Bounded b1, Num b2, Num b3) => (b1 -> b1 -> b1, b2 -> b2 -> b2, b3 -> b3 -> b3). Este tipo significa que si proporciona una instancia Ordy Boundedpara algún tipo b1, y una Numinstancia para algunos tipos b2y b3, obtendrá una tupla de funciones. Cuando separas la tupla y solo mantienes una pieza, las otras restricciones no desaparecen, por lo que básicamente tienes resF :: (Ord b1, Bounded b1, Num b2, Num b3) => b1 -> b1 -> b1y resG :: (Ord b1, Bounded b1, Num b2, Num b3) => b2 -> b2 -> b2.

Ahora, en resF, b2y b3son tipos ambiguos, ya que se usan a la izquierda =>pero no a la derecha. De acuerdo con las reglas de tipo predeterminado, estas serán predeterminadas Integer, por lo que terminará resFteniendo realmente un tipo de (Ord b1, Bounded b1) => b1 -> b1 -> b1y las cosas funcionarán bien.

resGes diferente. En él, b1y b3están los tipos ambiguos. b3se establece de forma predeterminada Integercomo lo hizo para resF. Sin embargo, GHC no tiene un valor predeterminado b1que satisfaga la restricción (Ord b1, Bounded b1), por lo que le da un error en ese sentido (que definitivamente podría ser más claro).

Para solucionar el problema, debe indicarle a GHC qué tipo b1sería. Dado que la parte de la tupla que estás guardando no se usa b1, puedes elegir lo que quieras y no importará. Aquí hay una forma de hacerlo (en este ejemplo, elegí Int):

(_, resG, _) = test :: (Num b2, Num b3) => (Int -> Int -> Int, b2 -> b2 -> b2, b3 -> b3 -> b3)

Una forma en que el error dice que no puede deducir de qué tipo aporque es ambiguo el tipo de la clase de tipos Numen las funciones (+)y (-), para resolver este problema, debe especificar cuál, ni la instancia de Ord, Boundedni la instancia de Num:

f :: (Ord a, Bounded a) => a -> a -> a
f a b = if a > b then maxBound else minBound

g :: (Ord a, Bounded a) => a -> a -> a
g a b = if a > b then minBound else maxBound

b1 = True
b2 = False


test a b | a == b = (const, const, const)
         | a      = (f , (-), (+))
         | b      = (g , (+), (-))


(resF, resG , plusH)  = test b1 b2 

three = 3 :: Int
two   = 2 :: Int 
one   = 1 :: Int
main = do
  putStrLn $ "Max: " ++ show (resF three two) putStrLn $ "Min: " ++ show (resF one two)
  putStrLn $ "2 - 1: " ++ show (resG two one) putStrLn $ "1 + 2: " ++ show (plusH one two)

λ> Max: 9223372036854775807
λ> Min: -9223372036854775808
λ> 2 - 1: 1
λ> 1 + 2: 3

Hasta ahora, todo bien, lo arreglé dando los tipos a las funciones resF, resG , plusHcon los números escritos three, two, one:: Int, incluso tú puedes hacer:

(resF, _ , _)  = test b1 b2 

Y también funcionará bien.

Ahora el problema es cuando lo haces:

(_, resG', _)    = test b1 b2

----- ^ ^ ----- (¡¡¡Problema !!!) Con el main, el resG'funcionará bien, porque está escrito por three, two, onevalores Int, ¡pero los _valores no están escritos! tres = 3 :: Int dos = 2 :: Int uno = 1 :: Int main = do putStrLn $ "2 - 1:" ++ mostrar (resG 'dos ​​uno)

¿Cuál es el tipo de _allí? y el otro _, no están especificados, y ese es el principal problema que tienes

Entonces, una solución alternativa es la siguiente:

test a b | a == b = (const, const, const)
         | a      = (f , (-), (+))
         | b      = (g , (+), (-))


type NoneTypedFunction = () -> () -> () -- this type is in case you don't actually want / need the function from the first ternary value

(resF, resG , resH) = test b1 b2 
(_, resG', _)       = test b1 b2 :: (NoneTypedFunction, Int -> Int -> Int, Int -> Int -> Int) 
(_, _, _)           = test b1 b1 :: (NoneTypedFunction, Int -> Int -> Int, Int -> Int -> Int) 


three = 3 :: Int
two   = 2 :: Int 
one   = 1 :: Int
main = do
  putStrLn $ "Max: " ++ show (resF three two)
  putStrLn $ "Min: " ++ show (resF one two) putStrLn $ "2 - 1: " ++ show (resG two one)
  putStrLn $ "2 - 1: " ++ show (resH two one) putStrLn $ "2 - 1: " ++ show (resG' two one)

Ahora le das el tipo correcto a cada uno

otra cosa importante

:t resF
resF :: Int -> Int -> Int

:t resG
resG :: Int -> Int -> Int

resG :: Int -> Int -> Int
:t resH

Los tipos en las funciones, después de la llamada testy dando una hora específica por primera vez, son fijos y ya no polimórficos.

Si quieres ser ilimitado:

first (a, _,  _)  = a
second (_, b, _   = b
third (a, b, c)   = c

y luego puedes hacer:

(first (test b1 b2)) one two

$> -9223372036854775808 (first (test b1 b2)) True False $> True

(first (test b1 b2)) 'c' 'b'
$> '\1114111'