docs Unison | 능력과 능력 핸들러 · Unison 프로그래밍 언어

Unison은 능력(ability) 이라는 편리한 기능을 제공하여, (비동기) I/O, 스트림 처리, 예외 처리, 파싱, 분산 계산 등 여러 작업을 일반적인 Unison 문법 그대로 작성할 수 있게 해줍니다. Unison의 능력 시스템(문헌에서는 종종 "대수적 효과(algebraic effects)"라고 부름)은 Sam Lindley, Conor McBride, Craig McLaughlin의 Frank 언어를 바탕으로 합니다. Unison은 이 논문에서 제시된 체계와 약간 다릅니다. 특히 다음과 같습니다:

• Unison의 능력 다형성은 일반적인 다형 타입으로 제공되며, 비어 있는 능력 집합을 가진 Unison 타입은 어떤 능력도 명시적으로 허용하지 않습니다. Frank에서는 비어 있는 능력 집합이 능력 다형 타입을 의미합니다.
• Unison은 함수 적용 구문을 능력 처리에 재사용하지 않고, 그 대신 별도의 handle 구문을 둡니다.

능력이 포함된 함수 타입

Unison에서 함수 타입의 일반적인 형태는 I ->{A} O입니다. 여기서 I는 함수의 입력 타입, O는 출력 타입, A는 이 함수가 요구하는 능력 집합입니다. 더 일반적으로, I ->{A1,A2,A3} O처럼 임의의 타입들을 콤마로 나열할 수 있습니다.

Unison에서 A -> B라는 함수 타입은 사실 A ->{e} B 타입의 문법 설탕(syntactic sugar)일 뿐이며, 여기서 e는 (비어 있을 수도 있는) 어떤 능력 집합입니다. 특정 함수가 능력을 전혀 요구하지 않는다는 것을 확실히 나타내려면 A ->{} B처럼 비어 있는 능력 집합을 사용합니다.

능력에 대한 타입 검사 규칙

능력에 대해 사용되는 일반적인 타입 검사 규칙은 다음과 같습니다. {A1,A2} 능력을 요구하는 함수 호출은, 최소한 {A1,A2} 능력이 사용 가능한 문맥 안에서만 발생해야 합니다. 그렇지 않으면 타입체커가 능력 검사 실패(ability check failure)를 보고합니다. 능력은 handle 블록(아래에서 설명)이나 타입 시그니처를 통해 사용할 수 있게 됩니다. 예를 들어 함수 본문 안에서 Text ->{IO} Nat 타입을 가진 함수라면, 그 본문에서는 {IO} 능력이 사용 가능하며, 따라서:

• f : Nat ->{} Nat 함수를 호출할 수 있습니다. f의 능력 요구 사항은 {}이며, 이는 사용 가능한 {IO} 능력 집합의 부분집합입니다.
• g : Text ->{IO} () 함수도 호출할 수 있습니다. g의 요구 사항은 {IO}이고, 이것 역시 사용 가능한 {IO} 능력 집합의 부분집합입니다.

여러 개의 인자를 받는 함수에 대해선 다른 규칙이 필요해 보일 수 있지만, 실제로는 동일합니다. 함수 본문은 시그니처에 있는 해당 함수 타입에 붙어 있는 능력들을 사용할 수 있습니다. 다음 예제는 타입이 통과되지 않습니다. 시그니처에 따르면 함수 본문은 순수해야 하기 때문입니다:

unison
doesNotWork : Text ->{Exception,IO} Text ->{} Nat
doesNotWork arg1 arg2 =
  printLine "Does not work!"
  42

하지만, 순수한 함수를 반환하기 전에 IO를 처리하면 타입 검사가 잘 통과됩니다:

unison
doesWork : Text ->{IO, Exception} Text -> Nat
doesWork arg1 =
  printLine "Works great!"
  arg2 -> 42

함수 본문 안에 포함되지 않은, 최상위 정의(top-level definition)는 순수해야 합니다. 예를 들어 다음은 타입이 통과되지 않습니다:

unison
msg = printLine "hello"

그러나 msg = '(printLine "Hello")라고 쓰면 타입 검사가 잘 됩니다. 이제 printLine 호출이 {IO} 요구 사항을 가진 함수 본문 안으로 들어갔기 때문입니다(직접 시도해 보세요!).

🤓 최상위 정의가 순수해야 한다는 이 제약은, 향후 Unison 버전에서 제거될 수도 있습니다.

능력 추론

f에 대해 능력 요구 사항을 추론할 때, 그 함수 본문 안에서 호출될 수 있는 모든 함수가 요구하는 능력들의 합집합이 f의 능력 요구 사항이 됩니다.

사용자 정의 능력

사용자 정의 능력은 다음과 같은 ability 선언으로 정의합니다:

unison
structural ability Store a

능력은 반드시 structural 또는 unique 키워드 중 하나와 함께 정의해야 합니다. 두 키워드의 차이에 대해서는 unique 타입과 structural 타입 섹션을 참고하세요.

이 선언은 타입 인자 a를 받는 새로운 능력 타입 생성자 Store를 만듭니다. 또한 값 레벨에서 Store.get과 Store.put이라는 두 개의 생성자도 함께 만듭니다. Store.get은 어디선가 타입 a의 값을 "가져올(get)" 수 있는 능력을 제공하고, Store.put은 타입 a의 값을 어딘가에 "저장(put)"할 수 있게 해 줍니다. 이 값들이 실제로 어디에 저장되는지는 핸들러에 따라 달라집니다.

Store의 생성자인 Store.get과 Store.put의 타입은 다음과 같습니다:

