ST 참조는 투명합니까?

왜 ST은 다음 코드를 허용하지 않도록 설계 되었습니까? as shown in the wikibook? 이 기사에서는 ST 효과가 또 다른 ST으로 누설 될 것이라고 제안하는 것으로 보이지만 실제로는 이유를 이해하지 못합니다.ST 참조는 투명합니까?

특정 ST s (STRef s a)을 실행할 수없는 것 같습니다. ST 효과가 포함되어 있고 명확하게 투명하지만 그러한 사용은 여전히 유효하지 않은 것으로 간주됩니까?

직감 한 IO 많은 독립 ST가 그와 관련된 IO 및 ST의 의미의 차이가 있음을 알려줍니다,하지만 난 모르겠어요.

> runST (newSTRef True) 

<interactive>:5:8: error: 
    • Couldn't match type ‘a’ with ‘STRef s Bool’ 
     because type variable ‘s’ would escape its scope 
     This (rigid, skolem) type variable is bound by 
     a type expected by the context: 
      forall s. ST s a 
     at <interactive>:5:1-21 
     Expected type: ST s a 
     Actual type: ST s (STRef s Bool) 
    • In the first argument of ‘runST’, namely ‘(newSTRef True)’ 
     In the expression: runST (newSTRef True) 
     In an equation for ‘it’: it = runST (newSTRef True) 
    • Relevant bindings include it :: a (bound at <interactive>:5:1) 

> :t newSTRef 
newSTRef :: a -> ST s (STRef s a) 

> :t runST 
runST :: (forall s. ST s a) -> a

출처

2017-11-19 sevo

ST의 내 이해는 우주처럼 생각합니다. 모든 ST 연산은 하나의 우주를 다른 우주로 돌릴 수 있습니다 (돌연변이에 의해). 그렇기 때문에'ST'는'RealWorld'로 태그를 붙임으로써'IO'로 바뀔 수 있습니다. 그래서 여러분의 질문은'IO'가 순수한 것인지 묻는 질문과 정말로 같습니다. – HuStmpHrrr

'forall s 유형의 모든 값. ST A는'IO A '타입의 모든 값이 명확하게 투명하기 때문에 (즉, 값 자체가 아닌 결과 값을 생성하는 방법을 나타내는 계산이므로) 투명하게 나타납니다. 'ST s (STRef s A)'는'run '될 수 없지만 여전히 유효한 계산입니다; 예 : 'STREF s A -> ST s B' 형 함수를 적용하여 forall을 얻을 수 있습니다. ST s B'를 실행할 수 있습니다. 그러나 실제로 질문이 무엇인지는 확실하지 않습니다. 문제의 코드가 왜 허용되어야한다고 생각합니까? (참고 : "나는 왜 그럴지 잘 모르겠다") – user2407038

'ST'는 동적으로 할당 된 메모리와 그 메모리에 대한 포인터/참조를 허용한다. 그것은 원칙적으로 모든 메모리가'runST'의 끝에서 해제 될 수 있도록 설계되었습니다. 이를 위해서는'runST'를 벗어날 수있는 포인터가 없어야합니다. 그러한 이스케이프 된 포인터는 또한 평가 순서와 관련된 이상한 효과를 유발할 수 있습니다. f (runST $ writeSTRef r True) + g (runST $ readSTRef r)'는 어떤 runST가 먼저 평가되는지에 따라 다른 결과를 얻을 수있다. 참조 투명성은 그러한 주문 문제를 피하기위한 것입니다. – chi

더 질문 자체보다 질문 제목 대답,하지만 여전히 :

예, ST는 referentially 투명합니다. 이것은 단지 추측하고 믿어 오랫동안

, 만 올해 우리는 대한 적절한 증거가 :

국가의 단항 캡슐화에 대한 논리적 관계 : runST의 존재 상황 동등성을 입증
아민 Timany 레오 Stefanesco, 모르 텐 크로 - 제스 퍼슨, 라스 Birkedal
조건부 정말 understa하지 않습니다 2018
http://iris-project.org/Preprint PDF

출처

2017-11-19 22:10:37

을 POPL을 받아 당신이 요구하는 것, 그래서 나는 당신의 질문을 가장 할 것입니다 :

ST가 runST (newSTRef True)을 허용하지 않도록 설계된 이유는 무엇입니까? 그이 허용 된 경우

더 이상 referentially 투명하지 않을 것이다 :

main = do 
    let r = runST (newSTRef True) 
    evaluate (runST (writeSTRef r False)) 
    print (runST (readSTRef r))

이 코드는 출력 False 것.

main = do 
    evaluate (runST (writeSTRef (runST (newSTRef True)) False)) 
    print (runST (readSTRef (runST (newSTRef True))))

이 코드 (모든 사용자에 r을 인라인의 결과)의 출력하고자 True, runST (newSTRef True)의 각 인스턴스는 새로운 STRef 변수를 할당하는 것 때문이다.

실제로 runST이 구현 된 방법은 ST s 작업 내에 할당 된 모든 리소스가 해당 작업을 벗어날 수 없도록합니다.

IO과 의 차이는 runIO 기능이 없다는 것입니다. 여러 개의 독립적 인 IO 작업을 만들 수 있지만 runIO 없이는 아무런 문제가 없습니다. 실제로 IO 작업을 실행하는 유일한 방법은 main에 바인드하고 런타임 시스템이이를 받아 들일 수있게하는 것입니다 (이는 main을 감싸는 암시적인 runIO과 같습니다). IO 액션이 실행됩니다. 프로그램.

물론이 단일 동작은 여러 개의 작은 동작을 결합하여 구성 할 수 있지만 결국에는 여전히 단일체입니다. 반면에 runST은 여러 개의 ST s 작업을 독립적으로 실행할 수 있습니다.

출처

2017-11-19 22:47:09 melpomene

나는 내 질문이 내가 예상했던 것보다 더 복잡한 주제를 다루었다는 것을 깨닫고 나는 그것이 불분명하다는 것을 인정한다. 그러나이 대답은 저에게 (그리고 다른 사람들에게) 단서를줍니다. 처음에 나는'ST s a'가'a = STRef s x' 일 때 순수한 코드에서 실제 참조를 혼합했기 때문에 참조 투명성을 깨뜨릴 것이라고 잘못 가정했습니다! 그러나 실존 적 유형은'runST'의 정확성을 강화하는데 결정적인 것으로 보인다. 이 부분은 이해하기가 가장 힘들고 매우 영리한 발명품 (또는 발견 물) 인 것 같습니다. – sevo

ST 참조는 투명합니까?

답변

관련 문제