Void

1. 타입 체커를 영리하게 이용해 먹는 패턴
2. 절대 평가 되지 않을 값이면 무슨 타입을 써주는 게 좋을까요?
3. 평가되지 않을 값의 타입이라도 GHC는 타입 체커를 돌립니다.
4. 결과 타입에 폴리모픽을 두는 트릭
5. Void
6. RankNTypes

타입 체커를 영리하게 이용해 먹는 패턴

Void는 값이 없습니다. 값이 없으니 다른 값들과 어울려 뭔가를 하지 못합니다. 타입은 값들의 추상화인데, 값도 가질 수 없는 타입이 왜 필요할까요? 하스켈의 타입 정보는 런타임에는 모두 사라집니다. 타입은 값이 있든 없든 런타임에서 쓰이는 게 아니라, 컴파일 타임에 타입 체커가 써먹습니다. Void는 타입 체커는 통과할 수 있고, 실제 값을 가지면 안되는 그런 곳에 사용합니다. 그런 곳이 어디일까는 아래 예시를 보세요. ※ dependent type 스타일은 타입 체커 기능을 극단적으로 활용하는 방법입니다.

https://www.fpcomplete.com/blog/2017/07/to-void-or-to-void/
여기 코드들은 모두 fpcomplete void 글에서 가져왔습니다. fpcomplete void 글을 읽으며, 고민됐던 부분들을 적었습니다.

절대 평가 되지 않을 값이면 무슨 타입을 써주는 게 좋을까요?

절대 평가 되지 않는 경우가 뭐가 있을까요?

loop :: IO ()
loop = do
  putStrLn "Ye!"
  loop

GHC는 절대 loop 결과값 ()을 평가할 일이 없습니다. 무한 루프를 돌며 빠져 나가는 때는 error signal을 받을 때 말고는 끝낼 일이 없기 때문에 리턴값으로 Caller에게 ()를 주는 일은 일어나지 않습니다. 그래서 lazy한 하스켈은 IO Int를 써주든 IO NeverBeEvaluated를 써주든 아무 상관이 없습니다. 절대 평가될 일이 없지만, IO는 타입 변수를 하나 갖는다는 규칙에 맞추기 위해 형식상 하나는 써줘야 합니다. 보통은 이럴데 ()을 써줍니다. 그런데 여기에 타입 지정을 하면 GHC에게 일을 하나 시킬 수 있습니다.

updateTimeRef :: IORef String -> IO () --------------(A)
--                                  ^^
-- 시간을 주기적으로 업데이트 해서 IORef에 넣는 코드.
...

useTimeRef :: IORef String -> IO SomeResult
-- IORef에서 시간을 꺼내서 작업하는 코드

getSomeResult :: IO SomeResult
getSomeResult = do
  now <- getCurrentTime
  timeRef <- newIORef (show now)
  eres <- race (updateTimeRef timeRef) (useTimeRef timeRef)
  case eres of
    Left () -> error "This shouldn't happen!" -- (A-1)
    -- Left someResult -> return someResult -- (B-1)
    Right someResult -> return someResult

race는 두 쓰레드 중 하나가 끝나길 기다리는데, 실제론 updateTimeRef는 무한 루프이니, useTimeRef가 끝나길 기다리게 됩니다. useTimeRef가 끝나면 updateTimeRef도 kill 합니다. 결과값이 뭔지 평가하진 않지만, 타입 체커가 타입은 봅니다. 실제 Left 경우에 걸려들 일은 없지만, 타입 체커는 그럴지 안그럴지 알지 못합니다.

-- 실제 평가될 일은 없지만 IO SomeResult로 바꾸면
updateTimeRef :: IORef String -> IO SomeResult ------(B)
--                                  ^^^^^^^^^^

(A)의 경우

updateTimeRef의 결과 타입을 IO ()로 하면, 
Left someResult에서 someResult는 ()이 되고, 
return ()값 하게 되니, 
getSomeResult의 리턴 타입 IO SomeResult와 맞지 않아 컴파일 에러입니다.
그래서 이럴 땐 return () 하지 않고 error를 써서 예외를 발생 시킵니다. (A-1)

(B)의 경우

updateTimeRef의 결과 타입을 IO SomeResult로 하면,   
Left someResult에서 someResult는 SomeResult 타입이고, (B-1)
return SomeResult값 하게 되어
getSomeResult의 리턴 타입 IO SomeResult와 맞게 됩니다.
런타임에 값이 들어오든 말든 타입 체커는 타입만 봅니다.

getSomeResult의 결과 타입이 IO SomeResult이니, return SomeResult는 되지만, return ()는 타입 체커를 통과하지 못합니다. updateTimeRef는 무한 루프를 도니 IO 뒤에 뭐라 써주든 상관은 없습니다. 하지만, 타입 체커를 통과하려면 IO SomeResult로 맞추면 됩니다.