• Store.get : {Store a} a
• Store.put : a ->{Store a} ()

{Store v} 타입은, 해당 결과를 계산하는 과정에서 Store v 능력이 필요하며, 이 능력을 제공하는 능력 핸들러의 문맥 안에서만 실행될 수 있음을 의미합니다.

능력 핸들러

어떤 능력 A와 타입 T에 대해, 생성자 {A} T(또는 이 생성자를 사용하는 함수)는 오직 능력 A가 제공되는 스코프 안에서만 사용할 수 있습니다. 능력은 handle 식으로 제공됩니다:

unison
handle e with h

이 식은 표현식 e가 함수 h가 처리하는 능력들에 접근할 수 있도록 해 줍니다. 구체적으로, e의 타입이 {A} T이고 h의 타입이 Request A T -> R라면, handle e with h의 타입은 R이 됩니다. Request 타입 생성자는 Unison이 제공하는 특수한 내장 타입으로, 능력 A에 대한 핸들러에 Request A T 타입의 인자를 전달합니다. e의 타입이 {A} T라면, 이를 처리하기 위해 h는 반드시 Request A T 타입의 인자를 받을 수 있어야 합니다. 어떤 스코프에서 필요로 하는 능력이, 둘러싼 handle 표현식들 중 어느 것에서도 제공되지 않는다면, 결국 타입 오류가 발생합니다.

다음 섹션의 예제는 능력 핸들러가 어떻게 동작하는지 더 잘 보여줍니다.

능력 생성자에 대한 패턴 매칭

각 능력의 생성자는 능력 핸들러에서 사용할 수 있는 패턴 하나에 대응합니다. 그러한 패턴의 일반적인 형태는 다음과 같습니다:

unison
{A.c p_1 p_2 p_n -> k}

여기서 A는 능력 이름, c는 생성자 이름, p_1부터 p_n까지는 생성자 인자를 매칭하는 패턴들이고, k는 프로그램의 계속(continuation)입니다. 매칭되는 값의 타입이 Request A T이고, 그 값에 사용된 생성자의 타입이 X ->{A} Y였다면, k의 타입은 Y -> {A} T가 됩니다.

계속(continuation)은 항상 능력 생성자의 반환 값을 인자로 받는 함수이며, 이 함수의 본문은 생성자 호출 직후에 이어지는 handle .. with 블록의 나머지 부분입니다. 예제는 아래를 참고하세요.

핸들러는 계속을 호출할지 말지, 혹은 여러 번 호출할지 선택할 수 있습니다. 예를 들어, 프로그램 실행을 중단(abort)하는 능력을 처리하기 위해 계속을 무시할 수 있습니다:

unison
structural ability Abort

toDefault!.handler : '{g} a -> Request {Abort} a ->{g} a
toDefault!.handler default = cases
  { a }                -> a
  { Abort.abort -> _ } -> default()

프로그램 p에서 Abort.abort 호출을 제거하면, p는 6으로 평가됩니다.

능력 생성자는 시그니처상 다음과 같이 주어지지만

unison
abort :
    ()

실제 타입은 {Abort} ()입니다.

{ Abort.abort -> _ } 패턴은 p 안에서 Abort.abort 호출이 발생했을 때 매칭됩니다. 이 패턴은 계속을 호출하지 않을 것이므로(이런 식으로 프로그램을 중단합니다) 계속을 무시합니다. 이 시점에서의 계속은 _ -> x + 2라는 식입니다.

{ x } 패턴은 계산이 순수한 경우(더 이상 Abort 능력을 요청하지 않고, 계속이 빈 경우)를 매칭합니다. Request에 대한 패턴 매칭은 이 경우를 처리하지 않으면 완전하지 않습니다.

핸들러가 계속을 호출할 때는, 보통 재귀 호출을 통해, 프로그램의 나머지 부분에서 능력이 어떻게 제공될지 기술해야 합니다. 예를 들어:

unison
use base Request

structural ability Store v where
  get : v
  put : v -> ()

storeHandler : v -> Request (Store v) a -> a
storeHandler storedValue = cases
  {Store.get -> k} ->
    handle k storedValue with storeHandler storedValue
  {Store.put v -> k} ->
    handle k () with storeHandler v
  {a} -> a

storeHandler의 with 절은, 계속에서 발생한 Request들을 처리하기 위해 storeHandler 자신을 다시 사용합니다. 즉, 재귀 정의입니다. 타입 v의 초기 "저장된 값"은 storedValue라는 인자로 핸들러에 전달되며, 값이 바뀌는 것은 각 재귀 호출에 서로 다른 값이 전달된다는 사실을 통해 표현됩니다.

Store.get 패턴에서, 계속 k는 v를 인자로 기대합니다. Store.get의 반환 타입이 v이기 때문입니다. Store.put 패턴에서 계속 k는 ()를 인자로 기대하는데, 이것이 Store.put의 반환 타입입니다.

이는 storeHandler와 여러 계속들(모두 k라는 이름을 가짐) 사이의 상호 재귀(mutual recursion)라는 점이 흥미롭습니다. 하지만 이들은 서로 꼬리 위치(tail position)에서 호출하므로 아무 문제가 없고, Unison 컴파일러는 꼬리 호출 제거를 수행합니다.

위 핸들러를 사용하는 예는 다음과 같습니다:

unison
modifyStore : (v -> v) ->{Store v} ()
modifyStore f =
  v = get
  put (f v)

여기서, 핸들러가 Store.get을 받았을 때의 계속은 v -> Store.put (f v)입니다. 핸들러가 Store.put을 받았을 때의 계속은 _ -> ()입니다.