1.4. Structures
프로그램 작성의 첫 단계는 보통 문제 영역의 개념을 파악한 뒤 코드에서 적절히 표현할 방법을 찾는 것이다.
때로는 영역 개념이 더 단순한 다른 개념의 모음이다.
그렇다면 단순한 구성 요소를 하나의 “패키지”로 묶고 의미 있는 이름을 붙이는 것이 편리하다.
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. Updating Structures
Point의 x 필드를 0으로 바꾸는 zeroX 함수를 생각해 보자.
대부분의 프로그래밍 언어 커뮤니티에서 이 문장은 x가 가리키는 메모리 위치를 새 값으로 덮어쓴다는 뜻이다.
그러나 Lean은 함수형 프로그래밍 언어다.
함수형 프로그래밍에서 이런 말은 거의 항상 새 Point를 할당하고 x 필드가 새 값을 가리키며, 나머지는 원래 구조체 값에서 가져온다는 뜻이다.
x의 새 값을 채우고 y를 수동으로 옮겨 이 설명을 그대로 따르는 것이 zeroX를 작성하는 한 방법이다:
def zeroX (p : Point) : Point :=
{ x := 0, y := p.y }그러나 이 방식에는 단점이 있다. 첫째, 구조체에 새 필드를 추가하면 어떤 필드든 갱신하는 모든 위치를 수정해야 하므로 유지 보수가 어려워진다. 둘째, 구조체에 같은 타입의 필드가 여러 개 있으면 복사해 붙이는 과정에서 필드 내용이 중복되거나 뒤바뀔 위험이 실제로 있다. 마지막으로 프로그램이 길고 번거로워진다.
Lean은 다른 필드는 그대로 두고 구조체의 일부 필드만 바꿀 수 있는 편리한 문법을 제공한다.
구조체 초기화에서 with 키워드를 사용하면 된다.
변경하지 않을 필드의 원천은 with 앞에 쓰고 새 필드는 뒤에 쓴다.
예를 들어 새 x 값만 사용해 zeroX를 다음과 같이 쓸 수 있다:
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. Behind the Scenes
모든 구조체에는 생성자가 있다. 여기서 “생성자”라는 용어가 혼동을 일으킬 수 있다. 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. Exercises
-
높이·너비·깊이를 각각
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