상호 재귀

상호 재귀 (Mutual Recursion)

Agda는 상호 정의된 데이터 타입, 레코드 타입, 함수를 작성하는 여러 방법을 제공해요.

  • 옛 스타일의 mutual 블록 (Old-style mutual blocks)
  • 전방 선언 (Forward declaration)
  • 교차 상호 블록 (Interleaved mutual blocks)

마지막 두 가지는 선언과 정의의 교차를 허용해 어떤 타입이 상호 정의된 데이터 타입의 생성자를 참조할 수 있게 하므로, 첫 번째보다 더 표현력이 풍부해요.

교차 상호 블록 (Interleaved mutual blocks)

상호 재귀 함수는 교차 상호(interleaved mutual) 블록 안에 배치하여 작성할 수 있어요. 각 함수의 타입 시그니처는 그 정의 절(clause)과 다른 함수의 오른쪽 변에서의 사용 위치보다 먼저 와야 해요.

서로 다른 함수에 대한 절들은 (예를 들어 교육 목적으로) 교차될 수 있어요:

interleaved mutual

  -- 선언:
  even : Nat → Bool
  odd  : Nat → Bool

  -- zero는 짝수이고 홀수가 아님
  even zero = true
  odd  zero = false

  -- suc 경우: 전임자에서 짝수성을 전환
  even (suc n) = odd n
  odd  (suc n) = even n

모듈과 postulate 같은 임의의 선언을 상호 재귀 정의와 혼합할 수 있어요. 데이터 타입과 레코드에 대해 다음 문법이 선언을 생성자 도입과 분리하는 데 사용되며, 하나 또는 여러 개의 data ... where 블록으로 나뉘어요:

interleaved mutual

  -- 곱 레코드, 코드 유니버스, 디코딩 함수의 선언
  record _×_ (A B : Set) : Set
  data U : Set
  El : U → Set

  -- 우리 유니버스에 자연수 타입에 대한 코드가 있음
  data U where `Nat : U
  El `Nat = Nat

  -- 참고로 우리는 레코드에서 값 쌍을 만드는 법을 앎
  record _×_ A B where
    inductive; no-eta-equality; pattern
    constructor _,_
    field fst : A; snd : B

  -- 그리고 우리 유니버스에 쌍에 대한 코드가 있음
  data _ where
    _`×_ : (A B : U) → U
  El (A `× B) = El A × El B

-- 이제 중첩된 자연수 쌍 타입을 만들 수 있음
ty-example : U
ty-example = `Nat `× ((`Nat `× `Nat) `× `Nat)

-- 그리고 그 값들
val-example : El ty-example
val-example = 0 , ((1 , 2) , 3)

서로 다른 데이터 타입에 대한 생성자를 data _ where 블록(이름 대신 밑줄)에서 혼합할 수 있어요.

교차 상호 블록은 아래 설명할 전방 선언 블록으로 desugar되는데, 그 과정은:

  • 시그니처를 제자리에 두고,
  • 함수에 대한 절들을 그 중 첫 번째 것과 함께 그룹화하고,
  • 데이터 타입에 대한 생성자들을 그 중 첫 번째 것과 함께 그룹화해요.

전방 선언 (Forward declaration)

상호 재귀 함수는 모든 상호 재귀 함수의 타입 시그니처를 그 정의 앞에 배치해 작성할 수 있어요. mutual 블록의 범위는 Agda가 자동으로 추론해요:

f : A
g : B[f]
f = a[f, g]
g = b[f, g].

모듈과 postulate 같은 임의의 선언을 상호 재귀 정의와 혼합할 수 있어요. 데이터 타입과 레코드에 대해 다음 문법이 선언과 정의를 분리하는 데 사용돼요:

-- 선언.
data Vec (A : Set) : Nat → Set  -- 'where'가 없음에 주의

-- 정의.
data Vec A where                -- 타입 시그니처가 없음에 주의
  []   : Vec A zero
  _::_ : {n : Nat} → A → Vec A n → Vec A (suc n)

-- 선언.
record Sigma (A : Set) (B : A → Set) : Set

-- 정의.
record Sigma A B where
  constructor _,_
  field fst : A
        snd : B fst

데이터 또는 레코드 선언의 두 번째 부분의 매개변수 목록은 변수 왼쪽 변처럼 동작해요 (infix 문법은 지원되지 않지만). 즉, 타입 시그니처가 없어야 하고, 암시적 매개변수를 생략하거나 이름으로 바인딩할 수 있어요.

이런 선언과 정의의 분리는 예를 들어 타입 코드 집합과 그것들의 실제 타입으로의 해석(소위 유니버스)을 정의할 때 필요해요:

-- 선언.
data TypeCode : Set
Interpretation : TypeCode → Set

-- 정의.
data TypeCode where
  nat : TypeCode
  pi  : (a : TypeCode) (b : Interpretation a → TypeCode) → TypeCode

Interpretation nat      = Nat
Interpretation (pi a b) = (x : Interpretation a) → Interpretation (b x)

참고: 교차 상호 블록과 달리 전방 선언 스타일에서는 데이터 타입당 data ... where 블록이 하나만 있을 수 있어요.

분리된 선언/정의를 private 또는 abstract로 만들 때는 private 키워드를 선언에, abstract 키워드를 정의에 붙여야 해요. 예를 들어 private하고 abstract한 함수는 다음과 같이 정의할 수 있어요:

private
  f : A
abstract
  f = e

옛 스타일의 mutual 블록 (Old-style mutual blocks)

상호 재귀 함수는 모든 상호 재귀 함수의 타입 시그니처를 그 정의 앞에 배치해 작성할 수 있어요:

mutual
  f : A
  f = a[f, g]

  g : B[f]
  g = b[f, g]

mutual 키워드를 사용하면 위의 유니버스 예제는 다음과 같이 표현돼요:

mutual
  data TypeCode : Set where
    nat : TypeCode
    pi  : (a : TypeCode) (b : Interpretation a → TypeCode) → TypeCode

  Interpretation : TypeCode → Set
  Interpretation nat      = Nat
  Interpretation (pi a b) = (x : Interpretation a) → Interpretation (b x)

이 대체 문법은 mutual 블록의 내용을 선언부와 정의부로 정렬하고 선언을 정의 앞에 배치함으로써 새로운 문법으로 desugar돼요.

선언은 다음을 포함해요:

  • 함수의 타입 시그니처, 데이터 및 레코드 선언, unquoteDecl. (함수는 여기서 postulate와 primitive 등도 포함해요.)
  • 모듈 별칭, import, open 문 같은 모듈 문장.
  • 영향을 주는 대상의 이름만 필요하고 정의는 필요하지 않은 프래그마 (예: INJECTIVE).

정의는 다음을 포함해요:

  • 함수 절, 데이터 생성자 및 레코드 정의, unquoteDef.
  • 패턴 동의어 정의.
  • 정의가 필요한 프래그마, 예: INLINE, REWRITE 등.
  • 타입 체킹에 필요하지 않은 프래그마, 예: 컴파일러 프래그마.

module ... where가 있는 모듈 정의는 옛 스타일의 mutual 블록에서 지원되지 않아요.

더 알아보기 (Learn more)