Além do padrão, o que mais pode @ significar em Haskell?

Atualmente, estou estudando o Haskell e tento entender um projeto que usa o Haskell para implementar algoritmos criptográficos. Depois de ler on - line Aprenda um Haskell para o Bem , comecei a entender o código nesse projeto. Então eu descobri que estou preso no seguinte código com o 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

Aqui o randomMtx é definido da seguinte maneira:

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

E o PRFKey está definido abaixo:

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

Todas as fontes de informação que encontro dizem que @ é o padrão, mas aparentemente esse código não é o caso. Verifiquei o tutorial on-line, os blogs e até o relatório do idioma Haskell 2010 em https://www.haskell.org/definition/haskell2010.pdf . Simplesmente não há resposta para essa pergunta.

Mais trechos de código podem ser encontrados neste projeto usando @ desta maneira também:

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

Agradeço profundamente qualquer ajuda nisso.

Esse @né um recurso avançado do Haskell moderno, que geralmente não é coberto por tutoriais como o LYAH, nem pode ser encontrado no Relatório.

É chamado de aplicativo de tipo e é uma extensão de idioma do GHC. Para entendê-lo, considere esta função polimórfica simples

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

A chamada intuitiva dupfunciona da seguinte maneira:

• o chamador escolhe um tipo a
• o chamador escolhe um valor x do tipo escolhido anteriormentea
• dup então responde com um valor do tipo (a,a)

Em certo sentido, são dupnecessários dois argumentos: o tipo ae o valor x :: a. No entanto, o GHC geralmente é capaz de inferir o tipo a(por exemplo x, de ou do contexto em que estamos usando dup), portanto, geralmente passamos apenas um argumento para dup, a saber x. Por exemplo, temos

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

Agora, e se queremos passar aexplicitamente? Bem, nesse caso, podemos ativar a TypeApplicationsextensão e escrever

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

Observe os @...argumentos que carregam tipos (não valores). Isso é algo que existe apenas no tempo de compilação - no tempo de execução, o argumento não existe.

Por que queremos isso? Bem, às vezes não há por xperto, e queremos estimular o compilador a escolher o certo a. Por exemplo

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

Os aplicativos de tipo geralmente são úteis em combinação com outras extensões que inviabilizam a inferência de tipo para o GHC, como tipos ambíguos ou famílias de tipos. Não vou discutir isso, mas você pode simplesmente entender que, às vezes, você realmente precisa ajudar o compilador, especialmente ao usar recursos avançados de tipo.

Agora, sobre o seu caso específico. Não tenho todos os detalhes, não conheço a biblioteca, mas é muito provável que você nrepresente um tipo de valor de número natural no nível de tipo . Aqui estamos mergulhando em extensões bastante avançadas, como as mencionadas acima DataKinds, talvez GADTs, e algumas máquinas de escrever. Embora eu não possa explicar tudo, espero que eu possa fornecer algumas informações básicas. Intuitivamente,

foo :: forall n . some type using n

toma como argumento @n, um tipo de tempo de compilação natural, que não é passado no tempo de execução. Em vez de,

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

takes @n(tempo de compilação), juntamente com uma prova que nsatisfaça a restrição C n. O último é um argumento de tempo de execução, que pode expor o valor real de n. De fato, no seu caso, acho que você tem algo que se parece vagamente

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

que essencialmente permite que o código traga o nível de tipo natural para o nível de termo, acessando essencialmente o "tipo" como um "valor". (O tipo acima é considerado um "ambíguo", a propósito - você realmente precisa @ndesambiguar.)

Finalmente: por que alguém deveria querer passar nno nível de tipo se depois convertemos isso para o nível de termo? Não seria mais fácil simplesmente escrever funções como

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

em vez do mais pesado

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

A resposta honesta é: sim, seria mais fácil. No entanto, ter nno nível de tipo permite ao compilador executar mais verificações estáticas. Por exemplo, você pode querer um tipo para representar "módulo inteiro n" e permitir a adição deles. Tendo

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, mas não há verificação disso xe ysão do mesmo módulo. Podemos adicionar maçãs e laranjas, se não tomarmos cuidado. Poderíamos escrever

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)

o que é melhor, mas ainda permite ligar foo 5 x ymesmo quando nnão é 5. Não é bom. Em vez de,

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

impede que as coisas dêem errado. O compilador verifica estaticamente tudo. O código é mais difícil de usar, sim, mas de certa forma dificultar o uso é o ponto principal: queremos tornar impossível para o usuário tentar adicionar algo do módulo errado.

Concluindo: estas são extensões muito avançadas. Se você é iniciante, precisará progredir lentamente em direção a essas técnicas. Não desanime se você não conseguir compreendê-los após apenas um breve estudo, isso leva algum tempo. Faça um pequeno passo de cada vez, resolva alguns exercícios para cada recurso para entender o objetivo. E você sempre terá o StackOverflow quando estiver parado :-)