레코드 타입

레코드 타입 (Record Types)

• 예제: Pair 타입 생성자 (Example: the Pair type constructor)
• 레코드 선언·구성·분해 (Declaring, constructing and decomposing records)
• 레코드 갱신 (Record update)
• 레코드 모듈 (Record modules)
• Eta-확장 (Eta-expansion)
• 재귀 레코드 (Recursive records)
• 레코드와 인스턴스 탐색 (Records and instance search)

레코드는 값을 함께 그룹화하기 위한 타입이에요. 그것들은 이름 붙은 필드와 (선택적) 추가 구성요소를 제공함으로써 의존 곱 타입을 일반화해요.

예제: Pair 타입 생성자 (Example: the Pair type constructor)

레코드 타입은 record 키워드로 선언할 수 있어요:

record Pair (A B : Set) : Set where
  field
    fst : A
    snd : B

이것은 새 타입 생성자 Pair : Set → Set → Set과 두 개의 투영 함수를 정의해요:

Pair.fst : {A B : Set} → Pair A B → A
Pair.snd : {A B : Set} → Pair A B → B

참고: 매개변수 A와 B는 투영 함수의 암시 인자예요.

test-fst : {A B : Set} → Pair A B → A
test-fst p = Pair.fst p

test-snd : {A B : Set} → Pair A B → B
test-snd p = Pair.snd p

투영 앞에 레코드 타입의 이름을 붙일 필요가 없도록 레코드 타입을 열 수 있어요 (레코드 모듈 참고):

open Pair

test-fst' : {A B : Set} → Pair A B → A
test-fst' p = fst p

test-snd' : {A B : Set} → Pair A B → B
test-snd' p = snd p

레코드 타입의 원소는 레코드 표현식으로 정의할 수 있는데, 여기서 결합은 단순한 키 = 값 쌍이에요:

p23 : Pair Nat Nat
p23 = record { fst = 2; snd = 3 }

레코드 where 표현식을 사용해, 결합을 let 바인딩처럼 취급할 수 있어요 (이전 바인딩을 참조하거나 매개변수화될 수 있음). 레코드 where 표현식의 필드는 also 모듈에서 상속될 수 있는데, using 또는 renaming 절에서 필드가 되어야 할 모든 바인딩을 언급함으로써 이루어져요.

p23' : Pair Nat Nat
p23' = record where
   -- 'fst' 바인딩을 'snd' 필드로 사용:
   open Pair p23 using () renaming (fst to snd)
   fst = 2

또는 코패턴(copatterns)을 사용해. 코패턴은 접두 형태로 사용될 수 있어요:

p34 : Pair Nat Nat
Pair.fst p34 = 3
Pair.snd p34 = 4

또는 접미 형태로 (이 경우 점을 앞에 붙여 씀):

p56 : Pair Nat Nat
p56 .Pair.fst = 5
p56 .Pair.snd = 6

또는 패턴 람다를 사용해 (이 경우 코패턴의 접미 형태만 사용할 수 있음):

p78 : Pair Nat Nat
p78 = λ where
  .Pair.fst → 7
  .Pair.snd → 8

constructor 키워드를 사용하면 이름 붙은 생성자로 레코드 타입의 원소를 정의할 수도 있어요:

record Pair (A B : Set) : Set where
  constructor _,_
  field
    fst : A
    snd : B

p45 : Pair Nat Nat
p45 = 4 , 5

constructor 키워드를 사용하지 않았더라도, Record.constructor 문법을 사용해 레코드의 내부-생성자를 이름으로 참조하는 것이 여전히 가능해요; 이 문법의 자세한 내용은 익명 생성자를 가진 레코드(Records with anonymous constructors)를 참고하세요.

record Anon (A B : Set) : Set where
  field
    fst : A
    snd : B

a45 : Anon Nat Nat
a45 = Anon.constructor 4 5

이런 의미에서 레코드 타입은 단일 생성자 데이터 타입과 크게 동작해요 (하지만 아래 Eta-확장 참고).

레코드 선언·구성·분해 (Declaring, constructing and decomposing records)

레코드 타입 선언하기 (Declaring record types)

레코드 선언의 일반적인 형태는 다음과 같아요:

record <recordname> <parameters> : Set <level> where
  <directives>
  constructor <constructorname>
  field
    <fieldname1> : <type1>
    <fieldname2> : <type2>
    -- ...
  <declarations>

