haskell - 除了模式之外，@在Haskell中还有什么意思？

Question

我目前正在研究Haskell，并尝试了解一个使用Haskell实施密码算法的项目。在在线阅读了《学习Haskell for Great Good》之后，我开始理解该项目中的代码。然后我发现我陷入了以下带有“@”符号的代码:

-- | 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定义如下:

-- | 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定义如下:

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

我可以找到的所有信息源都说@是按格式排列，但是这段代码显然不是这种情况。我在 https://www.haskell.org/definition/haskell2010.pdf上检查了在线教程，博客，甚至查看了Haskell 2010语言报告。这个问题根本没有答案。

也可以通过这种方式使用@在此项目中找到更多代码段:

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

我对此深表感谢。

Answer 1

@n是现代Haskell的高级功能，通常LYAH之类的教程都没有涵盖，也无法在报告中找到。

它称为type application，是GHC语言的扩展。要理解它，请考虑这个简单的多态函数

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

直观地调用 dup的工作方式如下:

call 者选择一种类型a

call 者选择先前选择的类型的值x a

dup然后以(a,a)类型的值回答

从某种意义上说， dup接受两个参数: a类型和值 x :: a。但是，GHC通常能够推断 a类型(例如从 x或从我们使用 dup的上下文中推断出)，因此我们通常仅将一个参数传递给 dup，即 x。例如，我们有

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

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

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

请注意 @...参数带有类型(不是值)。这些只是在编译时存在的-在运行时参数不存在。

我们为什么要那样？好吧，有时候周围没有 x，我们想让编译器选择正确的 a。例如。

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

类型应用程序通常与其他一些扩展结合使用，这些扩展使类型推断对于GHC不可行，例如歧义类型或类型族。我不会讨论这些内容，但是您可以简单地了解到有时确实需要帮助编译器，尤其是在使用强大的类型级功能时。

现在，关于您的具体情况。我没有所有的细节，我也不知道该库，但是您的 n很可能在类型级别代表一种自然数值。在这里，我们正在研究相当高级的扩展，例如上述扩展以及 DataKinds，也许是 GADTs，以及一些类型类机制。虽然我无法解释所有内容，但希望我可以提供一些基本见解。凭直觉

foo :: forall n . some type using n

以 @n作为参数，一种自然的编译时，不会在运行时传递。代替，

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

接受 @n(编译时)，以及 n满足约束 C n的证明。后者是运行时参数，可能会暴露 n的实际值。确实，就您而言，我猜您有些含糊的相似之处

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

这实质上允许代码将类型级别的自然语言带到术语级别，实质上是将“类型”作为“值”进行访问。 (顺便说一下，上述类型被认为是“模棱两可”的—您确实需要 @n来消除歧义。)

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

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

而不是比较麻烦

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

诚实的答案是:是的，这样会更容易。但是，在类型级别使用 n可使编译器执行更多静态检查。例如，您可能想要一种类型来表示“整数 n整数”，并允许添加它们。有

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具有相同的模数。如果我们不小心，我们可能会添加苹果和橙子。我们可以写

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。不好。代替，

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

防止出错。编译器将静态检查所有内容。是的，代码更难使用，但从某种意义上讲，这更难于使用是我们的全部要点:我们希望使用户无法尝试添加错误的模数。

结论:这些是非常高级的扩展。如果您是初学者，则需要慢慢地朝着这些技术发展。如果只经过短暂的学习就不能抓住它们，不要气disc，这会花费一些时间。一次走一小步，为每个功能解决一些练习以了解其要点。当您被卡住时，您将始终拥有StackOverflow :-)