Haskell : signature de fonction

Question

Ce programme se compile sans problème :

bar :: MonadIO m
    => m String
bar = undefined

run2IO :: MonadIO m
       => m String
       -> m String
run2IO foo  = liftIO bar

Quand je change bar a foo (nom de l'argument),

run2IO :: MonadIO m
       => m String
       -> m String
run2IO foo  = liftIO foo

J'ai compris :

Impossible de faire correspondre le type 'm' avec 'IO'. 'm' est une variable de type rigide liée par la signature de type pour run2IO : : MonadIO m => m String -> m String ...

Type attendu : IO String Type réel : m String ...

Pourquoi les deux cas ne sont-ils pas équivalents ?

Answer 1

Rappelez-vous le type de liftIO :

liftIO :: MonadIO m => IO a -> m a

Il est important de noter que le premier argument doit être un élément concret. IO valeur. Cela signifie que lorsque vous avez une expression liftIO x entonces x doit être de type IO a .

Lorsqu'une fonction Haskell est universellement quantifiée (à l'aide d'une fonction implicite ou explicite forall ), cela signifie que le appelant de la fonction choisit par quoi la variable de type est remplacée. À titre d'exemple, considérons la variable id fonction : il a le type a -> a mais lorsque vous évaluez l'expression id True entonces id prend le type Bool -> Bool parce que a est instancié en tant que Bool type.

Maintenant, considérez à nouveau votre premier exemple :

run2IO :: MonadIO m => m Integer -> m Integer
run2IO foo = liftIO bar

El foo est complètement hors de propos ici, donc tout ce qui compte en fait est la liftIO bar expression. Puisque liftIO nécessite son premier argument doit être de type IO a entonces bar doit être de type IO a . Cependant, bar est polymorphe : il a en fait le type MonadIO m => m Integer .

Heureusement, IO a un MonadIO l'instance, donc le bar valeur est instancié en utilisant IO pour devenir IO Integer ce qui est bien, car bar est universellement quantifié, donc son instanciation est choisie par son utilisation.

Maintenant, considérons l'autre situation, dans laquelle liftIO foo est utilisé à la place. Ce site semble comme si c'était la même chose, mais en fait, ce n'est pas du tout le cas : cette fois-ci, les MonadIO m => m Integer La valeur est un argument de la fonction, et non une valeur distincte. La quantification porte sur l'ensemble de la fonction, et non sur la valeur individuelle. Pour comprendre cela de manière plus intuitive, il peut être utile de considérer les éléments suivants id à nouveau, mais cette fois-ci, considérez sa définition :

id :: a -> a
id x = x

Dans ce cas, x ne peut être instancié pour être Bool dans sa définition, car cela signifierait id ne pouvait fonctionner que sur Bool ce qui est évidemment faux. En effet, dans l'implémentation de id , x doit être utilisé de manière totalement générique - il ne peut pas être instancié dans un type spécifique car cela violerait les garanties de paramétrie.

Par conséquent, dans votre run2IO fonction, foo doit être utilisé de manière tout à fait générique comme une MonadIO et non une valeur spécifique MonadIO instance. Le site liftIO l'appel tente d'utiliser l'adresse spécifique IO ce qui n'est pas autorisé, puisque l'appelant peut ne pas fournir d'instance IO valeur.

---

Il est possible, bien sûr, que vous souhaitiez que l'argument de la fonction soit quantifié de la même manière que bar c'est-à-dire que vous pourriez vouloir que son instanciation soit choisie par l'implémentation, et non par l'appelant. Dans ce cas, vous pouvez utiliser la fonction RankNTypes pour spécifier un type différent en utilisant une extension de langage explicite. forall :

{-# LANGUAGE RankNTypes #-}

run3IO :: MonadIO m => (forall m1. MonadIO m1 => m1 Integer) -> m Integer
run3IO foo = liftIO foo

Cette fonction permet de vérifier la typologie, mais elle n'est pas très utile.

Answer 2

Dans le premier, vous utilisez liftIO en bar . Cela nécessite en fait bar :: IO String . Maintenant, IO se trouve être (trivialement) une instance sur MonadIO donc cela fonctionne - le compilateur rejette simplement le polymorphisme de bar .

Dans le deuxième cas, le compilateur n'a pas à décider quelle monade particulière utiliser comme type de foo : elle est fixée par l'environnement, c'est-à-dire le appelant peut décider de ce que MonadIO instance qu'il devrait être. Pour avoir à nouveau la liberté de choisir IO comme monade, vous aurez besoin de la signature suivante :

{-# LANGUAGE Rank2Types, UnicodeSyntax #-}

run2IO' :: MonadIO m
       => (∀ m' . MonadIO m' => m' String)
       -> m String
run2IO' foo  = liftIO foo

... mais je ne pense pas que ce soit vraiment ce que vous voulez : vous pourriez alors aussi bien écrire

run2IO' :: MonadIO m => IO String -> m String
run2IO' foo  = liftIO foo

ou simplement run2IO = liftIO .