1.3. Functions and Definitions🔗

Lean에서는 def 키워드로 정의를 도입한다. 예를 들어 hello라는 이름이 문자열 "Hello"를 가리키게 정의하려면 다음과 같이 쓴다.

def hello := "Hello"

Lean에서 새 이름은 콜론-등호 연산자인 :=로 정의하며 =를 쓰지 않는다. =는 이미 존재하는 표현식 사이의 동등성(equality)을 나타내는 데 사용되므로, 두 연산자를 다르게 쓰면 혼동을 막을 수 있다.

hello의 정의에서 "Hello" 표현식은 충분히 단순하므로 Lean이 정의의 타입을 자동으로 알아낼 수 있다. 하지만 대부분의 정의는 그렇게 단순하지 않으므로 보통 타입을 추가해야 한다. 정의하는 이름 뒤에 콜론을 쓰면 된다.

def lean : String := "Lean"

이제 이름을 정의했으므로 사용할 수 있다.

"Hello Lean"#eval String.append hello (String.append " " lean)

다음과 같이 출력된다.

"Hello Lean"

Lean에서는 정의한 이름을 정의 뒤에서만 사용할 수 있다.

많은 언어에서 함수 정의는 다른 값의 정의와 다른 문법을 사용한다. 예를 들어 Python 함수 정의는 def 키워드로 시작하고 다른 정의는 등호로 작성한다. Lean에서는 다른 값과 같은 def 키워드로 함수를 정의한다. 그럼에도 hello 같은 정의는 호출할 때마다 같은 결과를 반환하는 인수 없는 함수가 아니라 값 자체를 직접 가리키는 이름을 도입한다.

1.3.1. Defining Functions🔗

Lean에서 함수를 정의하는 방법은 여러 가지다. 가장 간단한 방법은 함수의 인수를 정의의 타입 앞에 공백으로 구분해 두는 것이다. 예를 들어 인수에 1을 더하는 함수는 다음과 같이 쓸 수 있다.

def add1 (n : Nat) : Nat := n + 1

#eval로 이 함수를 시험하면 예상대로 8이 나온다.

8#eval add1 7

함수를 여러 인수에 적용할 때 각 인수 사이에 공백을 쓰는 것처럼 여러 인수를 받는 함수는 인수의 이름과 타입 사이에 공백을 두어 정의한다. 두 인수 중 큰 값과 같은 결과를 내는 maximum 함수는 n, k라는 두 Nat 인수를 받고 Nat을 반환한다.

def maximum (n : Nat) (k : Nat) : Nat :=
  if n < k then
    k
  else n

마찬가지로 spaceBetween 함수는 두 문자열 사이에 공백을 넣어 이어 붙인다.

def spaceBetween (before : String) (after : String) : String :=
  String.append before (String.append " " after)

maximum처럼 정의한 함수에 인수를 주면 본문에서 인수 이름을 주어진 값으로 바꾼 다음 결과 본문을 평가해 결과를 정한다. 예를 들면 다음과 같다.

                  maximum (5 + 8) (2 * 7)maximum 13 14if 13 < 14 then 14 else 1314

자연수·정수·문자열로 평가되는 표현식의 타입은 각각 Nat, Int, String이다. 함수도 마찬가지다. Nat을 받아 Bool을 반환하는 함수의 타입은 Nat → Bool이고, 두 Nat을 받아 Nat을 반환하는 함수의 타입은 Nat → Nat → Nat이다.

특수하게도 Lean은 #check에 이름을 직접 쓰면 함수의 서명을 반환한다. #check add1을 입력하면 add1 (n : Nat) : Nat이 나온다. 함수 이름을 괄호로 감싸 일반 표현식으로 취급하게 하면 함수의 타입을 표시하게 할 수 있다. 따라서 #check (add1)은 add1 : Nat → Nat을, #check (maximum)은 maximum : Nat → Nat → Nat을 낸다. 이 화살표는 ASCII 대체 화살표 ->로도 쓸 수 있으므로 앞의 함수 타입은 각각 example : Nat -> Nat := add1, example : Nat -> Nat -> Nat := maximum으로 쓸 수 있다.

이면에서 모든 함수는 실제로 정확히 하나의 인수를 기대한다. 여러 인수를 받는 것처럼 보이는 maximum 같은 함수는 사실 하나의 인수를 받은 뒤 새 함수를 반환하는 함수다. 새 함수가 다음 인수를 받고 더 이상 인수를 기대하지 않을 때까지 이 과정이 계속된다. 여러 인수 함수에 인수 하나를 제공하면 이를 확인할 수 있다. #check maximum 3은 maximum 3 : Nat → Nat을 내고 #check spaceBetween "Hello "는 spaceBetween "Hello " : String → String을 낸다. 함수를 반환하는 함수로 여러 인수 함수를 구현하는 것을 수학자 Haskell Curry의 이름을 따 커링이라고 한다. 함수 화살표는 오른쪽으로 결합하므로 Nat → Nat → Nat은 Nat → (Nat → Nat)으로 괄호를 칠 수 있다.