평가되지 않을 값의 타입이라도 GHC는 타입 체커를 돌립니다.

타입 체커는 런타임에 값이 평가될지 안될지는 보지 않습니다. 이걸 이용해서 updateTimeRef는 무한루프를 돌며 useTimeRef보다 먼저 죽지 않는다는 검증을 GHC가 하도록 할 수 있습니다. 프로그래머가 계속 신경쓰지 않아도 GHC가 알아서 체크해주면, 런타임에 가서 드러날 에러들을 줄일 수 있기 때문에, 하스켈에서는 타입 체커를 최대한 활용하려는 노력, 패턴들이 자주 보입니다.

뭘 써도 상관 없는 자리에 SomeResult를 넣으니, error를 써주지 않아도 부드럽게 getSomeResult를 정의할 수 있게 되었습니다. 여기서 그치는게 아니라, 숨어있는 이득이 있습니다. 실제 updateTimeRef는 SomeResult 타입 값을 만들어내지 않는데, SomeResult를 써 줄 수 있다는 말은 SomeResult가 평가되지 않는 무한 루프가 돈다는 뜻입니다. 풀어서 말하면, GHC가 updateTimeRef가 무한 루프가 도는지 체크를 하게 됐다는 겁니다.

그런데 아래 문장 때문에 잘 못 이해한 건 아닌지 의심스럽습니다.

The type system is in effect enforcing our requirement that useTimeRef will outlive updateTimeRef.

타입 체커가 useTimeRef가 updateTimeRef보다 오래 살아남아야 한다는 조건을 만족하는지 확인한다는 말입니다. 그런데, 거꾸로 아닌가요? updateTimeRef가 먼저 죽으면 안되는 거 아닌가요? outlive(~보다 오래 살다)를 잘 못 번역한건지, 문장이 거꾸로 쓰인걸로 보입니다.

저는 이해를 아예 못한 게 아니라, 이해는 한 것 같은데, 모순되는 텍스트들이 있으면 계속 되새김질 해보다 마지막에 자료를 의심합니다. 꽤 오랫동안 올라와 있던 포스트인데, 오류가 있다면 진작 잡아내지 않았을까요? 저와 같이 고민한 분들이 있으면 댓글을 달아 주시면 좋겠습니다.

useTimeRef보다 updateTimeRef가 더 빨리 죽으면 컴파일이 안되도록 타입 체커에게 힌트를 준 상황처럼 됐습니다. 타입 체커가 무한 루프를 체크합니다.

무한 루프의 리턴 타입은 실제 평가 될 일이 없기 때문에 아무거나 써줘도 됩니다. 그런데, 여기에 적절한 타입을 써주면, 프로그래머가 확인해야 될 걸 GHC에게 떠넘길수 있습니다.

아래 코드는 fpcomplete의 코드를 조금 더 단순하게 바꿔서 필요한 동작만 있도록 했습니다.

fpcomplete의 내용은, func를 IO MySpecial로 만들려면 무한 루프여야 한다는 뜻입니다. func가 실제로 리턴하는 값이 MySpecial이 아닌데, IO MySpecial로 써주려면 무한 루프인 경우뿐이 없으니, func가 무한 루프여야 하는 걸 GHC가 체크하는 효과가 난다는 뜻 입니다. func가 무한 루프이니 당연히 func2보다 func가 오래 삽니다.

import Control.Concurrent.Async (race)
data MySpecial = MySpecial Int

func :: IO MySpecial 
func = do
  putStrLn "ok"
  func

func2 :: IO MySpecial
func2 = do
    return $ MySpecial 1 

work :: IO MySpecial
work = do
  eres <- race func func2
  case eres of
    Left r -> return r
    Right r -> return r

익숙해지면 아래 코드만 봐도 무한 루프임을 눈치 챈다고 합니다. 리턴 타입이 폴리모픽인게 무슨 뜻일까요?

결과 타입에 폴리모픽을 두는 트릭

updateTimeRef :: IORef String -> IO a

보통은 함수의 출력에 타입 변수 a를 붙이는게 별다른 의미는 없다고 합니다. 그런데 여기처럼 쓰면 무한 루프임을 알려주는 의미가 있다고 합니다. 아래 설명을 보면, 만일 updateTimeRef :: IORef String -> IO () 이라면,

getSomeResult :: IO SomeResult
...
    eres <- race (updateTimeRef timeRef) (useTimeRef timeRef)
    case eres of
        Left sRes -> return sRes --- (가)
        Right sRes -> return sRes

Left의 경우 sRes가 () 타입입니다. 그럼 getSomeResult :: IO SomeResult와 타입이 맞지 않아 타입 체커 에러입니다. 그럼 updateTimeRef :: ... -> IO SomeResult 로 바꾸면, 타입 체커가 sRes가 SomeResult 타입이므로 OK입니다. 만일, updateTimeRef가 손댈 수 없는 라이브러리에 있다면 어떻게 할까요? 이럴 때를 위해서 IO SomeResult가 아니라 IO a로 타입을 열어 놓는 방법을 쓰면 됩니다. updateTimeRef :: ... -> IO a 라면, 위와 같은 case문을 그대로 써도 됩니다.

