1.4. 구조체
프로그램을 작성하는 첫 단계는 보통 문제 영역의 개념을 파악한 다음, 그 개념을 코드로 표현할 적절한 방법을 찾는 것입니다. 때로는 어떤 영역의 개념이 더 단순한 다른 개념들의 모음인 경우가 있습니다. 이런 경우에는 이 단순한 구성 요소들을 하나의 “패키지”로 묶고 의미 있는 이름을 붙이면 편리할 수 있습니다. Lean에서는 구조체를 사용하여 이를 수행하며, 구조체는 C나 Rust의 struct, C#의 record와 유사합니다.
구조체를 정의하면 다른 어떤 타입으로도 환원할 수 없는 완전히 새로운 타입이 Lean에 도입됩니다. 이는 여러 구조체가 같은 데이터를 담고 있으면서도 서로 다른 개념을 나타낼 수 있기 때문에 유용합니다. 예를 들어, 점은 데카르트 좌표나 극좌표 중 하나로 표현할 수 있는데, 어느 쪽이든 부동소수점 수 한 쌍으로 이루어집니다. 별도의 구조체를 정의하면 API 클라이언트가 둘을 서로 혼동하는 일을 막을 수 있습니다.
Lean의 부동소수점 수 타입은 Float라고 하며, 부동소수점 수는 일반적인 표기법으로 씁니다.
#check 1.2#check -454.2123215#check 0.0
부동소수점 수를 소수점과 함께 작성하면 Lean은 타입을 Float로 추론합니다. 소수점 없이 작성하면 타입 표기가 필요할 수 있습니다.
#check 0#check (0 : Float)
데카르트 좌표의 점은 x와 y라는 두 개의 Float 필드를 가진 구조체입니다. 이는 structure 키워드를 사용하여 선언합니다.
structure Point where
x : Float
y : Float
이 선언 이후 Point는 새로운 구조체 타입이 됩니다. 구조체 타입의 값을 만드는 일반적인 방법은 중괄호 안에 모든 필드의 값을 제공하는 것입니다. 데카르트 평면의 원점은 x와 y가 모두 0인 지점입니다:
def origin : Point := { x := 0.0, y := 0.0 }
#eval origin의 결과는 origin의 정의와 매우 비슷해 보입니다.
구조체는 여러 데이터를 “하나로 묶어” 이름을 붙이고 하나의 단위로 다루기 위해 존재하므로, 구조체의 개별 필드를 꺼낼 수 있는 것도 중요합니다. 이는 C, Python, Rust, JavaScript에서처럼 점 표기법을 사용하여 수행합니다.
#eval origin.x#eval origin.y이를 사용하여 구조체를 인자로 받는 함수를 정의할 수 있습니다. 예를 들어, 점의 덧셈은 내부의 좌표 값들을 더하는 방식으로 수행됩니다. 다음이 성립해야 합니다.
#eval addPoints { x := 1.5, y := 32 } { x := -8, y := 0.2 }결과는 다음과 같습니다
이 함수는 p1과 p2라는 두 Point를 인자로 받습니다. 결과로 나오는 점은 p1과 p2 양쪽의 x 필드와 y 필드를 바탕으로 합니다:
def addPoints (p1 : Point) (p2 : Point) : Point :=
{ x := p1.x + p2.x, y := p1.y + p2.y }
마찬가지로, 두 점 사이의 거리는 두 점의 x 성분의 차를 제곱한 값과 y 성분의 차를 제곱한 값을 더한 뒤 제곱근을 취한 것이며, 다음과 같이 작성할 수 있습니다:
def distance (p1 : Point) (p2 : Point) : Float :=
Float.sqrt (((p2.x - p1.x) ^ 2.0) + ((p2.y - p1.y) ^ 2.0))
예를 들어, (1, 2)와 (5, -1) 사이의 거리는 5입니다:
#eval distance { x := 1.0, y := 2.0 } { x := 5.0, y := -1.0 }
여러 구조체가 같은 이름의 필드를 가질 수 있습니다. 3차원 점 데이터 타입은 x와 y 필드를 공유할 수 있으며, 같은 필드 이름으로 인스턴스를 만들 수 있습니다:
structure Point3D where
x : Float
y : Float
z : Floatdef origin3D : Point3D := { x := 0.0, y := 0.0, z := 0.0 }즉, 중괄호 문법을 사용하려면 구조체의 기대 타입을 알 수 있어야 합니다. 타입을 알 수 없으면 Lean은 구조체를 인스턴스화할 수 없습니다. 예를 들어,
#check { x := 0.0, y := 0.0 }다음과 같은 오류가 발생합니다
늘 그렇듯이, 타입 표기를 제공하면 이 상황을 해결할 수 있습니다.
#check ({ x := 0.0, y := 0.0 } : Point)프로그램을 더 간결하게 작성할 수 있도록, Lean에서는 중괄호 안에 구조체 타입 표기를 넣는 것도 허용합니다.
#check { x := 0.0, y := 0.0 : Point}1.4.1. 구조체 업데이트하기
Point의 x 필드를 0으로 바꾸는 함수 zeroX를 생각해 봅시다. 대부분의 프로그래밍 언어 커뮤니티에서 이 문장은 x가 가리키는 메모리 위치를 새 값으로 덮어쓴다는 뜻입니다. 그러나 Lean은 함수형 프로그래밍 언어입니다. 함수형 프로그래밍 커뮤니티에서 이런 문장은 거의 언제나 새로운 Point를 할당한다는 뜻입니다. 이때 x 필드는 새 값을 가리키고, 나머지 필드는 모두 입력의 원래 값을 가리킵니다. zeroX를 작성하는 한 가지 방법은 이 설명을 문자 그대로 따르는 것입니다. x에는 새 값을 채우고 y는 직접 옮겨 줍니다:
def zeroX (p : Point) : Point :=
{ x := 0, y := p.y }하지만 이런 프로그래밍 스타일에는 단점이 있습니다. 첫째, 구조체에 새 필드가 추가되면 필드를 하나라도 갱신하는 모든 곳을 수정해야 하므로 유지보수가 어려워집니다. 둘째, 구조체에 같은 타입의 필드가 여러 개 있으면 복사-붙여넣기 코딩 때문에 필드 내용이 중복되거나 뒤바뀔 위험이 실제로 있습니다. 마지막으로, 프로그램이 길고 번잡해집니다.
Lean은 구조체의 일부 필드는 바꾸고 나머지 필드는 그대로 두는 편리한 문법을 제공합니다. 이는 구조체 초기화에서 with 키워드를 사용하여 수행합니다. 바뀌지 않는 필드의 출처는 with 앞에 오고, 새 필드는 그 뒤에 옵니다. 예를 들어, zeroX는 새 x 값만으로 작성할 수 있습니다:
def zeroX (p : Point) : Point :=
{ p with x := 0 }
이 구조체 갱신 문법은 기존 값을 수정하지 않는다는 점을 기억하십시오. 이 문법은 기존 값과 일부 필드를 공유하는 새로운 값을 만듭니다. 점 fourAndThree가 주어졌을 때:
def fourAndThree : Point :=
{ x := 4.3, y := 3.4 }
이 값을 평가하고, zeroX로 갱신한 결과를 평가한 다음, 다시 이 값을 평가하면 원래 값이 나옵니다:
#eval fourAndThree#eval zeroX fourAndThree#eval fourAndThree구조체 업데이트가 원래 구조체를 수정하지 않는다는 사실에서 비롯되는 결과 중 하나는 새 값이 이전 값으로부터 계산되는 경우를 추론하기가 더 쉬워진다는 점입니다. 이전 구조체에 대한 모든 참조는 새로 제공된 모든 값에서도 계속 같은 필드 값을 가리킵니다.
1.4.2. 내부 동작 살펴보기
모든 구조체에는 생성자가 있습니다. 여기서 “생성자”라는 용어는 혼란을 일으킬 수 있습니다. Java나 Python 같은 언어의 생성자와 달리, Lean의 생성자는 데이터 타입이 초기화될 때 실행되는 임의의 코드가 아닙니다. 대신 생성자는 새로 할당된 자료 구조에 저장할 데이터를 모으기만 합니다. 데이터를 전처리하거나 유효하지 않은 인자를 거부하는 사용자 정의 생성자를 제공하는 것은 불가능합니다. 이는 사실 “생성자”라는 단어가 두 맥락에서 서로 다르지만 연관된 의미를 지니는 경우입니다.
기본적으로 S라는 이름의 구조체의 생성자 이름은 S.mk입니다. 여기서 S는 네임스페이스 한정자이고, mk는 생성자 자체의 이름입니다. 중괄호 초기화 문법을 사용하는 대신 생성자를 직접 적용할 수도 있습니다.
#check Point.mk 1.5 2.8하지만 이는 일반적으로 좋은 Lean 스타일로 여겨지지 않으며, Lean조차도 피드백을 반환할 때 표준 구조체 초기화 문법을 사용합니다.
생성자는 함수 타입을 가지므로, 함수가 필요한 곳이라면 어디서든 사용할 수 있습니다. 예를 들어 Point.mk는 두 개의 Float(각각 x와 y)를 받아 새로운 Point를 반환하는 함수입니다.
#check (Point.mk)
구조체의 생성자 이름을 재정의하려면 이름 앞에 콜론 두 개를 붙여 작성하십시오. 예를 들어 Point.mk 대신 Point.point를 사용하려면 다음과 같이 작성하십시오.
structure Point where
point ::
x : Float
y : Float
구조체에는 생성자뿐 아니라 각 필드마다 접근자 함수도 정의됩니다. 접근자 함수는 구조체의 네임스페이스에 속하며 이름은 해당 필드와 같습니다. Point의 경우 접근자 함수 Point.x와 Point.y가 생성됩니다.
#check (Point.x)#check (Point.y)
사실, 중괄호를 사용한 구조체 생성 문법이 내부적으로 구조체 생성자 호출로 변환되는 것과 마찬가지로, 앞서 정의한 addPoints에 있는 문법 x도 x 접근자 호출로 변환됩니다. 즉, #eval origin.x와 #eval Point.x origin은 모두 다음 결과를 냅니다
접근자 점 표기법은 구조체 필드 외에도 사용할 수 있습니다. 인자를 몇 개 받든 상관없이 함수에도 사용할 수 있습니다. 더 일반적으로, 접근자 표기법은 TARGET.f ARG1 ARG2 ... 형태를 가집니다. TARGET의 타입이 T이면 T.f라는 이름의 함수가 호출됩니다. TARGET은 그 함수에서 타입이 T인 가장 왼쪽 인자가 되며, 이 인자는 첫 번째 인자인 경우가 많지만 항상 그런 것은 아닙니다. ARG1 ARG2 ...는 나머지 인자로 순서대로 전달됩니다. 예를 들어, String은 append 필드를 가진 구조체가 아니지만, 접근자 표기법을 사용하여 문자열에서 String.append를 호출할 수 있습니다.
#eval "one string".append " and another"
이 예제에서 TARGET은 "one string"을 나타내고, ARG1은 " and another"를 나타냅니다.
Point.modifyBoth 함수(즉, Point 네임스페이스에 정의된 modifyBoth)는 Point의 두 필드 모두에 함수를 적용합니다:
def Point.modifyBoth (f : Float → Float) (p : Point) : Point :=
{ x := f p.x, y := f p.y }
Point 인자가 함수 인자보다 뒤에 오더라도 점 표기법을 사용할 수 있습니다:
#eval fourAndThree.modifyBoth Float.floor
이 경우 TARGET은 fourAndThree를 나타내고, ARG1은 Float.floor입니다. 접근자 표기법의 대상이 반드시 첫 번째 인자로 쓰이는 것이 아니라, 타입이 일치하는 첫 번째 인자로 쓰이기 때문입니다.
1.4.3. 연습 문제
-
직육면체의 높이, 너비, 깊이를 각각
Float로 담는RectangularPrism이라는 이름의 구조체를 정의하십시오. -
직육면체의 부피를 계산하는
volume : RectangularPrism → Float라는 이름의 함수를 정의하십시오. -
선분을 양 끝점으로 나타내는
Segment라는 이름의 구조체를 정의하고, 선분의 길이를 계산하는 함수length : Segment → Float를 정의하십시오.Segment의 필드는 최대 두 개여야 합니다. -
RectangularPrism선언으로 도입되는 이름은 무엇입니까? -
다음
Hamster와Book선언은 어떤 이름들을 도입합니까? 그 이름들의 타입은 무엇입니까?structure Hamster where name : String fluffy : Boolstructure Book where makeBook :: title : String author : String price : Float