9. 구조체와 레코드🔗

앞서 Lean의 기초 체계에 귀납적 타입이 포함되어 있음을 살펴보았습니다. 또한 타입 유니버스, 의존 화살표 타입, 귀납적 타입만을 기반으로 상당한 규모의 수학 체계를 구축할 수 있다는 것이 주목할 만한 사실이라는 점도 언급했습니다. 그 밖의 모든 것은 이들로부터 따라 나옵니다. Lean 표준 라이브러리에는 귀납적 타입의 사례가 많이 있으며(예: Nat, Prod, List), 논리 연결사조차 귀납적 타입을 사용하여 정의됩니다.

생성자가 하나뿐인 비재귀 귀납적 타입을 구조체 또는 레코드라고 부른다는 것을 떠올려 보십시오. 곱 타입은 구조체이며, 의존 곱(시그마) 타입도 마찬가지입니다. 일반적으로 구조체 S를 정의할 때에는 보통 S의 각 인스턴스를 “분해”하여 그 필드에 저장된 값을 꺼낼 수 있게 해 주는 투영 함수도 함께 정의합니다. 쌍의 첫 번째 원소와 두 번째 원소를 반환하는 함수 Prod.fst와 Prod.snd가 이러한 사영의 예입니다.

프로그램을 작성하거나 수학을 형식화할 때, 많은 필드를 포함하는 구조체를 정의하는 일은 드물지 않습니다. Lean에서 사용할 수 있는 structure 명령은 이 과정을 지원하는 기반을 제공합니다. 이 명령으로 구조체를 정의하면 Lean이 모든 사영 함수를 자동으로 생성합니다. structure 명령을 사용하면 이전에 정의한 구조체를 바탕으로 새로운 구조체를 정의할 수도 있습니다. 또한 Lean은 주어진 구조체의 인스턴스를 정의하기 위한 편리한 표기법을 제공합니다.

9.1. 구조체 선언하기🔗

structure 명령은 본질적으로 귀납적 데이터 타입을 정의하기 위한 “프런트엔드”입니다. 모든 structure 선언은 같은 이름의 네임스페이스를 도입합니다. 일반적인 형식은 다음과 같습니다:

    structure <name> <parameters> <parent-structures> where
      <constructor> :: <fields>

대부분의 부분은 선택 사항입니다. 다음은 예시입니다.

structure Point (α : Type u) where
  mk ::
  x : α
  y : α

Point 타입의 값은 Point.mk a b를 사용하여 생성하며, 점 p의 필드에는 Point.x p와 Point.y p를 사용하여 접근합니다(단, p.x와 p.y도 사용할 수 있습니다. 아래를 참고하십시오). structure 명령은 유용한 재귀자와 정리도 생성합니다. 다음은 위 선언에 대해 생성되는 구성물 중 일부입니다.

structure Point (α : Type u) where
  mk ::
  x : α
  y : α

-- a Type
Point.{u} (α : Type u) : Type u#check Point

Point.{u} (α : Type u) : Type u

-- the eliminator
@Point.rec : {α : Type u_2} →
  {motive : Point α → Sort u_1} → ((x y : α) → motive { x := x, y := y }) → (t : Point α) → motive t#check @Point.rec

@Point.rec : {α : Type u_2} →
  {motive : Point α → Sort u_1} → ((x y : α) → motive { x := x, y := y }) → (t : Point α) → motive t

-- the constructor
@Point.mk : {α : Type u_1} → α → α → Point α#check @Point.mk

@Point.mk : {α : Type u_1} → α → α → Point α

-- a projection
@Point.x : {α : Type u_1} → Point α → α#check @Point.x

@Point.x : {α : Type u_1} → Point α → α

-- a projection
@Point.y : {α : Type u_1} → Point α → α#check @Point.y

@Point.y : {α : Type u_1} → Point α → α

생성자 이름을 지정하지 않으면 생성자의 이름은 기본적으로 mk가 됩니다.

다음은 생성된 구성 요소를 사용하는 간단한 정리와 표현식의 예입니다. 평소와 같이 open Point 명령을 사용하면 Point 접두사를 생략할 수 있습니다.

