ST 모나드 - forall의 강력함

IO와 비슷하지만, forall의 추가로 타입 체커가 많은 걸 보장합니다.

ST 모나드의 용도

용도 요약
Mutation이 위험한 이유가 뭘까요? 한 쓰레드가 Mutation이 가능한 값을 수정해 놓을 필요가 있을 때, 값을 읽고, 값을 수정해서 다시 쓰려고 할 때, 다른 쓰레드가 바꿔 놓으면 원하는 값을 유지하기 어렵습니다. 바로 여러 쓰레드가 비동기로 접근해서 생기는 문제입니다. 만일, Mutation이 일어나는 동안 하나의 프로세스만 접근한다는 걸 보장한다면 어떨까요?

한 쓰레드 내에서만 Mutation이 일어나고, 이 Mutation이 이 쓰레드를 벗어나는 일이 없다면, Mutation도 안전해질 수 있습니다.

자세한 내용은 아래 다믜님의 슬라이드를 참고해 주세요.
Haskell School Seminar - ST Monad - 다믜님

여기서는 한 쓰레드에서만 쓴다는 걸 어떻게 타입으로 보장하는지를 보는 게 목표입니다.

forall

forall - 아무거나와 모든 것의 차이

생각 스트레칭

RankNType

Is having a (a -> b) -> b equivalent to having an a? 답변에서 소스 발췌

forall b. (a -> b) -> b

이 타입 함수는 (a -> b) 함수를 받으면 b를 돌려줍니다. 안에 a를 가지고 있어야 합니다. 하지만 a가 뭔지를 모르니 구현이 안되겠구나로 생각했습니다. 그런데, a가 당장은 뭔지 모르지만, 나중에 알려 줄 방법이 있다면 어떻게 될까요?
보기 좋게 하기 위해, 위 서명으로 타입을 만들고,

-- 여기서 a는 forall이 아니라, 나중에 Box a 타입이 만들어질 때 결정됩니다.
type Box a = forall b. (a -> b) -> b

이 타입을 만들어내는 함수를 따로 두면 됩니다.

box :: a -> Box a
box a = \f -> f a

forall b. (a -> b) -> b 타입을 말로 읽어 보았습니다.
예를 들어 10이상이면 big, 아래면 small이라 하고, 이를 구분하는 함수를 isBig이라 하면, “5라는 숫자는 isBig을 만나면 small이 될 수” 입니다. 즉,

“a는 (a -> b)를 만나면 b가 될 놈” 입니다.

그런데 그냥 b가 될 놈이 아니라, forall b. (a -> b) -> b가 될 놈입니다. 이 함수의 구현은 b에 전혀 의존하지 않는 구현이란 얘깁니다. b가 무슨 타입이 들어오든 (a -> b) -> b 구현이 문제가 생기지 않아야 합니다. 위 예처럼 box함수가 하듯이 먼저 a를 넣어 놓으면, b가 어떤 함수든 (a -> b)인 함수를 넣어줄 수 있습니다.

※ 그래서 a는 forall b. (a -> b) -> b로 표현할 수 있습니다. 참고 - 홈펑터와 요네다 보조 정리

폴리모픽 자리에는 언젠가는 구체 타입이 들어온다.

forall a. Show a => a라고 되어 있으면, 언젠가 Show 인스턴스가 정의되어 있는 타입이 들어올테고,
forall a. a라고 되어 있으면, 제한 없이 어떤 타입이든 들어올 겁니다.
(forall a. a -> b)라고 되어 있으면, “모든 타입을 받아도 문제 없이 b를 내뱉는 함수”가 들어 옵니다.

이 제한을 따르는 나중에 들어올 값에, 문제가 생기지 않게 구현되어 있다는 얘기입니다. 서명은 함수가 어떻게 구현되어 있는지 알리는 역할을 합니다. 제한된 타입들이 공통적으로 갖고 있는 메소드만을 써야만, 해당 타입들이 들어왔을 때 문제가 생기지 않습니다. 모든 타입이 공통적으로 가지고 있는 메소드는 없습니다. forall a. a (forall a. a -> b가 아닙니다.)의 경우, 즉 모든 타입에 문제가 생기지 않으려면, a 타입에 의존하는 동작이 아예 없어야 합니다. 아니면, 모든 타입에는 bottom이 있으니, undefined로 구현하는 방법이 있을 순 있습니다.

Return Type Polymorphic

Return 타입은 들어오는 값에 따라 결정 됩니다.

read :: Read a => String -> a

