1.3. 함수와 정의🔗

Lean에서 정의는 def 키워드를 사용하여 도입합니다. 예를 들어, 이름 hello가 문자열 "Hello"를 가리키도록 정의하려면 다음과 같이 작성합니다:

def hello := "Hello"

Lean에서는 새 이름을 정의할 때 =가 아니라 콜론-등호 연산자 :=를 사용합니다. 이는 =가 이미 존재하는 표현식 사이의 동등성을 기술하는 데 쓰이기 때문이며, 서로 다른 두 연산자를 사용하면 혼동을 막는 데 도움이 됩니다.

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. 함수 정의하기🔗

Lean에서 함수를 정의하는 방법은 다양합니다. 가장 간단한 방법은 함수의 인자를 정의의 타입 앞에 공백으로 구분하여 두는 것입니다. 예를 들어, 인자에 1을 더하는 함수는 다음과 같이 작성할 수 있습니다:

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

#eval로 이 함수를 테스트하면 예상대로 8이 나옵니다:

8#eval add1 7

인자 사이마다 공백을 넣어 함수를 여러 인자에 적용하듯이, 여러 인자를 받는 함수도 인자의 이름과 타입 사이에 공백을 넣어 정의합니다. 함수 maximum은 두 인자 중 더 큰 값을 결과로 내며, 두 개의 Nat 인자 n과 k를 받아 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입니다.

특수한 경우로, 함수 이름을 #check와 함께 직접 사용하면 Lean은 그 함수의 시그니처를 반환합니다. #check add1을 입력하면 add1 (n : Nat) : Nat이 출력됩니다. 그러나 함수 이름을 괄호로 감싸면 함수가 일반 표현식으로 취급되므로, 이를 이용해 Lean이 함수의 타입을 보여 주도록 “속일” 수 있습니다. 따라서 #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)의 이름을 따서 커링(currying)이라고 합니다. 함수 화살표는 오른쪽으로 결합합니다. 즉, Nat → Nat → Nat는 Nat → (Nat → Nat)처럼 괄호를 친 것으로 읽어야 합니다.

1.3.1.1. 연습 문제🔗

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

1.3.2. 타입 정의하기🔗

타입이 있는 프로그래밍 언어 대부분에는 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. 마주칠 수 있는 메시지🔗

타입에 정의를 사용하는 실험은 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로 만든 정의는 환원 가능한 것으로 표시됩니다.