Outre as-pattern, que signifie @ à Haskell?

J'étudie actuellement Haskell et j'essaie de comprendre un projet qui utilise Haskell pour implémenter des algorithmes cryptographiques. Après avoir lu Learn You a Haskell for Great Good en ligne, je commence à comprendre le code de ce projet. Ensuite, j'ai constaté que je suis bloqué sur le code suivant avec le symbole "@":

-- | Generate an @n@-dimensional secret key over @rq@.
genKey :: forall rq rnd n . (MonadRandom rnd, Random rq, Reflects n Int)
       => rnd (PRFKey n rq)
genKey = fmap Key $ randomMtx 1 $ value @n

Ici, randomMtx est défini comme suit:

-- | A random matrix having a given number of rows and columns.
randomMtx :: (MonadRandom rnd, Random a) => Int -> Int -> rnd (Matrix a)
randomMtx r c = M.fromList r c <$> replicateM (r*c) getRandom

Et PRFKey est défini ci-dessous:

-- | A PRF secret key of dimension @n@ over ring @a@.
newtype PRFKey n a = Key { key :: Matrix a }

Toutes les sources d'informations que je peux trouver disent que @ est le modèle as, mais ce morceau de code n'est apparemment pas le cas. J'ai vérifié le didacticiel en ligne, les blogs et même le rapport linguistique Haskell 2010 sur https://www.haskell.org/definition/haskell2010.pdf . Il n'y a tout simplement pas de réponse à cette question.

Plus d'extraits de code peuvent être trouvés dans ce projet en utilisant @ de cette manière aussi:

-- | Generate public parameters (\( \mathbf{A}_0 \) and \(
-- \mathbf{A}_1 \)) for @n@-dimensional secret keys over a ring @rq@
-- for gadget indicated by @gad@.
genParams :: forall gad rq rnd n .
            (MonadRandom rnd, Random rq, Reflects n Int, Gadget gad rq)
          => rnd (PRFParams n gad rq)
genParams = let len = length $ gadget @gad @rq
                n   = value @n
            in Params <$> (randomMtx n (n*len)) <*> (randomMtx n (n*len))

J'apprécie profondément toute aide à ce sujet.

C'est @nune fonctionnalité avancée de Haskell moderne, qui n'est généralement pas couverte par des didacticiels comme LYAH, ni le rapport.

C'est ce qu'on appelle une application de type et est une extension de langage GHC. Pour le comprendre, considérons cette simple fonction polymorphe

dup :: forall a . a -> (a, a)
dup x = (x, x)

L'appel intuitif dupfonctionne comme suit:

• l' appelant choisit un type a
• l' appelant choisit une valeur x du type précédemment choisia
• dup répond ensuite avec une valeur de type (a,a)

Dans un sens, dupprend deux arguments: le type aet la valeur x :: a. Cependant, GHC est généralement capable d'inférer le type a(par exemple à xpartir du contexte où nous l'utilisons dup), donc nous ne transmettons généralement qu'un seul argument dup, à savoir x. Par exemple, nous avons

dup True    :: (Bool, Bool)
dup "hello" :: (String, String)
...

Maintenant, que se passe- at- il si nous voulons passer explicitement? Eh bien, dans ce cas, nous pouvons activer l' TypeApplicationsextension et écrire

dup @Bool True      :: (Bool, Bool)
dup @String "hello" :: (String, String)
...

Notez les @...arguments portant des types (pas des valeurs). C'est quelque chose qui existe au moment de la compilation, seulement - au moment de l'exécution, l'argument n'existe pas.

Pourquoi voulons-nous cela? Eh bien, parfois il n'y en a pas xet nous voulons inciter le compilateur à choisir le bon a. Par exemple

dup @Bool   :: Bool -> (Bool, Bool)
dup @String :: String -> (String, String)
...