모든 구성요소는 선택적이며 어떤 순서로든 주어질 수 있어요. 특히 필드는 둘 이상의 블록에서 다른 선언과 섞여 주어질 수 있어요. 각 필드는 레코드의 구성요소예요. 이후 필드의 타입은 이전 필드에 의존할 수 있어요.

사용 가능한 지시어(directive)는 eta-equality, no-eta-equality, pattern(Eta-확장 참고), inductive와 coinductive(재귀 레코드 참고)예요.

레코드 값 구성하기 (Constructing record values)

레코드 값은 각 레코드 필드에 대한 값을 주어 구성돼요:

record { <fieldname1> = <term1> ; <fieldname2> = <term2> ; ... }

여기서 항의 타입은 필드의 타입과 일치해야 해요. 레코드에 생성자 <constructorname>이 선언되어 있으면 이것은 also 이렇게 쓸 수 있어요:

<constructorname> <term1> <term2> ...

이름 붙은 정의에 대해 이것은 also 코패턴으로 표현될 수 있어요:

<named-def> : <recordname> <parameters>
<recordname>.<fieldname1> <named-def> = <term1>
<recordname>.<fieldname2> <named-def> = <term2>
...

레코드는 다른 레코드를 갱신하여 구성될 수도 있어요.

모듈에서 레코드 구성하기 (Building records from modules)

record { <fields> } 문법은 also 모듈 이름을 받아들여요. 필드는 주어진 모듈의 대응하는 정의를 사용해 정의돼요. 예를 들어 이 레코드 타입 R과 모듈 M을 가정하면:

record R : Set where
  field
    x : X
    y : Y
    z : Z

module M where
   x = ...
   y = ...

r : R
r = record { M; z = ... }

이 구성은 명시적 필드 정의와 적용된 모듈의 임의의 조합을 지원해요. 필드가 명시적으로 주어지고 모듈 중 하나에서도 사용 가능하면 명시적인 것이 우선해요. 필드가 둘 이상의 모듈에서 사용 가능하면 그것은 모호해서 거부돼요. 결과적으로 할당의 순서는 중요하지 않아요.

모듈은 both 인자에 적용될 수 있고 hiding, using, renaming같은 import 지시어를 가질 수 있어요. 위 예제를 바탕으로 한 인위적인 예는 다음과 같아요:

module M2 (a : A) where
  w = ...
  z = ...

r2 : A → R
r2 a = record { M hiding (y); M2 a renaming (w to y) }

익명 생성자를 가진 레코드 (Records with anonymous constructors)

레코드가 이름 붙은 생성자 지시어로 정의되지 않았더라도, Agda는 여전히 레코드에 대한 생성자를 내부적으로 생성해요. 이 이름은 record{} 문법을 구현하는 데 내부적으로 사용되지만, 반영(Reflection)을 사용해 여전히 얻을 수 있어요. Agda 2.8.0부터 표면 문법에서도 이 이름을 참조하는 것이 가능해요:

_ : Name
_ = quote Anon.constructor

이 문법은 이름이 사용될 수 있는 곳이면 어디서나 사용될 수 있고, 생성자에 이름이 붙은 것처럼 정확히 동작해요.

