Oprócz wzorca, co jeszcze @ może oznaczać w Haskell?

Obecnie studiuję Haskell i staram się zrozumieć projekt, w którym Haskell wdraża algorytmy kryptograficzne. Po przeczytaniu „ Naucz się Haskella dla wielkiego dobra” w Internecie, zaczynam rozumieć kod z tego projektu. Potem okazało się, że utknąłem na następującym kodzie z symbolem „@”:

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

Tutaj randomMtx jest zdefiniowany w następujący sposób:

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

A PRFKey jest zdefiniowany poniżej:

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

Wszystkie źródła informacji, które mogę znaleźć, mówią, że @ jest wzorem, ale ten fragment kodu najwyraźniej nie jest taki przypadek. Sprawdziłem samouczek online, blogi, a nawet raport językowy Haskell 2010 na https://www.haskell.org/definition/haskell2010.pdf . Po prostu nie ma odpowiedzi na to pytanie.

Więcej fragmentów kodu można znaleźć w tym projekcie również przy użyciu @ w ten sposób:

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

Bardzo doceniam wszelką pomoc w tym zakresie.

Że @n to zaawansowana funkcja współczesnego Haskell, która zwykle nie jest objęta samouczkami takimi jak LYAH, ani nie można znaleźć w Raporcie.

Nazywa się to aplikacją typu i jest rozszerzeniem języka GHC. Aby to zrozumieć, rozważ tę prostą funkcję polimorficzną

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

Intuicyjne wywoływanie dupdziała w następujący sposób:

• rozmówca wybiera typ a
• wywołujący wybiera wartości x uprzednio wybranym typema
• dup następnie odpowiada wartością typu (a,a)

W pewnym sensie dupprzyjmuje dwa argumenty: typ ai wartość x :: a. Jednak GHC jest zwykle w stanie wywnioskować typ a(np. Z xlub z kontekstu, w którym używamy dup), więc zwykle przekazujemy tylko jeden argument dup, mianowicie x. Na przykład mamy

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

Co teraz, jeśli chcemy przekazać ajawnie? W takim przypadku możemy włączyć TypeApplicationsrozszerzenie i napisać

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

Zwróć uwagę na @...argumenty niosące typy (nie wartości). Są to coś, co istnieje tylko w czasie kompilacji - w czasie wykonywania argument nie istnieje.

Dlaczego tego chcemy? Czasami nie ma go w xpobliżu i chcemy zmusić kompilator do wybrania właściwego a. Na przykład

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

Aplikacje typu są często przydatne w połączeniu z niektórymi innymi rozszerzeniami, które sprawiają, że wnioskowanie typu jest niemożliwe dla GHC, takie jak typy niejednoznaczne lub rodziny typów. Nie będę ich omawiać, ale możesz po prostu zrozumieć, że czasami naprawdę potrzebujesz pomocy kompilatorowi, szczególnie gdy używasz zaawansowanych funkcji na poziomie tekstu.

Teraz o twoim konkretnym przypadku. Nie znam wszystkich szczegółów, nie znam biblioteki, ale jest bardzo prawdopodobne, że nreprezentujesz rodzaj wartości liczb naturalnych na poziomie typu . Tutaj nurkujemy w raczej zaawansowanych rozszerzeniach, takich jak wyżej wymienione, a DataKindsmoże GADTsi w niektórych maszynach typowych. Chociaż nie potrafię wyjaśnić wszystkiego, mam nadzieję, że mogę zapewnić podstawowy wgląd. Intuicyjnie,

foo :: forall n . some type using n

przyjmuje za argument @nrodzaj naturalnego czasu kompilacji, który nie jest przekazywany w czasie wykonywania. Zamiast,

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

zajmuje @n(czas kompilacji), wraz z dowodem na ton spełnia Wiązanie C n. Ten ostatni argument jest argumentem wykonawczym, który może ujawnić rzeczywistą wartość n. Rzeczywiście, w twoim przypadku wydaje mi się, że masz coś niejasnego

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

co zasadniczo umożliwia kodowi przeniesienie poziomu typu naturalnego na poziom terminu, zasadniczo uzyskując dostęp do „typu” jako „wartości”. (Nawiasem mówiąc, powyższy typ jest uważany za „dwuznaczny” - naprawdę potrzebujesz@n go ujednoznacznić).

Wreszcie: dlaczego warto przejść n na poziomie typu, jeśli później przekonwertujemy to na poziom terminu? Nie byłoby łatwiej po prostu napisać takie funkcje jak

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

zamiast bardziej uciążliwego

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

Szczera odpowiedź brzmi: tak, byłoby łatwiej. Jednak posiadanie nna poziomie typu pozwala kompilatorowi przeprowadzać więcej kontroli statycznych. Na przykład możesz chcieć, aby typ reprezentował „liczby całkowite modulon ” i pozwolił na ich dodawanie. Mający

data Mod = Mod Int  -- Int modulo some n

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

działa, ale nie ma wyboru, że xiy mają ten sam moduł. Jeśli nie będziemy ostrożni, możemy dodać jabłka i pomarańcze. Zamiast tego moglibyśmy pisać

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)

co jest lepsze, ale nadal pozwala dzwonić, foo 5 x ynawet jeśli nnie jest5 . Niedobrze. Zamiast,

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

zapobiega błędom. Kompilator sprawdza wszystko statycznie. Kod jest trudniejszy w użyciu, tak, ale w pewnym sensie utrudnienie w użyciu jest sednem: chcemy, aby użytkownik nie mógł spróbować dodać czegoś o złym module.

Podsumowując: są to bardzo zaawansowane rozszerzenia. Jeśli jesteś początkujący, musisz powoli robić postępy w kierunku tych technik. Nie zniechęcaj się, jeśli nie możesz ich pojąć po krótkim studiu, zajmuje to trochę czasu. Zrób mały krok po kroku, rozwiąż kilka ćwiczeń dla każdej funkcji, aby zrozumieć jej sens. I zawsze będziesz mieć StackOverflow, gdy utkniesz :-)