Помимо as-pattern, что еще может означать @ в Haskell?

Question

Я изучаю Haskell в настоящее время и пытаюсь понять проект, который использует Haskell для реализации алгоритмов криптографии c. Прочитав Learn You a 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 }

Все источники информации, которые я могу найти, говорят, что @ является шаблоном as, но этот фрагмент кода явно не тот случай. Я проверил онлайн-учебник, блоги и даже языковой отчет Haskell 2010 на https://www.haskell.org/definition/haskell2010.pdf. На этот вопрос просто нет ответа.

В этом проекте можно найти и другие фрагменты кода, использующие @ и так:

-- | 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, и не может быть найдена в Отчете.

Она называется приложением типа и является расширением языка GH C. Чтобы понять это, рассмотрим эту простую полиморфную c функцию

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

Интуитивно вызываемый dup работает следующим образом:

• вызывающая сторона выбирает тип a
• абонент выбирает значение x ранее выбранного типа a
• * Затем 1028 * отвечает значением типа (a,a)

В некотором смысле dup принимает два аргумента: тип a и значение x :: a. Однако GH C обычно может выводить тип 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)
...

Приложения типов часто полезны в сочетании с некоторыми другими расширениями, которые делают вывод типов невозможным для GH C, такими как неоднозначные типы или семейства типов. Я не буду обсуждать это, но вы можете просто понять, что иногда вам действительно нужно помочь компилятору, особенно при использовании мощных функций уровня типов.

Теперь о вашем конкретном случае c. У меня нет всех деталей, я не знаю библиотеку, но очень вероятно, что ваш 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 на уровне типа позволяет компилятору выполнять больше проверок stati c. Например, вы можете захотеть, чтобы тип представлял «целые числа по модулю 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))

предотвращает неправильное использование go. Компилятор статически все проверяет. Код труднее использовать, да, но в некотором смысле усложнить его использование - вот в чем суть: мы хотим сделать невозможным для пользователя попытку добавить что-то с неправильным модулем.

Заключение: эти очень продвинутые расширения. Если вы новичок, вам нужно будет постепенно продвигаться к этим методам. Не падайте духом, если вы не можете получить их после короткого изучения, это займет некоторое время. Сделайте небольшой шаг за раз, решите несколько упражнений для каждой функции, чтобы понять ее смысл. И у вас всегда будет StackOverflow, когда вы застряли: -)