除了 as-pattern，@ 在 Haskell 中还有什么意思? [英] Besides as-pattern, what else can @ mean in Haskell?

问题描述

我目前正在研究 Haskell，并尝试了解一个使用 Haskell 实现加密算法的项目.在线阅读Learn You a Haskell for Great Good 后，我开始理解该项目中的代码.然后我发现我被困在以下带有@"符号的代码中:

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

这里的randomMtx定义如下:

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

而 PRFKey 定义如下:

And PRFKey is defined below:

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

我能找到的所有信息来源都说@是as-pattern，但是这段代码显然不是这种情况.我在 查看了在线教程、博客，甚至Haskell 2010 语言报告https://www.haskell.org/definition/haskell2010.pdf.这个问题根本没有答案.

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.

推荐答案

那个 @n 是现代 Haskell 的一个高级特性，通常像 LYAH 这样的教程没有涵盖，也找不到报告.

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.

它被称为 type application 是一个 GHC 语言扩展.为了理解它，考虑这个简单的多态函数

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)

直观地调用 dup 的工作原理如下:

Intuitively calling dup works as follows:

• 调用者选择一个类型 a
• 调用者选择一个值 x 之前选择的类型a
• dup 然后用 (a,a)
类型的值回答

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

从某种意义上说，dup 有两个参数:类型 a 和值 x :: a.然而，GHC 通常能够推断类型 a(例如从 x，或从我们使用 dup 的上下文)，所以我们通常只传递一个参数给dup，即x.例如，我们有

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

现在，如果我们想显式地传递 a 怎么办?那么，在这种情况下，我们可以打开 TypeApplications 扩展，然后编写

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.

我们为什么要那样?好吧，有时周围没有 x，我们希望促使编译器选择正确的 a.例如

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

类型应用程序通常与其他一些扩展结合使用，这些扩展使 GHC 无法进行类型推断，例如不明确的类型或类型系列.我不会讨论这些，但您可以简单地理解，有时您确实需要帮助编译器，尤其是在使用强大的类型级功能时.

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.

现在，关于您的具体情况.我没有所有的细节，我不知道这个库，但很可能你的 n 代表一种类型级别的自然数值.在这里，我们将深入研究相当高级的扩展，例如上述扩展以及 DataKinds、可能是 GADTs 和一些类型类机制.虽然我不能解释一切，但希望我能提供一些基本的见解.直觉上，

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

作为参数@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

采用@n(编译时)，以及n满足约束C n的证明.后者是一个运行时参数，它可能会暴露 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

本质上允许代码将类型级别自然带入术语级别，本质上将类型"作为值"访问.(顺便说一下，上述类型被认为是歧义"类型——您确实需要 @n 来消除歧义.)

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

最后:如果我们稍后将其转换为术语级别，为什么要在类型级别传递 n ?简单地写出像

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

而不是更麻烦

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

诚实的回答是:是的，这会更容易.但是，在类型级别具有 n 允许编译器执行更多静态检查.例如，您可能想要一个类型来表示整数模 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)

有效，但没有检查 x 和 y 是否具有相同的模数.如果我们不小心的话，我们可能会加苹果和橙子.我们可以改写

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)

哪个更好，但仍然允许调用 foo 5 x y 即使 n 不是 5.不好.相反，

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.

结论:这些是非常高级的扩展.如果您是初学者，则需要慢慢地学习这些技术.如果您在短期学习后仍无法掌握它们，请不要气馁，这确实需要一些时间.一次一小步，为每个功能解决一些练习，以了解它的要点.当你陷入困境时，你总会有 StackOverflow :-)

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

这篇关于除了 as-pattern，@ 在 Haskell 中还有什么意思?的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！