useTimeRef :: ... -> IO SomeOtherResult
getSomeResult :: IO SomeOtherResult 

폴리모픽으로 만들어 놓으면, 위와 같이 IO SomeOtherResult로 바뀌어도 수정없이 쓸 수 있습니다.

실제 IO a가 의미하는 건 무한 루프이거나 예외 입니다. 둘 중에 뭐가 됐든 (가) Left 에 걸려들 일은 없습니다. 이런 타입을 보면 무한 루프이거나 예외를 던질 수 있겠다고 알 수 있습니다.

Void

실제론 값이 들어오면 안되는 자리지만, 타입 체커는 통과해야 할 때 Void를 써 줍니다. 위와 비슷하게 GHC에게 로직 체크 일부를 떠맡길 때 씁니다.

updateTimeRef :: IO SomeResult, 또는 IO a로 해 놓으면, 무한 루프가 아닌데도 오류가 나지 않는 경우가 하나 남아 있습니다. 여기선 그럴 일이 없겠지만, 실수로 SomeResult값을 리턴하게 바꾸면 타입 체커를 통과해버립니다. GHC가 무한 루프임을 체크해 주길 바랐는데, 구멍이 하나 있는 셈입니다.

이 구멍을 막을 수 있는 방법이 바로 Void입니다.

data Void
absurd :: Void -> a

Void는 값 생성자가 없습니다. absurd는 도메인의 모든 요소에 대해 매핑이 되어야 total 함수인데, 도메인에 요소가 없으면? 그럼 total 함수입니다. 만일 partial이라면 모든 값이 a와 매핑되지 않는다는 말로, 예외를 발생시키거나 무한 루프가 돈다는 얘기입니다. 어차피 total이든 아니든 타입 체커만 통과하면 될 것 같은데, total이 아닐 것처럼 생겨서 한 번 짚어 준 게 아닐까요? 어쨌든, case 문을 다음처럼 바꾸면

  case eres of
    Left voidValue -> absurd voidValue
    Right someResult -> return someResult

타입 체커는 군말없이 통과합니다. absurd는 Void타입 값을 받아 a를 리턴합니다. 런타임이 아니라 타입 체커를 위한 장치입니다. 폴리모픽 타입이니 컴파일은 통과할테지만, 언제라도 Void타입이라 표시한 voidValue에 값이 들어오면 타입 미스 매치가 일어날테니, Left에 걸려들게 코딩하면 GHC가 잡아내 줍니다. absurd는 Void를 받아서 a를 출력한다기 보다, 타입 체커 통과를 위해 Void값을 다른 모양으로 보이게 한다고 생각하면 편합니다.

a를 써서 어느 정도 해결할 수 있지만, Void를 쓰면 코드를 읽을 때 훨씬 더 직관적입니다.

RankNTypes

withSideThread :: IO void -> IO a -> IO a
withSideThread infinite finite = do
  res <- race infinite finite
  case res of
    Left x -> absurd x
    Right y -> return y

이렇게 하면 에러가 납니다.

    • Couldn't match type ‘void’ with ‘a’
      ‘void’ is a rigid type variable bound by
        the type signature for:
          withSideThread :: forall void a. IO void -> IO a -> IO a
        at /Users/michael/Desktop/foo.hs:7:19
      ‘a’ is a rigid type variable bound by
        the type signature for:
          withSideThread :: forall void a. IO void -> IO a -> IO a
        at /Users/michael/Desktop/foo.hs:7:19
      Expected type: IO a
        Actual type: IO void

이 에러를 피하기 위해 다음처럼 void를 a로 바꾸면

withSideThread :: IO a -> IO a -> IO a
withSideThread infinite finite = do
  res <- race infinite finite
  case res of
    Left x -> return x
    Right y -> return y

타입 체커가 무한 루프임을 체크해 주는 동작은 사라져 버립니다. 왜냐 하면 다음 처럼 쓸 수 있기 때문입니다.

getSomeResult :: IO SomeResult
getSomeResult = do
  now <- getCurrentTime
  timeRef <- newIORef (show now)
  withSideThread (return SomeResult) (useTimeRef timeRef)

타입 체커의 개런티는 그대로 가져가면서 정의하는 방법은

withSideThread :: (forall void. IO void) -> IO a -> IO a
withSideThread infinite finite = do
  res <- race infinite finite
  case res of
    Left x -> absurd x
    Right y -> return y

forall을 이용하는 방법입니다. forall의 자세한 설명은 참고글을 읽어주세요.

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

미완성 포스트… @todo: To Void or to void? 섹션을 이해하려면 positive, negative 개념을 명확히 한 후 봐야 할 것 같습니다.