1.3.1.1. Exercises🔗

joinStringsWith 함수의 타입을 String → String → String → String으로 정의하라. 이 함수는 첫 번째 인수를 두 번째와 세 번째 인수 사이에 넣어 새 문자열을 만든다. joinStringsWith ", " "one" "and another"는 "one, and another"로 평가되어야 한다.
joinStringsWith ": "의 타입은 무엇인가? Lean으로 답을 확인하라.
주어진 높이, 너비, 깊이로 직육면체의 부피를 계산하는 Nat → Nat → Nat → Nat 타입의 volume 함수를 정의하라.

1.3.2. Defining Types🔗

대부분의 타입 언어에는 C의 typedef처럼 타입 별칭을 정의하는 방법이 있다. 그러나 Lean에서 타입은 언어의 일급 부분이며 다른 값과 마찬가지로 표현식이다. 따라서 정의는 다른 값을 참조하듯 타입도 참조할 수 있다.

예를 들어 String을 입력하기 번거롭다면 더 짧은 약어 Str을 정의할 수 있다.

def Str : Type := String

그러면 정의의 타입으로 String 대신 Str을 사용할 수 있다.

def aStr : Str := "This is a string."

이것이 작동하는 이유는 타입도 Lean의 나머지와 같은 규칙을 따르기 때문이다. 타입은 표현식이고 표현식에서는 정의한 이름을 그 정의로 바꿀 수 있다. Str을 String이라는 뜻으로 정의했으므로 aStr의 정의가 올바르다.

1.3.2.1. Messages You May Meet🔗

타입에 정의를 사용하는 실험은 Lean이 정수 리터럴 오버로딩을 지원하는 방식 때문에 더 복잡해진다. Nat이 너무 짧다면 더 긴 이름 NaturalNumber를 정의할 수 있다.

def NaturalNumber : Type := Nat

그러나 정의의 타입으로 Nat 대신 NaturalNumber를 사용하면 예상대로 작동하지 않는다. 특히 다음 정의는:

def thirtyEight : NaturalNumber := failed to synthesize instance of type class
  OfNat NaturalNumber 38
numerals are polymorphic in Lean, but the numeral `38` cannot be used in a context where the expected type is
  NaturalNumber
due to the absence of the instance above

Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command.38

다음 오류가 발생한다:

failed to synthesize instance of type class
  OfNat NaturalNumber 38
numerals are polymorphic in Lean, but the numeral `38` cannot be used in a context where the expected type is
  NaturalNumber
due to the absence of the instance above

Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command.

이 오류는 Lean이 숫자 리터럴을 오버로드할 수 있게 하기 때문에 발생한다. 가능한 경우 자연수 리터럴을 시스템에 내장된 타입인 것처럼 새 타입에 사용할 수 있다. 이는 수학을 편리하게 표현하려는 Lean의 목표와 관련 있으며 수학의 분야마다 숫자 표기를 매우 다른 목적으로 사용한다. 오버로딩을 허용하는 이 기능은 오버로딩을 찾기 전에 정의한 모든 이름을 정의로 바꾸지 않으므로 위 오류 메시지가 발생한다.

이 제한을 우회하는 한 방법은 정의 오른쪽에 Nat 타입을 제공해 38에 Nat의 오버로딩 규칙을 적용하는 것이다.

def thirtyEight : NaturalNumber := (38 : Nat)

NaturalNumber와 Nat은 정의상 같은 타입이므로 이 정의는 여전히 타입이 올바르다!

또 다른 해결책은 Nat의 오버로딩과 동등하게 작동하는 NaturalNumber 오버로딩을 정의하는 것이다. 그러나 이를 위해서는 Lean의 더 고급 기능이 필요하다.

마지막으로 Nat의 새 이름을 def 대신 abbrev로 정의하면 오버로딩 확인 과정에서 정의한 이름을 그 정의로 바꿀 수 있다. abbrev로 쓴 정의는 항상 전개된다. 예를 들면 다음과 같다.

abbrev N : Type := Nat

그리고

def thirtyNine : N := 39

문제없이 받아들여진다.

이면에서 일부 정의는 오버로딩 확인 중 전개할 수 있도록 내부적으로 표시되고 다른 정의는 그렇지 않다. 전개할 정의를 환원 가능(reducible)이라고 한다. 환원 가능성을 제어하는 것은 Lean의 확장성에 필수적이다. 모든 정의를 완전히 전개하면 기계가 처리하기 느리고 사용자가 이해하기 어려운 매우 큰 타입이 될 수 있다. abbrev로 만든 정의는 환원 가능으로 표시된다.