В настоящее время я изучаю Haskell и пытаюсь понять проект, который использует Haskell для реализации криптографических алгоритмов. После того, как я прочел в Интернете « Изучаю тебя на гаскелле для хорошего блага» , я начал понимать код этого проекта. Затем я обнаружил, что застрял в следующем коде с символом «@»:
-- | 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))
Я глубоко признателен за любую помощь в этом.
источник
Ответы:
Это
@n
расширенная функция современного Haskell, которая обычно не рассматривается в таких учебных пособиях, как LYAH, и не может быть найдена в Отчете.Он называется приложением типа и является расширением языка GHC. Чтобы понять это, рассмотрим эту простую полиморфную функцию
Интуитивно понятный вызов
dup
работает следующим образом:a
x
из ранее выбранного типаa
dup
затем отвечает со значением типа(a,a)
В некотором смысле,
dup
принимает два аргумента: типa
и значениеx :: a
. Однако GHC обычно может выводить типa
(напримерx
, из контекста или из контекста, в котором мы используемdup
), поэтому мы обычно передаем только один аргументdup
, а именноx
. Например, у нас естьА что если мы хотим передать
a
явно? Ну, в этом случае мы можем включитьTypeApplications
расширение и написатьОбратите внимание на
@...
аргументы, несущие типы (не значения). Это то, что существует только во время компиляции - во время выполнения аргумент не существует.Почему мы этого хотим? Ну, иногда
x
вокруг нет , и мы хотим подтолкнуть компилятор к правильному выборуa
. НапримерПриложения типов часто полезны в сочетании с некоторыми другими расширениями, которые делают вывод типов невозможным для GHC, например, неоднозначные типы или семейства типов. Я не буду обсуждать это, но вы можете просто понять, что иногда вам действительно нужно помочь компилятору, особенно при использовании мощных функций уровня типа.
Теперь о вашем конкретном случае. У меня нет всех деталей, я не знаю библиотеку, но очень вероятно, что ваш
n
представляет собой некое значение натурального числа на уровне типа . Здесь мы погружаемся в довольно продвинутые расширения, такие как вышеупомянутые, плюсDataKinds
, может бытьGADTs
, и некоторые механизмы класса типов. Хотя я не могу все объяснить, надеюсь, я смогу дать некоторые основные идеи. Наглядно,принимает в качестве аргумента
@n
своего рода естественное время компиляции, которое не передается во время выполнения. Вместо,берет
@n
(время компиляции) вместе с доказательством, котороеn
удовлетворяет ограничениюC n
. Последний является аргументом времени выполнения, который может представлять фактическое значениеn
. Действительно, в вашем случае, я думаю, у вас есть что-то смутно похожеекоторый, по сути, позволяет коду привести естественный уровень типа к уровню терминов, по сути, получая доступ к «типу» как «значению». (Кстати, вышеприведенный тип считается «неоднозначным» - вам действительно необходимо
@n
устранить неоднозначность.)И наконец: зачем нужно переходить
n
на уровень типа, если мы потом позже преобразуем его в термин «уровень»? Не было бы проще просто написать такие функции, каквместо более громоздкого
Честный ответ: да, было бы проще. Однако наличие
n
на уровне типа позволяет компилятору выполнять больше статических проверок. Например, вы можете захотеть, чтобы тип представлял «целые числа по модулюn
» и разрешал добавлять их. имеющийработает, но нет проверки, что
x
иy
имеют одинаковый модуль. Мы можем добавить яблоки и апельсины, если не будем осторожны. Мы могли бы вместо этого написатьчто лучше, но все же позволяет звонить,
foo 5 x y
даже когдаn
нет5
. Фигово. Вместо,мешает что-то пойти не так Компилятор статически все проверяет. Код труднее использовать, да, но в некотором смысле усложнить его использование - вот в чем суть: мы хотим сделать невозможным для пользователя попытку добавить что-то с неправильным модулем.
Заключение: это очень продвинутые расширения. Если вы новичок, вам нужно будет постепенно продвигаться к этим методам. Не расстраивайтесь, если вы не можете понять их только после небольшого изучения, это займет некоторое время. Сделайте небольшой шаг за раз, решите несколько упражнений для каждой функции, чтобы понять ее смысл. И у вас всегда будет StackOverflow, когда вы застряли :-)
источник