structure Point (α : Type u) where
  x : α
  y : α

10#eval Point.x (Point.mk 10 20)

20#eval Point.y (Point.mk 10 20)

open Point

example (a b : α) : x (mk a b) = a :=
  rfl

example (a b : α) : y (mk a b) = b :=
  rfl

p : Point Nat가 주어졌을 때, 점 표기법 p.x는 Point.x p의 축약형입니다. 이를 통해 구조체의 필드에 편리하게 접근할 수 있습니다.

structure Point (α : Type u) where
 x : α
 y : α

def p := Point.mk 10 20

p.x : Nat#check p.x

p.x : Nat

10#eval p.x

20#eval p.y

점 표기법은 레코드의 사영에 접근할 때뿐만 아니라, 같은 이름의 네임스페이스에 정의된 함수를 적용할 때에도 편리합니다. 논리곱 절에서 보았듯이, p의 타입이 Point이면, foo의 첫 번째 비암시적 인자의 타입이 Point라고 가정할 때 표현식 p.foo는 Point.foo p로 해석됩니다. 따라서 아래 예제에서 표현식 p.add q는 Point.add p q의 축약형입니다.

structure Point (α : Type u) where
  x : α
  y : α
deriving Repr

def Point.add (p q : Point Nat) :=
  mk (p.x + q.x) (p.y + q.y)

def p : Point Nat := Point.mk 1 2

def q : Point Nat := Point.mk 3 4

{ x := 4, y := 6 }#eval p.add q

{ x := 4, y := 6 }

다음 장에서는 α에 연관된 덧셈 연산이 있다고 가정할 때, add와 같은 함수가 Point Nat뿐만 아니라 Point α의 원소에 대해서도 일반적으로 작동하도록 정의하는 방법을 배우게 됩니다.

더 일반적으로, p : Point일 때 표현식 p.foo x y z가 주어지면, Lean은 Point.foo의 인수 중 타입이 Point인 첫 번째 인수 자리에 p를 삽입합니다. 예를 들어, 아래의 스칼라 곱 정의에서 p.smul 3은 Point.smul 3 p로 해석됩니다.

structure Point (α : Type u) where
 x : α
 y : α
 deriving Repr

def Point.smul (n : Nat) (p : Point Nat) :=
  Point.mk (n * p.x) (n * p.y)

def p : Point Nat := Point.mk 1 2

{ x := 3, y := 6 }#eval p.smul 3

{ x := 3, y := 6 }

example {p : Point Nat} : p.smul 3 = Point.smul 3 p := rfl

두 번째 비암시적 인자로 리스트를 받는 List.map 함수에도 비슷한 기법을 흔히 사용합니다:

@List.map : {α : Type u_1} → {β : Type u_2} → (α → β) → List α → List β#check @List.map

@List.map : {α : Type u_1} → {β : Type u_2} → (α → β) → List α → List β

def xs : List Nat := [1, 2, 3]

def f : Nat → Nat := fun x => x * x

[1, 4, 9]#eval xs.map f

[1, 4, 9]

example {xs : List α} {f : α → β} :
    xs.map f = List.map f xs :=
  rfl

여기서 xs.map f는 List.map f xs로 해석됩니다.

9.2. 객체🔗

지금까지 우리는 생성자를 사용하여 구조체 타입의 원소를 만들어 왔습니다. 필드가 많은 구조체의 경우 필드가 정의된 순서를 기억해야 하므로 이 방식은 불편할 때가 많습니다. 그래서 Lean은 구조체 타입의 원소를 정의할 수 있는 다음과 같은 대체 표기법을 제공합니다.

    { (<field-name> := <expr>)* : structure-type }
    or
    { (<field-name> := <expr>)* }

구조체의 이름을 기대 타입으로부터 추론할 수 있으면 언제든지 접미사 : structure-type을 생략할 수 있습니다. 예를 들어, 이 표기법을 사용하여 “점(point)”을 정의해 봅시다. 필드를 지정하는 순서는 중요하지 않으므로, 아래의 표현식은 모두 같은 점을 정의합니다.

