PureScript "내부"정량화 된 유형

Question

타일에 잘못된 용어가 있다고 가정합니다. 아래에서 대신 사용해야하는 내용을 알려주십시오.

runST :: forall a eff. (forall h. Eff (st :: ST h | eff) a) -> Eff eff a 

여기서 주목해야 할 것은이 지역의 H 타입은 함수 화살표의 왼쪽에있는 괄호 안에 정량화되어 있습니다 : PureScript by Example, section 8.17 Mutable State에서

는 runST의 유형에 대한 논의있다 . 즉, 우리가 runST에 어떤 행동을 하든지간에 어떤 지역에서도 작동해야합니다.

나는 최종 목표를 이해하지만, 사람이 유형의 관점에서이 문장을 명확히 할 수 있으며이 위에 따라 어떻게 제한됩니다?

가능한 경우 간단한 유형으로 차이를 표시 할 수 있습니까? 예 : 어떤 차이가 있습니까 :

f1 :: forall i o. Array i -> Array o 
f2 :: forall o. (forall i. Array i) -> Array o 

나는 짧은 예제가 도움이된다고 생각합니다.

Answer 1

어떤 유형의 값이 Array a입니까?

글쎄, 무엇이 a인지 알거나, a에 대해 알고 있다면 구체적인 예를 들어 줄 수있을 것입니다. a이 Int 인 것으로 알려진 경우 [1, 2, 3]은 좋은 답변입니다. a에 Monoid 인스턴스가있는 경우 [mempty]이 작동합니다. 그러나 a에 대해 알지 못하면 자신감있게 대답 할 수있는 유일한 대답은 []입니다.

어떤 유형의 값이 forall a. Array a입니까?

해당 유형에 거주하는 값이 a 인 경우 Array a에 있어야합니다. a에 대해 알지 못해서 대답은 "[]"입니다. 따라서 forall은이 경우 유형의 가능한 구현을 하나만하도록 제한합니다.

이제 forall a. Array a은 다른 유형과 마찬가지로 유형이므로 함수의 인수 유형으로 나타날 수 있습니다. 이러한 함수 호출자는 제공 할 수있는 값을 하나만 가질 수 있습니다. 해당 함수의 구현자인은 인 유형 a (선택한 유형으로 작동해야하므로) 인수를 사용하도록 선택할 수 있습니다.

runST에 대해서도 마찬가지입니다. runST의 구현자는 어떤 h이든 사용하여 작업을 호출 할 수 있으므로 작업 할 새 메모리 영역을 개념적으로 생성합니다. 호출자는 아무 것도 알지 못해도 주어진 메모리 영역에서 작업해야합니다. 즉, 제공된 동작 (newSTRef, writeSTRef 등)은 추상적으로 만 사용할 수 있으며 사용자가 만든 모든 참조는 runST 블록의 범위를 벗어날 수 없습니다 (유형 변수 h은 해당 범위 외부에 존재하지 않습니다). runST은 순수한 결과를 안전하게 반환 할 수 있습니다.

따라서 forall은 함수 인수로 제공 할 수있는 값을 제한하는 데 유용한 도구입니다.