Besides as-pattern, what else can @ mean in Haskell?

Question

I am studying Haskell currently and try to understand a project that uses Haskell to implement cryptographic algorithms. After reading Learn You a Haskell for Great Good online, I begin to understand the code in that project. Then I found I am stuck at the following code with the "@" symbol:

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

Here the randomMtx is defined as follows:

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

And PRFKey is defined below:

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

All information sources I can find say that @ is the as-pattern, but this piece of code is apparently not that case. I have checked the online tutorial, blogs and even the Haskell 2010 language report at https://www.haskell.org/definition/haskell2010.pdf. There is simply no answer to this question.

More code snippets can be found in this project using @ in this way too:

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

I deeply appreciate any help on this.

Answer 1

That @n is an advanced feature of modern Haskell, which is usually not covered by tutorials like LYAH, nor can be found the the Report.

It's called a type application and is a GHC language extension. To understand it, consider this simple polymorphic function

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

Intuitively calling dup works as follows:

• the caller chooses a type a
• the caller chooses a value x of the previously chosen type a
• dup then answers with a value of type (a,a)

In a sense, dup takes two arguments: the type a and the value x :: a. However, GHC is usually able to infer the type a (e.g. from x, or from the context where we are using dup), so we usually pass only one argument to dup, namely x. For instance, we have

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

Now, what if we want to pass a explicitly? Well, in that case we can turn on the TypeApplications extension, and write

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

Note the @... arguments carrying types (not values). Those are something that exists at compile time, only -- at runtime the argument does not exist.

Why do we want that? Well, sometimes there is no x around, and we want to prod the compiler to choose the right a. E.g.

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

Type applications are often useful in combination with some other extensions which make type inference unfeasible for GHC, like ambiguous types or type families. I won't discuss those, but you can simply understand that sometimes you really need to help the compiler, especially when using powerful type-level features.

Now, about your specific case. I don't have all the details, I don't know the library, but it's very likely that your n represents a kind of natural-number value at the type level. Here we are diving in rather advanced extensions, like the above-mentioned ones plus DataKinds, maybe GADTs, and some typeclass machinery. While I can't explain everything, hopefully I can provide some basic insight. Intuitively,

foo :: forall n . some type using n

takes as argument @n, a kind-of compile-time natural, which is not passed at runtime. Instead,

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

takes @n (compile-time), together with a proof that n satisfies constraint C n. The latter is a run-time argument, which might expose the actual value of n. Indeed, in your case, I guess you have something vaguely resembling

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

which essentially allows the code to bring the type-level natural to the term-level, essentially accessing the "type" as a "value". (The above type is considered an "ambiguous" one, by the way -- you really need @n to disambiguate.)

Finally: why should one want to pass n at the type level if we then later on convert that to the term level? Wouldn't be easier to simply write out functions like

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

instead of the more cumbersome

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

The honest answer is: yes, it would be easier. However, having n at the type level allows the compiler to perform more static checks. For instance, you might want a type to represent "integers modulo n", and allow adding those. Having

data Mod = Mod Int  -- Int modulo some n

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

works, but there is no check that x and y are of the same modulus. We might add apples and oranges, if we are not careful. We could instead write

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)

which is better, but still allows to call foo 5 x y even when n is not 5. Not good. Instead,

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

prevents things to go wrong. The compiler statically checks everything. The code is harder to use, yes, but in a sense making it harder to use is the whole point: we want to make it impossible for the user to try adding something of the wrong modulus.

Concluding: these are very advanced extensions. If you're a beginner, you will need to slowly progress towards these techniques. Don't be discouraged if you can't grasp them after only a short study, it does take some time. Make a small step at a time, solve some exercises for each feature to understand the point of it. And you'll always have StackOverflow when you are stuck :-)