Además de as-pattern, ¿qué más puede significar @ en Haskell?

Actualmente estoy estudiando Haskell e intento entender un proyecto que utiliza Haskell para implementar algoritmos criptográficos. Después de leer Learn You a Haskell for Great Good en línea, empiezo a comprender el código de ese proyecto. Luego descubrí que estoy atascado en el siguiente código con el símbolo "@":

-- | 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

Aquí el randomMtx se define de la siguiente manera:

-- | 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

Y PRFKey se define a continuación:

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

Todas las fuentes de información que puedo encontrar dicen que @ es el as-patrón, pero este código aparentemente no es ese el caso. He consultado el tutorial en línea, los blogs e incluso el informe del idioma Haskell 2010 en https://www.haskell.org/definition/haskell2010.pdf . Simplemente no hay respuesta a esta pregunta.

Se pueden encontrar más fragmentos de código en este proyecto usando @ de esta manera también:

-- | 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))

Aprecio profundamente cualquier ayuda en esto.

Esa @nes una característica avanzada del Haskell moderno, que generalmente no está cubierto por tutoriales como LYAH, ni se puede encontrar en el Informe.

Se llama una aplicación tipo y es una extensión de lenguaje GHC. Para entenderlo, considere esta simple función polimórfica

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

La llamada intuitiva dupfunciona de la siguiente manera:

• la persona que llama elige un tipo a
• la persona que llama elige un valor x del tipo elegido previamentea
• dup luego responde con un valor de tipo (a,a)

En cierto sentido, duptoma dos argumentos: el tipo ay el valor x :: a. Sin embargo, GHC generalmente puede inferir el tipo a(p. Ej. x, Del contexto en el que lo estamos utilizando dup), por lo que generalmente solo pasamos un argumento dup, a saber x. Por ejemplo, tenemos

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

Ahora, ¿qué pasa si queremos pasar aexplícitamente? Bueno, en ese caso podemos activar la TypeApplicationsextensión y escribir

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

Tenga en cuenta los @...argumentos que llevan tipos (no valores). Esos son algo que existe en tiempo de compilación, solo, en tiempo de ejecución el argumento no existe.

¿Por qué queremos eso? Bueno, a veces no hay nada x, y queremos presionar al compilador para que elija el correcto a. P.ej

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

Las aplicaciones de tipo a menudo son útiles en combinación con algunas otras extensiones que hacen inferencia de tipo inviable para GHC, como los tipos ambiguos o las familias de tipos. No hablaré de eso, pero puedes entender que a veces realmente necesitas ayudar al compilador, especialmente cuando utilizas potentes funciones de nivel de tipo.

Ahora, sobre su caso específico. No tengo todos los detalles, no conozco la biblioteca, pero es muy probable que nrepresente una especie de valor de número natural a nivel de tipo . Aquí nos estamos sumergiendo en extensiones bastante avanzadas, como las mencionadas anteriormente, más DataKinds, tal vez GADTs, y algunas máquinas de tipo. Si bien no puedo explicar todo, espero poder proporcionar una idea básica. Intuitivamente

foo :: forall n . some type using n

toma como argumento @nun tipo de tiempo de compilación natural, que no se pasa en tiempo de ejecución. En lugar,

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

toma @n(tiempo de compilación), junto con una prueba que nsatisface la restricción C n. Este último es un argumento en tiempo de ejecución, que podría exponer el valor real de n. De hecho, en su caso, supongo que tiene algo vagamente parecido

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

que esencialmente permite que el código traiga el nivel de tipo natural al nivel de término, esencialmente accediendo al "tipo" como un "valor". (El tipo anterior se considera "ambiguo", por cierto, realmente necesita @ndesambiguar).

Finalmente: ¿por qué debería uno querer pasar nal nivel de tipo si luego lo convertimos al nivel de término? No sería más fácil simplemente escribir funciones como

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

en lugar de los más engorrosos

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

La respuesta honesta es: sí, sería más fácil. Sin embargo, tener nel nivel de tipo permite al compilador realizar más comprobaciones estáticas. Por ejemplo, es posible que desee que un tipo represente "módulo de enteros n" y permita agregarlos. Teniendo

data Mod = Mod Int  -- Int modulo some n

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

funciona, pero no hay verificación de eso xy yson del mismo módulo. Podríamos agregar manzanas y naranjas, si no tenemos cuidado. En su lugar podríamos escribir

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)

lo cual es mejor, pero aún permite llamar foo 5 x yincluso cuando nno lo es 5. No está bien. En lugar,

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))

evita que las cosas salgan mal. El compilador comprueba estáticamente todo. El código es más difícil de usar, sí, pero en cierto sentido hacer que sea más difícil de usar es el punto: queremos hacer imposible que el usuario intente agregar algo del módulo incorrecto.

Conclusión: estas son extensiones muy avanzadas. Si eres un principiante, deberás progresar lentamente hacia estas técnicas. No se desanime si no puede comprenderlos después de un breve estudio, lleva algún tiempo. Haga un pequeño paso a la vez, resuelva algunos ejercicios para cada característica para comprender el punto. Y siempre tendrá StackOverflow cuando esté atascado :-)