Les applications de type sont souvent utiles en combinaison avec d'autres extensions qui rendent l'inférence de type impossible pour GHC, comme les types ambigus ou les familles de types. Je n'en discuterai pas, mais vous pouvez simplement comprendre que parfois vous avez vraiment besoin d'aider le compilateur, en particulier lorsque vous utilisez de puissantes fonctionnalités au niveau du type.

Maintenant, à propos de votre cas spécifique. Je n'ai pas tous les détails, je ne connais pas la bibliothèque, mais il est très probable que votre nreprésente une sorte de valeur de nombre naturel au niveau du type . Ici, nous plongons dans des extensions assez avancées, comme celles mentionnées ci-dessus plus DataKinds, peut GADTs- être , et certaines machines de classe. Bien que je ne puisse pas tout expliquer, j'espère pouvoir vous fournir quelques informations de base. Intuitivement,

foo :: forall n . some type using n

prend comme argument @n, une sorte de naturel au moment de la compilation, qui n'est pas transmis au moment de l'exécution. Au lieu,

foo :: forall n . C n => some type using n

prend @n(au moment de la compilation), avec une preuve qui nsatisfait la contrainte C n. Ce dernier est un argument d'exécution, qui peut révéler la valeur réelle de n. En effet, dans votre cas, je suppose que vous avez quelque chose qui ressemble vaguement

value :: forall n . Reflects n Int => Int

ce qui permet essentiellement au code d'apporter le niveau de type naturel au niveau de terme, en accédant essentiellement au "type" en tant que "valeur". (Le type ci-dessus est considéré comme "ambigu", soit dit en passant - vous devez vraiment @nlever l' ambiguïté .)

Enfin: pourquoi devrait-on vouloir passer nau niveau du type si nous convertissons ensuite cela au niveau du terme? Il ne serait pas plus facile d'écrire simplement des fonctions comme

foo :: Int -> ...
foo n ... = ... use n

au lieu du plus lourd

foo :: forall n . Reflects n Int => ...
foo ... = ... use (value @n)

La réponse honnête est: oui, ce serait plus facile. Cependant, avoir nau niveau du type permet au compilateur d'effectuer des vérifications plus statiques. Par exemple, vous voudrez peut-être qu'un type représente "des entiers modulo n" et permette d'en ajouter. Ayant

data Mod = Mod Int  -- Int modulo some n

foo :: Int -> Mod -> Mod -> Mod
foo n (Mod x) (Mod y) = Mod ((x+y) `mod` n)

fonctionne, mais il n'y a pas de vérification xet ysont du même module. Nous pouvons ajouter des pommes et des oranges, si nous ne faisons pas attention. On pourrait plutôt écrire

data Mod n = Mod Int  -- Int modulo n

foo :: Int -> Mod n -> Mod n -> Mod n
foo n (Mod x) (Mod y) = Mod ((x+y) `mod` n)

ce qui est mieux, mais permet toujours d'appeler foo 5 x ymême quand ce nn'est pas le cas 5. Pas bon. Au lieu,

data Mod n = Mod Int  -- Int modulo n

-- a lot of type machinery omitted here

foo :: forall n . SomeConstraint n => Mod n -> Mod n -> Mod n
foo (Mod x) (Mod y) = Mod ((x+y) `mod` (value @n))

empêche les choses de mal tourner. Le compilateur vérifie statiquement tout. Le code est plus difficile à utiliser, oui, mais dans un sens, le rendre plus difficile à utiliser est tout l'intérêt: nous voulons qu'il soit impossible pour l'utilisateur d'essayer d'ajouter quelque chose du mauvais module.

Conclusion: ce sont des extensions très avancées. Si vous êtes débutant, vous devrez progresser lentement vers ces techniques. Ne vous découragez pas si vous ne pouvez pas les saisir après seulement une courte étude, cela prend du temps. Faites un petit pas à la fois, résolvez quelques exercices pour chaque fonctionnalité pour en comprendre l'intérêt. Et vous aurez toujours StackOverflow lorsque vous serez coincé :-)