haskell - ne pas comprendre pourquoi cet exemple de type associé nécessite plus d'inférence
-
29-10-2019 - |
Question
Considérez le code suivant,
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 (𝔪 α)
Ensuite, si l'on essaie d'écrire une instance en utilisant la fonction expTypeArg,
instance forall 𝔪. (Monad 𝔪, Monad (A 𝔪)) => MyMonadCls (A 𝔪) where
type ExprTyp (A 𝔪) = MyBaseExpr
var nme init@(expTypArg -> typb) =
return init
le compilateur se plaint
Couldn't match type `ExprTyp 𝔪0' with `MyBaseExpr'
Expected type: ExprTyp (A 𝔪) α
Actual type: ExprTyp 𝔪0 α
Mais, si l'on ajoute des expressions de type étendues,
instance forall 𝔪. (Monad 𝔪, Monad (A 𝔪)) => MyMonadCls (A 𝔪) where
type ExprTyp (A 𝔪) = MyBaseExpr
var nme init@((expTypArg :: MyMonadCls (A 𝔪) =>
ExprTyp (A 𝔪) α ->
(A 𝔪 α)) -> typb) =
return init
alors ça résout très bien.Quel est le problème de résolution de ExprTyp == MyBaseExpr
pour expTypArg
?
modifier
Merci beaucoup, Daniel!Voici un moyen de supprimer une partie du verbage, après avoir remarqué que seul le type de 𝔪
doit être appliqué.
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
La solution
ExprTyp n'est pas (nécessairement) une fonction de type injectif.Cela signifie que recevoir quelque chose du type ExprType m
ne définit pas m
- il peut également y avoir un n
différent tel que ExprType n = ExprType m
.Cela rend le type de expTypArg
un peu délicat: il utilise le polymorphisme de type retour de la même manière, par exemple read
, vous devrez donc donner des annotations de type supplémentaires à son résultat dans les mêmes situations que vous avez à faire avec read
.