structure Point (α : Type u) where
  x : α
  y : α

{ x := 10, y := 20 } : Point Nat#check { x := 10, y := 20 : Point Nat }

{ x := 10, y := 20 } : Point Nat

{ x := 10, y := 20 } : Point Nat#check { y := 20, x := 10 : Point _ }

{ x := 10, y := 20 } : Point Nat

{ x := 10, y := 20 } : Point Nat#check ({ x := 10, y := 20 } : Point Nat)

{ x := 10, y := 20 } : Point Nat

example : Point Nat :=
  { y := 20, x := 10 }

필드는 중괄호를 사용하여 암시적으로 표시할 수 있습니다. 암시적 필드는 생성자의 암시적 매개변수가 됩니다.

필드의 값이 지정되지 않으면 Lean은 그 값을 추론하려고 시도합니다. 지정되지 않은 필드를 추론할 수 없으면 Lean은 해당 자리 표시자를 합성할 수 없다는 오류를 표시합니다.

`MyStruct`: universes `u`, `v` only occur together. This usually means there is a `max` expression in the type where none of these universes appear on their own.

Note: This linter can be disabled with `set_option linter.checkUnivs false`structure MyStruct where
    {α : Type u}
    {β : Type v}
    a : α
    b : β

{ α := Nat, β := Bool, a := 10, b := true } : MyStruct#check { a := 10, b := true : MyStruct }

{ α := Nat, β := Bool, a := 10, b := true } : MyStruct

레코드 업데이트는 또 다른 흔한 연산으로, 기존 레코드 객체에서 하나 이상의 필드 값을 수정하여 새 레코드 객체를 만드는 것에 해당합니다. Lean에서는 필드 할당 앞에 s with 표기를 덧붙여, 레코드 명세에서 값이 할당되지 않은 필드를 이전에 정의된 구조체 객체 s에서 가져오도록 지정할 수 있습니다. 레코드 객체가 둘 이상 제공되면, Lean은 지정되지 않은 필드를 포함하는 객체를 찾을 때까지 그 객체들을 순서대로 살펴봅니다. 모든 객체를 살펴본 후에도 지정되지 않은 필드 이름이 하나라도 남아 있으면 Lean은 오류를 발생시킵니다.

structure Point (α : Type u) where
  x : α
  y : α
deriving Repr

def p : Point Nat :=
  { x := 1, y := 2 }

{ x := 1, y := 3 }#eval { p with y := 3 }

{ x := 1, y := 3 }

{ x := 4, y := 2 }#eval { p with x := 4 }

{ x := 4, y := 2 }

structure Point3 (α : Type u) where
  x : α
  y : α
  z : α

def q : Point3 Nat :=
  { x := 5, y := 5, z := 5 }

def r : Point3 Nat :=
  { p, q with x := 6 }

example : r.x = 6 := rfl

example : r.y = 2 := rfl

example : r.z = 5 := rfl

9.3. 상속🔗

새 필드를 추가하여 기존 구조체를 확장할 수 있습니다. 이 기능을 사용하면 일종의 상속을 흉내 낼 수 있습니다.

                structure Point (α : Type u) where
  x : α
  y : α

inductive Color where
  | red | green | blue

structure ColorPoint (α : Type u) extends Point α where
  c : Color

다음 예제에서는 다중 상속을 사용하여 구조체를 정의한 다음, 부모 구조체들의 객체를 사용하여 객체를 정의합니다.

                structure Point (α : Type u) where
  x : α
  y : α
  z : α

structure RGBValue where
  red : Nat
  green : Nat
  blue : Nat

structure RedGreenPoint (α : Type u) extends Point α, RGBValue where
  no_blue : blue = 0

def p : Point Nat :=
  { x := 10, y := 10, z := 20 }

def rgp : RedGreenPoint Nat :=
  { p with red := 200, green := 40, blue := 0, no_blue := rfl }

example : rgp.x   = 10 := rfl
example : rgp.red = 200 := rfl