[haskell] 패턴과 더불어 Haskell에서 @은 무엇을 의미할까요?

Program / 글쓴이

현재 Haskell을 연구하고 있으며 Haskell을 사용하여 암호화 알고리즘을 구현하는 프로젝트를 이해하려고합니다. Great Good을위한 Haskell Learn Online 을 읽은 후 해당 프로젝트의 코드를 이해하기 시작합니다. 그런 다음 “@”기호가있는 다음 코드에 붙어 있습니다.

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

나는 이것에 대한 도움을 깊이 감사합니다.

답변

이는 @n현대 하스켈의 고급 기능으로, LYAH와 같은 자습서에서는 다루지 않으며 보고서를 찾을 수 없습니다.

형식 응용 프로그램 이라고하며 GHC 언어 확장입니다. 그것을 이해하려면이 간단한 다형성 함수를 고려하십시오

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

직관적으로 전화 dup하면 다음과 같이 작동합니다.

  • 호출자 선택 유형 a
  • 호출자 선택 값이 x 미리 선택된 유형을a
  • dup 그런 다음 유형의 값으로 답변 (a,a)

어떤 의미에서는 dup두 가지 인수를 취합니다. 유형a 과 value 합니다 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 , 일부 typeclass 기계. 모든 것을 설명 할 수는 없지만 기본적인 통찰력을 제공 할 수 있기를 바랍니다. 직관적으로

foo :: forall n . some type using n

논쟁으로 받아들이다 @n런타임에 전달되지 않는 일종의 컴파일 타임 자연 로 사용합니다. 대신에

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

제약 조건 을 만족시키는 증명@n 과 함께 (컴파일 타임) 이 걸립니다 . 후자는 런타임 인수이며의 실제 값을 노출 할 수 있습니다 . 사실, 당신의 경우에는 모호하게 닮은 것이 있다고 생각합니다.nC nn

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형식 수준을 유지하면 컴파일러에서 더 많은 정적 검사를 수행 할 수 있습니다. 예를 들어, 유형이 “integers modulo 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경우에도 전화를 걸 수 있습니다 . 안좋다. 대신에n5

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

일이 잘못되는 것을 방지합니다. 컴파일러는 모든 것을 정적으로 검사합니다. 코드는 사용하기가 더 어렵지만, 사용하기 어렵게 만드는 것이 요점입니다. 사용자가 잘못된 계수를 추가하는 것을 불가능하게 만들고 싶습니다.

결론 : 이들은 매우 고급 확장입니다. 초보자 인 경우 이러한 기술을 향해 천천히 진행해야합니다. 짧은 연구 후에도 이해할 수 없다면 실망하지 마십시오. 시간이 걸립니다. 한 번에 작은 단계를 수행하고 각 기능의 요점을 이해하기 위해 몇 가지 연습을 해결하십시오. 그리고 당신은 붙어있을 때 항상 StackOverflow를 가질 것입니다 🙂

답변