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. 연습 문제🔗

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

1.3.2. 타입 정의하기🔗

대부분의 타입이 있는 프로그래밍 언어에는 C의 typedef처럼 타입에 대한 별칭을 정의하는 수단이 있습니다. 하지만 Lean에서는 타입이 언어의 일급(first-class) 요소입니다—타입은 다른 것들과 마찬가지로 표현식입니다. 이는 정의(definition)가 다른 값을 참조할 수 있는 것과 마찬가지로 타입도 참조할 수 있음을 의미합니다.

예를 들어 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의 더 고급 기능이 필요합니다.

마지막으로, def 대신 abbrev를 사용하여 Nat의 새 이름을 정의하면 오버로딩 해소가 정의된 이름을 그 정의로 치환할 수 있게 됩니다. abbrev를 사용하여 작성된 정의는 항상 펼쳐집니다. 예를 들어,

abbrev N : Type := Nat

그리고

def thirtyNine : N := 39

아무런 문제없이 받아들여집니다.

내부적으로는 일부 정의가 오버로드 해소 과정에서 펼쳐질 수 있는 것으로 표시되는 반면, 그렇지 않은 정의도 있습니다. 펼쳐지게 될 정의를 reducible(축약 가능)하다고 부릅니다. Lean이 확장 가능하도록 하려면 축약 가능성(reducibility)에 대한 제어가 필수적입니다. 모든 정의를 완전히 펼치면 기계가 처리하기에는 지나치게 느리고 사용자가 이해하기에는 어려운, 매우 큰 타입이 만들어질 수 있습니다. abbrev로 생성된 정의는 reducible로 표시됩니다.