a는 Read클래스 인스턴스라는 것만 아는데, 최종 무슨 타입이 될까요?
나중에 부르고 있는 맥락에 따라 결정됩니다. 다른 함수와 만나게(조립하게) 되면, 그 함수들의 접점 타입을 참조해서 추론합니다.

ST 모나드와 forall

newtype ST s a = ST (STRep s a)
type STRep s a = State# s -> (# State# s, a #)

ST타입은 State# s를 받아 순서쌍을 돌려주는 함수를 가지고 있습니다.

-- 암시적으로 들어 있는 forall을 같이 써주면 
-- forall a. (forall s. ST s a) -> a 
runsST :: (forall s. ST s a) -> a

runState :: State s a -> s -> (a, s)와 비교하면 인자로 s를 받는 부분이 없습니다.

s는 어디서 올까요?

runST (ST st_rep) = case runRW# st_rep of (# _, a #) -> a

GHC.Exts에 프리미티브로 다음과 같이 정의되어 있습니다.

runRW# :: forall (r :: RuntimeRep) (o :: TYPE r). (State# RealWorld -> o) -> o
runRW# m = m realWorld#

컴파일러가 특별하게 처리할 realWorld#을 s자리에 넣어주고 있습니다.
인자로 넘어 오는 ST계산computation을 보면 (forall s. ST s a)가 들어 오게 될테니, s는 어떤 타입을 줘도 상관 없다는 얘기입니다.

RankN인 것과 아닌 것의 차이가 뭘까요?

runSTLike :: forall a s. (ST s a) -> a -- 가정
runST :: forall a. (forall s. ST s a) -> a -- 실제 구현

위부터 얘기하면, s가 꼭 모든 타입을 받아도 문제가 없는 ST계산이 들어 올 필요가 없습니다.
반면 RankN은 반드시 모든 타입을 받아도 문제가 생기지 않는 ST계산이 들어와야 합니다.

“The forall ensures that the internal state used by the ST computation is inaccessible to the rest of the program.”

이 차이가 어째서 이런 결과를 만들어 낼까요?

forall이 붙지 않은 위의 경우, 모든 타입을 받아도 문제가 없는 ST계산이 아니라, Int를 State로 받는 계산이거나, String을 State로 받는 계산 등, 특정 타입을 State로 받는 ST계산이 들어올 수 있습니다. 즉, State가 무슨 타입인지 알 수 있습니다. 나중에라도 State가 무슨 타입인지 알 수 있다는 얘기입니다. 마지막, 결과값에서 이 State를 볼 수가 있습니다. 즉, State가 필요한 Ref들이 빠져나갈 수 있습니다.

반면, RankN으로 (forall s. ST s a)로, 괄호 안에 forall이 있을 경우, 반드시 State로 모든 타입을 받을 수 있는 ST계산만 들어와야 합니다. State 타입이 뭔지 알 수가 없다는 얘기입니다. 안에서 이 값이 바뀌더라도 바깥에서는 이 타입이 뭔지 알 수가 없습니다. 다시 말해, 괄호 안의 forall 스코프는 괄호안으로 한정됩니다.

ST모나드의 목표는 Mutation이 일어나는 ST s (STRef s a)를 안전하게 쓰자입니다.

data STRef s a = STRef (MutVar# s a)
data MutVar# s a

이 걸 runSTFake와 runST에 넣어주면 어떻게 되나 보겠습니다.

runSTFake :: forall a s. ST s (STRef s a) -> STRef s a
runST :: forall a. (forall s. ST s (STRef s a)) -> STRef s a

runSTFake에서 ST s (STRef s a)가 아니라, 전체 runSTFake는 s가 어떤 타입이 들어와도 문제 없는 구현이란 뜻입니다. ST안에 들어 있는 s와 결과 STRef s a에 있는 s는 같은 s입니다. 이럴 경우 원래 ST의 목적과는 달리 State가, 즉 STRef형태의 값들이 빠져 나갑니다.
runST는 어떤 타입의 s에도 문제 없는 ST계산을 받아서, 즉 s가 뭔지 모르는 계산을 받아서, 모르는 s에 의존하는 STRef s a를 내뱉고 있습니다. forall s가 Rank2로 걸려 있어, 마지막 결과 s와는 다른 값입니다. 헛갈리지 않게 다시 쓰면

runST :: forall a s'. (forall s. ST s (STRef s a)) -> STRef s' a

즉, ST안에 있는 s와 바깥의 s'은 같은 값이 아닙니다. 이 경우 타입 불일치 에러가 납니다. 즉 forall 하나를 추가하는 것 만으로, 타입 체커가 ST안에서 만든 Ref값 같은 것들이 ST를 벗어날 수 없음을 보장할 수 있습니다.