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)
데카르트 좌표점(Cartesian point)은 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