다형 채널과 Send 바운드

두 회가 병행 처리의 타입 시스템을 거의 완전하게 했다: 술어가 값이 스레드를 넘어도 되는가를 정하고, 흐름 pass가 이미 넘었는가를 좇는다. 하지만 리뷰가 한 틈을 남겼음을 찾았고, 그것은 흐름에 대한 것이 아니라 —— 추론이 아직 확정하지 않은 타입에 대한 것이다. 채널은 어떤 요소 타입의 값을 나르고, 그 타입은 Send여야 한다. 그것을 검사하는 것은, 요소 타입이 구체적일 때는 쉽다. 요소 타입이 아직 변수일 때는 쉽지 않다.

다형의 경우의 구멍

첫 판은 Send 요건을, 그것이 명백히 생기는 바로 그 자리에서 검사했다: 채널의 요소 타입이 표기에 쓰이는 곳, 그리고 send 조작이 구체적 인자에 적용되는 곳. 특정 타입으로 채널을 쓰는 어느 프로그램 에도, 그것은 모든 것을 잡는다. 하지만 작은 wrapper —— 채널을 취해 그것에 무언가를 보내는 함수, 요소 타입에 대해 총칭적으로 쓰인 —— 를 생각하라. 여기서 요소 타입은, 추론이 무엇 구체적인 것으로도 결코 해결하지 않을 수 있는 타입 변수이고, 첫 판은, 미해결 변수를 만나면, 낙관적으로 그것을 지나가게 했다.

그 낙관은 건전하지 않다. 총칭적 채널 wrapper는, 무엇이든 부어 넣을 수 있는 구멍이다: 한 번 검사하고, 그다음 보낼 수 없는 타입으로 실체화하면, 설계가 스레드 경계를 넘는 것을 금하는 값이 wrapper 안에서 넘고, 그 Send 의무는 실제로는 결코 discharge되지 않는다. 틈은 작고 놓치기 쉽다 —— 그것이야말로, 테스트가 아니라 리뷰가 그것을 떠올린 이유이고, 두 회 전에 Send의 구조적 구멍이 떠오른 것과 같다.

교과서적 수정, 그리고 왜 아닌가

“술어를 만족해야 하는 타입 변수”로의, 잘 알려진 완전히 일반적인 답이 있다: qualified types, Haskell이나 Rust 같은 언어의 trait 제약 기구다. Send 요건을 제약으로 타입 변수에 붙이고, 들고 다니고, 변수가 해결될 때 discharge하고, 그리고 —— 비싼 부분 —— 정의가 재사용 가능한 다형 스킴으로 generalize될 때, 남은 제약을 스킴에 기록하고, 그래서 이후의 모든 사용이 그것을 재검사한다. 그것은 일반적으로 옳은 답이고, 타입 클래스를 가진 성숙한 타입 시스템이 하는 것이다.

Mere의 타입 검사기는 그것을 갖지 않고, 여기서 그것을 채택하는 것은 그것을 세우는 것을 뜻한다. 그 스킴은 제약을 전혀 나르지 않고 —— 다형 타입은 그저 양화된 변수를 가진 타입으로, 딸린 의무가 없다 —— 그리고 시스템 어디에도 제약 solver가 없다. qualified types를 더하는 것은, solver를 더하고, 제약을 generalize와 instantiate에 꿰고, 추론의 모든 부분에 손대는 것을 뜻한다. 그것은 큰 새 서브시스템이고, 일부러 solver 없이 유지된 타입 검사기의 성격을 바꿔 버린다. 상황은 이펙트 시스템의 고차 함수 선택과 꼭 같은 형태다: 세련된 일반적 답은 존재하고, 그것을 채택하는 것은, 타입 시스템이 이미 얼마나 무겁고자 하는가에 대해 내린 결정에 반한다.

더 값싼 규칙: 아직 Send를 지는 것을 generalize하지 않기

그래서 바운드는 solver 없이, 겨냥한 규칙으로 강제된다. 추론이 도는 대로, Send 의무가, 채널이나 병렬 map의 요소 타입이 나타나는 곳에서 pending 리스트로 push된다. 정의가 generalize될 각 점에서 —— 그리고 최상위 선언의 끝에서 —— discharge pass가 pending 의무를 walk한다. 구체 타입에 대해서는, 그저 Send를 검사하고, 실패하면 에러를 보고한다. 아직 미해결이고 generalize되려는 타입 변수 —— 그것이 바로 다형 채널의 경우 —— 에 대해서는, 하나의 규칙을 적용한다: 그것을 generalize하지 않는다.

변수를 generalize하기를 거부하는 것이, 구멍을 닫는다. generalize된 변수는, 많은 다른 타입으로 실체화될 수 있는 변수이고, 그것이야말로 밀수 공격이 요하는 자유다 —— wrapper를 한 번 검사하고, 보낼 수 없는 타입으로 재사용한다. generalize되지 않은 변수는, 둘째 타입으로 재사용될 수 없다; 그 binding은, 첫 구체적 사용에서 그 요소 타입이 고정되는 단형 채널 함수가 된다. 보낼 수 없는 값을 통과시킨 경로는 사라진다, 그것을 가능하게 한 다형성이 그저 사양되기에. 그런 변수가 어느 사용으로도 결코 확정되지 않으면, 그것은 명시적 에러로 떠오른다 —— 채널의 요소 타입이 모호하다, 표기하라 —— 조용히 통과하는 것이 아니라.

이것은 단형화 제약이다: 변수가 generalize 시점에 아직 채워지지 않은 의무를 나를 때, 그것을 단형으로 유지한다. 건전성을 지키기 위해 다형성을 제한하는 것은 잘 밟힌 수다 —— ML의 value restriction, Haskell의 monomorphism restriction은 같은 본능이다 —— 그리고 그것은, 제약 solver가 요구할 기구의 어느 것도 없이 건전성을 산다. 병행 처리의 타입 이야기의 전부가, 타입 시스템이 늘 그러했던 것인 채다: Hindley–Milner 추론과, 한 줌의 ad-hoc 구조적 술어 —— Trivial, 정리를 요하는, 그리고 이제 Send와 Sync —— 로, 어디에도 일반적 solver가 없다.

그 대가, 그리고 기다리는 것

대가는, 특정하고 좁은 표현력의 상실이다: 진짜로 다형인 채널 콤비네이터를 쓰고, 한 프로그램 안에서, 여러 다른 요소 타입으로 재사용할 수 없다. 이것을 이끈 trial은, 그 패턴을 rare라 판했고, 완전히 일반적인 답 —— qualified types —— 은 버려지는 것이 아니라 미뤄지고, 실제 프로그램이 언젠가 그 재사용을 요하면 다룰 미래의 물음으로 철되었다. 이것은 다시 한 번, 되풀이되는 규율이다: 건전한 최소의 것을 지금 세우고, 일반적 답을 선반에 두고, 사용으로 발견되는 진짜 수요에, 그 대가를 치를지를 정하게 한다.

이것으로, 병행 처리의 타입 시스템의 절반이 완성된다. 설계는 좁혀지고, 술어는 건전해지고, move는 제어 흐름을 넘어 좇아지고, 마지막 다형의 틈은 닫혔다 —— 그 전부가 solver 없는 Hindley–Milner 코어 안에서, 다섯 Part 전에 세워진 언어와 정합하여. 남는 것은, 그것을 실제로 돌리는 것이다: spawn과 채널을 진짜 스레드와 진짜 공유 메모리로 바꾸고, 그것을 네 번, backend마다 한 번, 어느 둘도 어긋나게 하지 않고 행한다. 다음 회: 네 backend에서 병행을 돌리기.