왼손잡이해방연대 아지트

사용자 확인중...

기묘한 것

왼손잡이해방연대,

35

2

연구의 일환으로 람다식으로 람다식을 계산하는 방법을 생각하고 있었다. 기존의 다양한 람다 계산기 구현을 찾아보던 중 기묘한 것을 찾았다. 기존의 것이라기에는 올초에 나온 따끈따끈한 논문이지만 꽤 재미있다.

그 제목은 Duality of λ-Abstraction. 듀얼리티는 우리말로는 쌍대성이던가? 대충 서로 뒤집힌 구조가 있으면 듀얼이라고 하는 것 같다. 타입 세계에도 여러 듀얼이 있다는데 아무튼 듀얼은 만능이라는 것이 어느 게임에서는 잘 알려져있다.

여기서 뒤집는 것은 함수 만들기(abstraction, λx.e)와 함수 호출하기(application, f(x))다. 이름은 coabstraction, coapplication 이래놨는데 co-를 나타낼 적절한 쉬운전문용어가 아직 없는 것 같으니 그냥 코함수 코호출 해야겠다. 함수를 fn (x : A) => e로 쓰듯이 코함수는 cofn (x : ~A) => e로 쓴다. e가 B 타입일 때 함수는 A → B가 되는 한편, 코함수는 A + B가 된다. 호출의 타입은 f : A → B, x : A일 때 f(x) : B인 한편, 코호출의 타입은 f: A + B, x: ~A일 때 f@x : B가 된다.

코함수 cofn (x : ~A) => e는 x가 코호출되면 x의 값이 되고, x가 안 쓰이고 e가 다 계산되면 그 값이 된다. 코호출 f@x는 코함수 안에서 쓰게 되는데, f가 A의 값이면 이후에 하려던 계산은 다 버리고 바로 코함수가 있던 곳으로 돌아가고, f가 B의 값이면 코호출 식이 그 값이 된다.

예를 들어 아래 프로그램을 실행해보자.

let div : int -> int -> (int + error) = fn n m =>
  if m = 0 then Left div_by_zero
           else Right (n / m)
in
cofn (err : ~error) => (div 3 0)@err + (div 13 4)@err

코드가 오른쪽부터 실행된다면:

   cofn (err : ~error) => (div 3 0)@err + (div 13 4)@err
-> cofn (err : ~error) => (div 3 0)@err + (Right 3)@err
-> cofn (err : ~error) => (div 3 0)@err + 3
-> cofn (err : ~error) => (Left div_by_zero)@err + 3
-> Left div_by_zero

이렇게 된다. (Right 3)@err는 그냥 3이 되었지만, (Left div_by_zero)@err를 계산하는 순간 3을 더하고 어쩌고 하려던 걸 다 관두고 err를 처음 도입했던 cofn ... 식의 값 자체가 Left div_by_zero로 계산되었다.

기존의 기능에 빗대어 본다면 try-catch/throw와 비슷하다. 근데 이제 예외를 던져서 어디로 갈지를 던지는 쪽에서 결정할 수 있다는 느낌이다.

생각해보니 Rust에 비슷한 기능이 있다. Result<Data, Error>를 리턴하는 함수에서는 e?를 하면 바로 에러를 던질 수 있다.

fn div(n: int, m: int) -> Result<int, error> {
  if m == 0 then Err(DivByZero) else Ok(n / m)
}

fn foo() -> Result<int, error> {
  Ok(div(13, 4)? + div(3, 0)?)
}

비슷한 것 같기도... 다만 Rust에서는 예외를 함수 리턴값까지만 보낼 수 있다.

이상 따끈따끈한 프로그래밍 언어 기능을 알아보았다. 기능 자체는 C언어의 longjmp랑 비슷하니 예전부터 있던 것이다. 다만 그 무시무시한 걸 함수형 언어 세계에서 타입-안전하게 쓸 수 있다는 점이 기묘한 것 같다. 사실 논문의 주요 포인트는 이 기능을 어디다가 쓸까 하는 것 보다는 타입 세상에서 새로운 듀얼을 발견해서 신난다는 느낌이다. "타입은 수학이다"라는 주장(커리-하워드 대응)을 적용해보면 ~A 타입은 not A에 해당한다. 전통적으로 not은 A -> False 타입에 대응시켰었는데 그런 식으로는 (not A) or A나 not (not A) = A 같은 당연한 성질들을 증명하지 못한다. 반면 ~A 타입으로는 다 된다고 한다. 프로그래밍 언어 수업에서 지나가듯 not 타입에 대한 이야기가 있었던 것도 같다. 반증으로 증명하기에 대응이 되지 않을까.

읽다보니까 랩에서 얘기가 나왔었던 것도 같고... 암튼 재밌었다.

목록