Haskell: sin comprender por qué este ejemplo de tipo asociado necesita más inferencia
-
29-10-2019 - |
Pregunta
Considere el siguiente código,
data MyBaseExpr α where
ConstE :: Show α => α -> MyBaseExpr α
class Monad 𝔪 => MyMonadCls 𝔪 where
type ExprTyp 𝔪 :: * -> *
var :: String -> ExprTyp 𝔪 α -> 𝔪 (ExprTyp 𝔪 α)
expTypArg :: forall 𝔪 α. MyMonadCls 𝔪 => ExprTyp 𝔪 α -> 𝔪 α
expTypArg a = undefined
-- dummy type which will be used as an instance
newtype A 𝔪 α = A (𝔪 α)
Entonces, si uno intenta escribir una instancia utilizando la función ExptyPearg,
instance forall 𝔪. (Monad 𝔪, Monad (A 𝔪)) => MyMonadCls (A 𝔪) where
type ExprTyp (A 𝔪) = MyBaseExpr
var nme init@(expTypArg -> typb) =
return init
El compilador se queja
Couldn't match type `ExprTyp 𝔪0' with `MyBaseExpr'
Expected type: ExprTyp (A 𝔪) α
Actual type: ExprTyp 𝔪0 α
Pero, si uno agrega algunas expresiones de tipo alcance,
instance forall 𝔪. (Monad 𝔪, Monad (A 𝔪)) => MyMonadCls (A 𝔪) where
type ExprTyp (A 𝔪) = MyBaseExpr
var nme init@((expTypArg :: MyMonadCls (A 𝔪) =>
ExprTyp (A 𝔪) α ->
(A 𝔪 α)) -> typb) =
return init
Luego se resuelve bien. ¿Cuál es el problema de resolver? ExprTyp == MyBaseExpr
por expTypArg
?
editar
¡Muchas gracias, Daniel! Aquí hay una manera de sacar parte de la verbage, después de notar que solo el tipo de 𝔪
necesita ser cumplido.
ignore_comp :: 𝔪 α -> 𝔪 β -> 𝔪 β
ignore_comp a b = b
instance forall 𝔪. (Monad 𝔪, Monad (A 𝔪)) => MyMonadCls (A 𝔪) where
type ExprTyp (A 𝔪) = MyBaseExpr
var nme init@(expTypArg -> typb) =
typb `ignore_comp`
return init
Solución
ExpRTyp no es (necesariamente) una función de tipo inyectivo. Esto significa que recibir algo de tipo ExprType m
no se clava m
- También puede haber un diferente n
tal que ExprType n = ExprType m
. Esto hace que el tipo de expTypArg
Un poco complicado: utiliza polimorfismo de tipo de retorno de la misma manera, por ejemplo, read
lo hace, por lo que deberá dar anotaciones de tipo adicional a su resultado en las mismas situaciones que debe ver con read
.