Haskell Language
Des procurations

Utiliser un proxy

Le type Proxy :: k -> * , trouvé dans Data.Proxy , est utilisé lorsque vous avez besoin de donner des informations de type au compilateur - par exemple, pour choisir une instance de classe de type - qui est néanmoins sans importance à l'exécution.

{-# LANGUAGE PolyKinds #-}

data Proxy a = Proxy

Les fonctions qui utilisent un Proxy utilisent généralement ScopedTypeVariables pour choisir une instance de classe de type basée sur a type.

Par exemple, l'exemple classique d'une fonction ambiguë,

showread :: String -> String
showread = show . read

ce qui se traduit par une erreur de type car le constructeur ne sait pas quelle instance de Show ou de Read à utiliser, peut être résolue avec Proxy :

{-# LANGUAGE ScopedTypeVariables #-}

import Data.Proxy

showread :: forall a. (Show a, Read a) => Proxy a -> String -> String
showread _ = (show :: a -> String) . read

Lorsque vous appelez une fonction avec Proxy , vous devez utiliser une annotation de type pour déclarer celle a vous vouliez dire.

ghci> showread (Proxy :: Proxy Int) "3"
"3"
ghci> showread (Proxy :: Proxy Bool) "'m'"  -- attempt to parse a char literal as a Bool
"*** Exception: Prelude.read: no parse

L'idiome "proxy polymorphe"

Étant donné que le Proxy ne contient aucune information d'exécution, il n'est jamais nécessaire de faire correspondre le modèle au constructeur du Proxy . Un idiome commun consiste donc à faire un résumé sur le type de données Proxy utilisant une variable de type.

showread :: forall proxy a. (Show a, Read a) => proxy a -> String -> String
showread _ = (show :: a -> String) . read

Maintenant, si vous avez une fa dans la portée de certains f , vous n'avez pas besoin d'écrire Proxy :: Proxy a lorsque vous appelez f .

ghci> let chars = "foo"  -- chars :: [Char]
ghci> showread chars "'a'"
"'a'"

Le proxy est comme ()

Comme Proxy ne contient aucune information d'exécution, vous pouvez toujours écrire une transformation naturelle fa -> Proxy a pour tout f .

proxy :: f a -> Proxy a
proxy _ = Proxy

C'est comme si une valeur donnée pouvait toujours être effacée sur () :

unit :: a -> ()
unit _ = ()

Techniquement, Proxy est l'objet terminal dans la catégorie des foncteurs, tout comme () est l'objet terminal dans la catégorie des valeurs.