{-# INLINE Anon.constructor #-}

기술적으로 constructor는 레코드 모듈 Anon에 바인딩된 이름이에요. 하지만 constructor는 키워드이므로 한정되지 않은 이름으로 쓸 수 없어요: constructor라는 함수를 선언하는 것은 불가능하고, 레코드 모듈을 열어도 생성자를 constructor로 접근할 수 없으며, 유사-이름은 using, hiding, renaming 지시어에 나열될 수 없어요 (그것을 하려는 것은 구문 오류).

constructor는 단지 별명(alias)이라는 점도 유의하세요. 투영과 달리 레코드 생성자 자체는 레코드 모듈의 정의가 아니에요: 그것은 레코드 타입의 원소를 인자로 받지 않아요. 모듈 적용이 그것이 인스턴스화하는 모듈의 정의를 복사하므로, module M = Anon 후에는 M.constructor가 사용 가능하지 않아요.

레코드의 생성자는 레코드 모듈 자체가 스코프에 있을 때마다 참조될 수 있어요. 레코드가 추상(abstract, 추상 정의 참고)이면 생성자를 참조하는 것은 여전히 오류라는 점에 유의하세요:

module _ where private
  record R : Set where

abstract record S : Set where

_ = R.constructor
-- Name not in scope: R.constructor

_ = S.constructor
-- Constructor S.constructor is abstract, thus, not in scope here

레코드 값 분해하기 (Decomposing record values)

필드 이름으로 레코드 값에서 대응하는 구성요소를 투영할 수 있어요. 투영은 함수처럼 접두 표기로, 또는 필드 이름에 점을 추가해 접미 표기로 사용될 수 있어요:

sum-prefix : Pair Nat Nat → Nat
sum-prefix p = Pair.fst p + Pair.snd p

sum-postfix : Pair Nat Nat → Nat
sum-postfix p = p .Pair.fst + p .Pair.snd

귀납적 레코드에 패턴 매칭하는 것도 가능해요:

sum-match : Pair Nat Nat → Nat
sum-match (x , y) = x + y

또는 let 바인딩 레코드 패턴을 사용해:

sum-let : Pair Nat Nat → Nat
sum-let p = let (x , y) = p in x + y

Agda 2.9.0부터 후자는 eta-동등성이 있는 레코드(예: Pair)를 요구하는데, 그렇지 않으면 ShouldBeEtaRecordPattern 경고가 발생해요.

참고: 레코드 값에 대한 패턴 매칭을 활성화하기 위해 생성자 이름을 붙일 필요는 없어요. 레코드 표현식이 패턴으로 나타날 수 있어요.

sum-record-match : Pair Nat Nat → Nat
sum-record-match record { fst = x ; snd = y } = x + y

레코드 갱신 (Record update)

레코드 타입과 대응하는 값이 있다고 가정해 봐요:

record MyRecord : Set where
  field
    a b c : Nat

old : MyRecord
old = record { a = 1; b = 2; c = 3 }

그런 다음 레코드 값의 (일부) 필드를 다음 방식으로 갱신할 수 있어요:

new : MyRecord
new = record old { a = 0; c = 5 }

또는 record where 문법을 사용해:

new₁ : MyRecord
new₁ = record old where
  a = 0
  c = 5

여기서 new는 record { a = 0; b = 2; c = 5 }로 정규화돼요. old 대신 타입 MyRecord의 값을 산출하는 어떤 표현식이든 사용될 수 있어요. 레코드가 모듈 이름으로 구성될 수 있고 모든 레코드가 모듈을 정의한다는 사실을 함께 사용하면, 이것은 also 이렇게 쓸 수 있어요:

new₂ : MyRecord
new₂  = record { MyRecord old; a = 0; c = 5}

레코드 갱신은 타입을 바꿀 수 없어요: 결과 값은 레코드 매개변수를 포함해 원본과 같은 타입을 가져야 해요. 따라서 원본 레코드의 타입이 추론될 수 있으면 레코드 갱신의 타입도 추론될 수 있어요.

레코드 갱신 문법은 타입 체킹 전에 확장돼요. 표현식

record old { upd-fields }

이 레코드 타입 R에 대해 검사될 때, 다음과 같이 확장돼요:

let r = old in record { new-fields }

여기서 old는 타입 R을 가져야 하며 new-fields는 다음과 같이 정의돼요: R의 각 필드 x에 대해, x = e가 upd-fields에 포함되어 있으면 x = e가 new-fields에 포함되고, 그렇지 않으면 x가 명시적 필드이면 x = R.x r이 new-fields에 포함되며, x가 암시적 또는 슈퍼클래스 필드이면 new-fields에서 생략돼요.

암시적 및 슈퍼클래스 필드를 특별히 취급하는 이유는 다음과 같은 코드를 허용하기 위해서예요:

data Vec (A : Set) : Nat → Set where
  [] : Vec A zero
  _∷_ : ∀{n} → A → Vec A n → Vec A (suc n)

record VList : Set where
  field
    {length} : Nat
    vec      : Vec Nat length
    -- 더 많은 필드 ...

xs : VList
xs = record { vec = 0 ∷ 1 ∷ 2 ∷ [] }

ys = record xs { vec = 0 ∷ [] }

특별한 취급 없이는 마지막 표현식에 length에 대한 새 바인딩(예: length = _)을 포함해야 했을 거예요.

레코드 모듈 (Record modules)

새 타입과 함께 레코드 선언은 같은 이름의, 레코드 타입의 원소에 대해 매개변수화된 투영 함수를 포함하는 모듈도 정의해요. 이것은 레코드가 "열려(open)"지고 필드가 스코프로 들어오게 해요. 예를 들어:

swap : {A B : Set} → Pair A B → Pair B A
swap p = snd , fst
  where open Pair p

예제에서 레코드 모듈 Pair는 다음과 같은 형태를 가져요:

module Pair {A B : Set} (p : Pair A B) where
  fst : A
  snd : B

참고: 이것은 정확히 맞지는 않아요: 투영 함수는 매개변수를 소거된 인자로 받아요. 하지만 매개변수가 원래 소거되지 않았다면 모듈 텔레스코프에서 소거되지 않아요.

레코드 선언 안에 정의함으로써 레코드 모듈에 임의의 정의를 추가하는 것이 가능해요:

record Functor (F : Set → Set) : Set₁ where
  field
    fmap : ∀ {A B} → (A → B) → F A → F B

  _<$_ : ∀ {A B} → A → F B → F A
  x <$ fb = fmap (λ _ → x) fb

참고: 일반적으로 새 정의는 필드 선언 뒤에 나타나야 하지만, 패턴 매칭이 없는 간단한 비-재귀 함수 정의는 필드와 섞일 수 있어요. 이 제한의 이유는 레코드 생성자의 타입이 let-표현식으로 표현 가능해야 하기 때문이에요. 아래 예제에서 D₁은 생성된 mkR의 타입이 잘 형성되는 선언만 포함할 수 있어요.

record R Γ : Setᵢ where
  constructor mkR
  field f₁ : A₁
  D₁
  field f₂ : A₂

mkR : ∀ {Γ} (f₁ : A₁) (let D₁) (f₂ : A₂) → R Γ

Eta-확장 (Eta-expansion)

레코드 타입의 eta(η) 규칙은

record R : Set where
   field
     a : A
     b : B
     c : C

모든 x : R이 record { a = R.a x ; b = R.b x ; c = R.c x }와 정의적으로 같다고 말해요.

eta-R : (x : R) → x ≡ record { a = R.a x ; b = R.b x ; c = R.c x }
eta-R r = refl

레코드 타입은 기본적으로(옵션: --eta-equality) 공유도(coinductive) 레코드를 제외하고 η-동등성을 누려요.

eta-equality/no-eta-equality 키워드는 선언되는 레코드 타입에 대해 η 규칙을 활성화/비활성화해요.

record R-noeta : Set where
  no-eta-equality
  field
    a : A
    b : B
    c : C

재귀 레코드 (Recursive records)

재귀 레코드는 레코드 타입 자체가 그 필드 중 하나의 타입에 나타나는 레코드예요. 재귀 레코드는 inductive 또는 coinductive 중 하나로 선언되어야 해요.

귀납적 레코드 (Inductive records)

귀납적 레코드는 유한 깊이의 값만 허용하는 재귀 레코드예요.

record Tree (A : Set) : Set where
  inductive
  constructor tree
  field
    elem     : A
    subtrees : List (Tree A)

open Tree

귀납적 레코드 타입(재귀 레코드 참고)은 기본적으로(--no-eta-equality가 주어지지 않는 한) η-동등성이 활성화돼요. (비-방어(unguarded) 레코드는 no-eta-equality로 주석을 달아야 해요. 비-방어 레코드 섹션 참고.)

eta-Tree : {A : Set} (t : Tree A) → t ≡ tree (elem t) (subtrees t)
eta-Tree t = refl

η-동등성이 있는 귀납적 레코드에 패턴 매칭하고 재귀하는 것이 가능해요:

map-Tree : {A B : Set} → (A → B) → Tree A → Tree B
map-Tree {A} {B} f (tree x ts) = tree (f x) (map-subtrees ts)
  where
    map-subtrees : List (Tree A) → List (Tree B)
    map-subtrees [] = []
    map-subtrees (t ∷ ts) = map-Tree f t ∷ map-subtrees ts

η-동등성이 없는 귀납적 레코드 타입에 대해 패턴 매칭은 기본적으로 허용되지 않아요. 패턴 매칭은 pattern 지시어를 사용해 수동으로 켤 수 있어요:

record HereditaryList : Set where
  inductive
  no-eta-equality
  pattern
  field sublists : List HereditaryList

pred : HereditaryList → List HereditaryList
pred record{ sublists = ts } = ts

레코드 타입에 eta-equality와 pattern 둘 다 주어지면, Agda는 UselessPatternDeclarationForRecord 경고로 중복 pattern 지시어를 사용자에게 알려요.

참고: 패턴 매칭이 활성화된 귀납적 레코드 타입의 값을 정의하는 데 코패턴 매칭을 사용하는 것은 허용되지 않아요. 이 조합은 정준성(canonicity)의 손실 또는 주체 축약의 손실 중 하나로 이어져요. 예를 들어 다음 정의를 생각해 봐요:

record Rec : Set where
  constructor con
  no-eta-equality
  pattern
  field
    f : Nat
open Rec

eta : (r : Rec) → r ≡ con (f r)
eta (con n) = refl

bar : Rec
f bar = 0

이 코드가 허용되면 eta bar는 타입 bar ≡ con 0의 닫힌 항이에요. 이제 eta bar는 refl : bar ≡ con 0로 축약되거나(no-eta-equality 지시어와 모순) 또는 eta bar는 걸린 항이에요(정준성 깨짐).

비-방어 레코드 (Unguarded records)

η-동등성은 무한 η-확장으로 이어질 수 있으므로 재귀 레코드에 항상 안전하지 않아요. 이것은 재귀 발생이 η가 없는(그래서 무한 확장을 멈추는) 타입 형성자에 의해 방어(guard)되지 않는 소위 비-방어(unguarded) 레코드의 경우예요. η-동등성은 그러한 레코드에 대해 꺼져 있어야 해요:

record Empty : Set where
  inductive
  no-eta-equality; pattern
  field emp : Empty

isReallyEmpty : Empty → {A : Set} → A
isReallyEmpty record{ emp = x } = isReallyEmpty x

Agda는 η가 있는 비-방어 레코드를 지적하는데, UnguardedEtaRecord 경고 참고. Agda의 비-방어 레코드 탐지는 완벽하지 않으므로, 어떤 경우에는 Agda의 경고에도 불구하고 η를 갖는 것이 안전해요. 그러한 경우 레코드 선언 앞에 ETA_EQUALITY 프래그마를 붙여 경고를 조용히 만들 수 있어요.

mutual
  {-# ETA_EQUALITY #-}
  record NonEmptyTuple (A : Set) (n : Nat) : Set where
    inductive; eta-equality
    field theTuple : FTuple A n

  FTuple : (A : Set) (n : Nat) → Set
  FTuple A zero    = A
  FTuple A (suc n) = Pair A (NonEmptyTuple A n)

nonEmptyTupleEta : {A : Set} {n : Nat} (t : NonEmptyTuple A n)
  → t ≡ record { theTuple = NonEmptyTuple.theTuple t }
nonEmptyTupleEta t = refl

공유도 레코드 (Coinductive records)

공유도 레코드는 (아마) 무한 깊이의 값을 허용하는 재귀 레코드예요.

record Stream (A : Set) : Set where
  coinductive
  constructor _::_
  field
    head : A
    tail : Stream A

open Stream

공유도 레코드의 값은 코패턴으로 정의할 수 있어요:

natsFrom : Nat → Stream Nat
head (natsFrom n) = n
tail (natsFrom n) = natsFrom (suc n)

코패턴 매칭을 지원하는 레코드의 생성자는 {-# INLINE #-} 프래그마로 표시될 수 있어요. 이것은 생성자의 사용을 해당하는 코패턴 정의로 자동 변환하는데, 종료 검사기를 돕는 데 유용할 수 있어요.

공유도 레코드에 대한 eta 동등성은 허용되지 않아요. 이 조합은 Agda가 쉽게 루프하게 만들 수 있기 때문이에요. 이것은 자신의 책임 하에 ETA_EQUALITY를 사용해 재정의될 수 있어요. 공유도 레코드에 대한 패턴 매칭도 마찬가지로 허용되지 않아요.

공유도 레코드에 대해 더 읽으려면 공유도(coinduction) 섹션을 참고하세요.

레코드와 인스턴스 탐색 (Records and instance search)

레코드 타입의 필드는 두 가지 직교하는 방식으로 인스턴스 탐색 메커니즘과 상호작용할 수 있어요.

레코드 필드는 그 이름을 이중 중괄호 {{ }}로 감싸 인스턴스 가시성을 줄 수 있어요. 구분을 위해 인스턴스 가시성을 가진 레코드 필드를 슈퍼클래스 필드(superclass fields)라고 불러요. 슈퍼클래스 필드는 레코드 생성자의 인스턴스 인자예요. 이것은 그것들이 종종 생략될 수 있음을 의미해요.

필드 선언 자체는 인스턴스 블록에 중첩될 수 있어요. 우리는 이것들을 (갖는 것) 인스턴스 투영(instance projections)이라고 불러요. 레코드 필드를 인스턴스 투영으로 만드는 것은 그것이 바인딩되는 가시성을 바꾸지 않아서, 추가로 슈퍼클래스 필드(또는 레코드 생성자의 숨은 인자)로 만들지 않는 한 레코드 값을 구성할 때 명시적으로 지정되어야 해요.

주어진 레코드 필드는 인스턴스 투영과 슈퍼클래스 필드 둘 다로 만들어질 수 있어요. 그러면 그것은 다음 섹션에서 설명된 두 동작 모두에 적용돼요:

record Ex2 (A : Set) : Set where
  field
    instance ⦃ both ⦄ : Ex1 A

슈퍼클래스 필드와 인스턴스 투영 둘 다 레코드 선언에서 여러 번, 그리고 필드 목록의 어떤 위치에서도 나타날 수 있어요.

슈퍼클래스 필드 (Superclass fields)

이름이 암시하듯이 슈퍼클래스 필드는 과(superclass) 관계(하스켈 의미에서)를 모델링하는 데 사용돼요. 예를 들어 Ord 값이 Eq 타입의 슈퍼클래스 필드를 가지도록 레코드 타입 쌍을 정의함으로써, Eq 클래스를 "확장"하는 Ord 클래스를 정의할 수 있어요:

record Eq (A : Set) : Set where
  field
    _==_ : A → A → Bool

open Eq ⦃ ... ⦄

record Ord (A : Set) : Set where
  field
    _<_     : A → A → Bool
    ⦃ eqA ⦄ : Eq A

open Ord ⦃ ... ⦄ hiding (eqA)

Ord가 eta 레코드인 한, 타입 Ord A의 로컬 인스턴스 변수는 Eq A 인스턴스도 스코프로 가져와요. 예를 들어 Ord A 인스턴스 인자를 취하는 함수는 Eq 인스턴스도 사용할 수 있어요:

_≤_ : {A : Set} ⦃ ordA : Ord A ⦄ → A → A → Bool
x ≤ y = (x == y) || (x < y)

슈퍼클래스 필드는 "하위클래스" 변수가 인스턴스로 스코프에 있을 때만 스코프로 가져와져요. 다음은 동작하지 않아요:

weird : {A : Set} (ordA : Ord A) → A → A → Bool
weird _ = x == y

하지만 슈퍼클래스 필드는 생성자의 인스턴스 인자이므로, 레코드 값에 매칭하여 수동으로 스코프로 가져올 수 있어요. 레코드 값이 비-인스턴스 가시성을 가졌다면, 패턴 매칭 후에도 하위클래스는 인스턴스 탐색에 사용할 수 없다는 점을 명심하세요:

works : {A : Set} (ordA : Ord A) → A → A → Bool
works record{} x y = x == y
-- record{}에 매칭하면 모든 필드가 로컬 변수가 됨, 슈퍼클래스 필드 포함.

fails : {A : Set} (ordA : Ord A) → A → A → Bool
fails record{} x y = x ≤ y
-- 타입 Ord A의 인스턴스가 스코프에서 발견되지 않음.
-- Ord 인자가 가시적이므로 인스턴스 탐색이 완전히 무시함.

경고: 슈퍼클래스 필드는 로컬 인스턴스 변수를 확장하여 로컬 인스턴스 테이블로 가져와져요. 이것은 대응하는 슈퍼클래스가 도출 가능하더라도 Agda가 하위클래스의 인스턴스를 찾는 데 실패할 수 있음을 의미해요. 예를 들어, 스코프에 대응하는 인스턴스가 없더라도 Ord 인스턴스를 구성할 때 eqA 필드를 명시적으로 제공할 수 있어요:

instance
  OrdNat : Ord Nat
  OrdNat = record
    { _<_ = Agda.Builtin.Nat._<_
    ; eqA = record { _==_ = Agda.Builtin.Nat._==_ }
    -- 전역 Eq Nat 인스턴스 없음!
    }

그러면 Eq Nat 인스턴스를 탐색하는 시도는 실패할 거예요. 슈퍼클래스 필드 확장은 인스턴스 가시성을 가진 로컬 변수에만 적용되고, 최상위 인스턴스 선언에는 적용되지 않기 때문이에요.

fails : Bool
fails = 1 == 2
-- 타입 Eq Nat의 인스턴스가 스코프에서 발견되지 않음.

슈퍼클래스 필드를 찾기 위해 인스턴스 변수를 eta-확장하는 것은 바인더 아래에서도 동작해요. 이것은 하위클래스 인스턴스의 족(family)이 대응하는 슈퍼클래스의 족으로 확장된다는 뜻이에요:

fam
  : {Ix : Set} {F : Ix → Set} ⦃ ords : ∀ {i} → Ord (F i) ⦄
  → (ix : Ix) → F ix → F ix → Bool
fam ix x y = x == y

슈퍼클래스 필드의 타입 자체가 슈퍼클래스 필드를 가진 레코드 타입이면, 그것은 재귀적으로 확장돼요:

data ORD : Set where
  lt le eq : ORD

record Cmp (A : Set) : Set where
  field
    ⦃ ordA ⦄ : Ord A
    compare  : A → A → ORD

cmp→eq : {A : Set} ⦃ ordA : Cmp A ⦄ → A → A → Bool
cmp→eq x y = x == y

슈퍼클래스 필드는 이후 필드들의 타입에서, 그리고 레코드 안에 중첩된 어떤 선언의 타입에서 로컬 인스턴스로 스코프에 있어요:

record Bounded (A : Set) : Set where
  field
    ⦃ cmpA ⦄ : Cmp A
    lo hi    : A

  -- 필드 *사이의* 선언:
  ordered : Bool
  ordered = lo < hi

  field in-order : ordered ≡ true

  -- 필드 *뒤의* 선언:
  is-empty : Bool
  is-empty = lo == hi

레코드 안의 어떤 이후 선언도 인스턴스 탐색을 통해 그 슈퍼클래스 필드에 의존할 수 있고, 이 필드들은 슈퍼클래스 확장에 사용할 수 있어요.

경고: 레코드 모듈을 열어도(심지어 로컬로도) 슈퍼클래스 필드가 로컬 인스턴스가 되지는 않아요. 모듈 적용에 의해 스코프로 가져와지는 것은 인스턴스 투영뿐이에요.

fails : {A : Set} (ordA : Ord A) → A → A → Bool
fails ord x y = let open Ord ord in x == y
-- 스코프에 Eq A 인스턴스 없음. 슈퍼클래스 필드 eqA는 인스턴스 투영이 없기 때문.

겹치는 슈퍼클래스 필드 (Overlapping superclass fields)

여러 하위클래스가 같은 클래스에서 "상속"할 때, 슈퍼클래스 필드 확장은 각 하위클래스를 확장하여 슈퍼클래스에 대한 구별되는 후보를 만들 거예요. 이 상황에서 인스턴스 탐색은 해결되지 않은 중복으로 실패할 거예요.

이것은 관련된 모든 슈퍼클래스 필드를 overlap 키워드로 표시하면 해결될 수 있어요. 예를 들어 Ord가 그 Eq 슈퍼클래스 필드도 overlap으로 표시되도록 재정의된다면, Eq를 also "확장"하는 Num 클래스를 정의할 수 있어요:

record Ord (A : Set) : Set where
  field
    _<_     : A → A → Bool
    overlap ⦃ eqA ⦄ : Eq A

record Num (A : Set) : Set where
  field
    fromNat         : Nat → A
    overlap ⦃ eqA ⦄ : Eq A

open Ord ⦃ ... ⦄ hiding (eqA)
open Num ⦃ ... ⦄ hiding (eqA)

이제 Num과 Ord 인스턴스를 둘 다 취하는 함수를 정의할 수 있어요:

_≤3 : {A : Set} ⦃ ordA : Ord A ⦄ ⦃ numA : Num A ⦄ → A → Bool
x ≤3 = (x == fromNat 3) || (x < fromNat 3)

인스턴스 제약에 대한 모든 가능한 후보가 overlap으로 표시된 슈퍼클래스 필드에서 생기면, 인스턴스 탐색은 가장 왼쪽 레코드 값에서 생기는 필드를 선택할 거예요. 위 함수에서 그것은 Ord 인자에서 오는 후보예요:

_
  : {A : Set} ⦃ ordA : Ord A ⦄ ⦃ numA : Num A ⦄ {arg : A}
  → (arg ≤3) ≡ ((_==_ ⦃ Ord.eqA ordA ⦄ arg (fromNat 3)) || _)
_ = refl

겹치는 후보가 재귀적 슈퍼클래스 확장에 의해 도입되면, 해결은 선언 순서의 더 이른 필드에서 생기는 것들을 선호할 거예요. '가는 길에' 확장된 후보들은 그들 자신이 overlap으로 표시될 필요는 없고; 이것으로 그들의 슈퍼클래스 필드에서 중복을 해결하기에 충분하지 않을 거예요.

record NumOrd (A : Set) : Set where
  field
    ⦃ numA ⦄ : Num A
    ⦃ ordA ⦄ : Ord A

_≤4 : {A : Set} ⦃ numordA : NumOrd A ⦄ → A → Bool
x ≤4 = (x == fromNat 4) || (x < fromNat 4)

여기서 Eq 인스턴스는 NumOrd 인자의 numA 필드에서 선택돼요:

_
  : {A : Set} ⦃ numordA : NumOrd A ⦄ {arg : A}
  → (arg ≤4) ≡ ((_==_ ⦃ numordA .numA .eqA ⦄ arg (fromNat 4)) || _)
_ = refl

슈퍼클래스 필드 생략하기 (Omitting superclass fields)

슈퍼클래스 필드는 생성자의 인스턴스 인자가 되므로, 생성자가 함수로 적용될 때, 레코드 표현식의 두 형태를 사용할 때, 그리고 레코드 값을 코패턴 매칭으로 정의할 때 생략될 수 있어요. 이 중 어떤 경우에든 빠진 필드는 인스턴스 탐색으로 채워질 거예요:

instance
  EqNat : Eq Nat
  EqNat ._==_ = Agda.Builtin.Nat._==_

ex1 ex2 ex3 : Ord Nat
ex1 ._<_ = Agda.Builtin.Nat._<_
ex2 = record { _<_ = Agda.Builtin.Nat._<_ }
ex3 = record where
  _<_ = Agda.Builtin.Nat._<_

인스턴스 투영 (Instance projections)

중첩된 인스턴스 블록에 정의된 레코드 필드는 투영 함수를 레코드 모듈에 중첩된 최상위 인스턴스 선언으로 만들어요. 그것은 레코드 생성자의 텔레스코프에서 필드의 가시성에는 영향을 주지 않아요:

record Eqtype : Set₁ where
  no-eta-equality -- (!)
  field
    carrier      : Set
    instance eqA : Eq carrier

open Eqtype renaming (carrier to [_])

선험적으로 이것은 인스턴스 테이블에 영향을 주지 않는데, 레코드 모듈 안의 정의는 레코드를 가시 인자로 취하기 때문이에요. 하지만 레코드 모듈이 인스턴스화되면, 결과 인스턴스화의 타입이 인스턴스에 대해 유효한 타입인 한, 투영은 인스턴스화된 타입에서 인스턴스로 사용 가능해질 거예요:

example : (T : Eqtype) → [ T ] → [ T ] → Bool
example T x y = let open Eqtype T in x == y

위 예제에서 let open Eqtype T 표현식에 의해 도입된 로컬 선언은 다음과 동등해요:

example' : (T : Eqtype) → [ T ] → [ T ] → Bool
example' T x y =
  let
    carrier = Eqtype.carrier T
    instance
      eqA : Eq carrier
      eqA = Eqtype.eqA T
  in x == y

참고: 인스턴스 투영은 레코드 모듈의 인스턴스화에 의해 스코프로 가져와지므로, 그것들이 no-eta-equality 레코드 타입에 속하더라도 동작해요.

인스턴스 투영은 레코드 모듈에서 최상위 인스턴스를 정의하는 것과 완전히 동등하므로, 레코드 모듈 적용에서 생기는 인스턴스들의 겹침 동작을 세밀하게 제어하기 위해 overlap 프래그마 중 하나로 주석을 달 수 있어요.

경고: 인스턴스 투영이 대응하는 최상위 투영을 갖는 것을 방지하는 모달리티(예: 비관련이고 --irrelevant-projections가 주어지지 않은 경우)를 가지면, 레코드 모듈을 인스턴스화해도 그것을 인스턴스로 스코프로 가져오지 않아요:

postulate
  Nonzero : Nat → Set
  _/_ : Nat → (div : Nat) ⦃ _ : Nonzero div ⦄ → Nat

record Pos : Set where
  field
    num : Nat
    instance .pos : Nonzero num

모듈 Pos를 열어 pos 필드를 인스턴스로 사용하려는 시도는 실패할 거예요.

fails : (x : Nat) (y : Pos) → Nat
fails x y = let open Pos y in x / num
-- 필드 'pos'는 투영이 없으므로:
-- 스코프에 타입 Nonzero num의 인스턴스가 발견되지 않음.

더 알아보기 (Learn more)

• Agda 문서: 레코드 타입 원문