Lean에서 다형 함수를 작성할 때는 보통 모든 암시적 매개변수를 나열할 필요가 없습니다. 대신 그냥 언급하기만 하면 됩니다. Lean이 그 타입을 결정할 수 있다면 해당 변수는 자동으로 암시적 매개변수로 삽입됩니다. 다시 말해, 앞에서 본 length의 정의는:

def length {α : Type} (xs : List α) : Nat := match xs with | [] => 0 | y :: ys => Nat.succ (length ys)

{α : Type} 없이도 다음과 같이 작성할 수 있습니다:

def length (xs : List α) : Nat := match xs with | [] => 0 | y :: ys => Nat.succ (length ys)

이는 암시적 매개변수를 많이 받는 고도로 다형적인 정의를 크게 단순화할 수 있습니다.

첫 번째 단계는 인자의 타입을 콜론 오른쪽으로 옮겨서 반환 타입이 함수 타입이 되도록 하는 것입니다. 예를 들어, length의 타입은 List α → Nat입니다. 그런 다음, :=를 패턴 매칭의 각 경우로 바꾸십시오:

def length : List α → Nat | [] => 0 | y :: ys => Nat.succ (length ys)

이 문법은 인자를 두 개 이상 받는 함수를 정의하는 데에도 사용할 수 있습니다. 이 경우 각 인자의 패턴은 쉼표로 구분합니다. 예를 들어, drop은 수 n과 리스트를 받아서, 처음 n개의 항목을 제거한 리스트를 반환합니다.

def drop : Nat → List α → List α | Nat.zero, xs => xs | _, [] => [] | Nat.succ n, x :: xs => drop n xs

이름 붙은 인자와 패턴은 한 정의 안에서 함께 사용할 수도 있습니다. 예를 들어, 기본값과 선택적 값을 받아 선택적 값이 none이면 기본값을 반환하는 함수는 다음과 같이 작성할 수 있습니다:

def fromOption (default : α) : Option α → α | none => default | some x => x

이 함수는 표준 라이브러리에서 Option.getD라는 이름으로 제공되며, 점 표기법으로 호출할 수 있습니다:

"salmonberry"#eval (some "salmonberry").getD ""

"salmonberry"

""#eval none.getD ""

""

예를 들어, unzip은 쌍의 리스트를 리스트의 쌍으로 변환하는 함수입니다. 쌍의 리스트가 비어 있으면 unzip의 결과는 빈 리스트 두 개로 이루어진 쌍입니다. 쌍의 리스트 맨 앞에 쌍이 있으면, 그 쌍의 두 필드가 리스트의 나머지 부분을 unzip한 결과에 각각 추가됩니다. 다음 unzip 정의는 이 설명을 그대로 따릅니다:

def unzip : List (α × β) → List α × List β | [] => ([], []) | (x, y) :: xys => (x :: (unzip xys).fst, y :: (unzip xys).snd)

안타깝게도 문제가 하나 있습니다. 이 코드는 필요 이상으로 느립니다. 쌍 리스트의 각 항목마다 재귀 호출이 두 번씩 일어나므로 이 함수는 지수 시간이 걸립니다. 하지만 두 재귀 호출의 결과는 같으므로 재귀 호출을 두 번 할 이유가 없습니다.

Lean에서는 let을 사용하여 재귀 호출의 결과에 이름을 붙여 저장해 둘 수 있습니다. let을 사용한 지역 정의는 def를 사용한 최상위 정의와 비슷합니다. 지역적으로 정의할 이름, 필요한 경우 인자, 타입 시그니처를 받고, 그 뒤에 :=와 본문이 옵니다. 지역 정의 다음에는 그 지역 정의를 사용할 수 있는 표현식(이를 let 표현식의 본문이라고 합니다)이 새 줄에 와야 하며, 이 줄은 파일에서 let 키워드의 열보다 작거나 같은 열에서 시작해야 합니다. unzip에서 let을 사용한 지역 정의는 다음과 같습니다:

def unzip : List (α × β) → List α × List β | [] => ([], []) | (x, y) :: xys => let unzipped : List α × List β := unzip xys (x :: unzipped.fst, y :: unzipped.snd)

let을 한 줄에서 사용하려면 지역 정의와 본문을 세미콜론으로 구분하십시오.

let을 사용하는 지역 정의에서도 하나의 패턴만으로 데이터 타입의 모든 경우를 매칭할 수 있을 때는 패턴 매칭을 사용할 수 있습니다. unzip의 경우, 재귀 호출의 결과는 쌍입니다. 쌍에는 생성자가 하나뿐이므로, unzipped라는 이름을 쌍 패턴으로 대체할 수 있습니다:

def unzip : List (α × β) → List α × List β | [] => ([], []) | (x, y) :: xys => let (xs, ys) : List α × List β := unzip xys (x :: xs, y :: ys)

let과 함께 패턴을 적절히 사용하면 접근자 호출을 직접 작성할 때보다 코드를 더 읽기 쉽게 만들 수 있습니다.

let과 def의 가장 큰 차이점은 재귀적인 let 정의는 let rec이라고 써서 명시적으로 표시해야 한다는 점입니다. 예를 들어, 리스트를 뒤집는 한 가지 방법은 다음 정의처럼 재귀적인 보조 함수를 사용하는 것입니다:

def reverse (xs : List α) : List α := let rec helper : List α → List α → List α | [], soFar => soFar | y :: ys, soFar => helper ys (y :: soFar) helper xs []

보조 함수는 입력 리스트를 따라 내려가면서 항목을 한 번에 하나씩 soFar로 옮깁니다. 입력 리스트의 끝에 도달하면 soFar에는 입력을 뒤집은 리스트가 담겨 있습니다.

많은 경우 Lean은 표현식의 타입을 자동으로 결정할 수 있습니다. 이러한 경우에는 최상위 정의(def 사용)와 지역 정의(let 사용) 모두에서 명시적인 타입을 생략할 수 있습니다. 예를 들어, unzip의 재귀 호출에는 타입 표기가 필요하지 않습니다:

def unzip : List (α × β) → List α × List β | [] => ([], []) | (x, y) :: xys => let unzipped := unzip xys (x :: unzipped.fst, y :: unzipped.snd)

명시적인 match 표현식을 사용하면 unzip의 반환 타입을 생략할 수 있습니다:

def unzip (pairs : List (α × β)) := match pairs with | [] => ([], []) | (x, y) :: xys => let unzipped := unzip xys (x :: unzipped.fst, y :: unzipped.snd)

일반적으로 타입 표기는 너무 적게 붙이기보다는 차라리 너무 많이 붙이는 편이 좋습니다. 첫째, 명시적인 타입은 코드에 대한 가정을 읽는 사람에게 전달합니다. Lean이 스스로 타입을 알아낼 수 있더라도, 타입 정보를 얻으려고 Lean에 거듭 질의하지 않아도 된다면 코드를 읽기가 여전히 더 쉬울 수 있습니다. 둘째, 명시적인 타입은 오류가 발생한 위치를 좁히는 데 도움이 됩니다. 프로그램이 타입을 명시적으로 밝힐수록 오류 메시지가 더 많은 정보를 줄 수 있습니다. 이는 Lean처럼 표현력이 매우 풍부한 타입 시스템을 갖춘 언어에서 특히 중요합니다. 셋째, 명시적인 타입은 애초에 프로그램을 작성하는 일 자체를 더 쉽게 만들어 줍니다. 타입은 명세이며, 컴파일러의 피드백은 그 명세를 만족하는 프로그램을 작성하는 데 유용한 도구가 될 수 있습니다. 마지막으로, Lean의 타입 추론은 최선을 다하되 성공을 보장하지는 않는 시스템입니다. Lean의 타입 시스템은 표현력이 매우 풍부하기 때문에, 모든 표현식에 대해 찾을 수 있는 “최선의” 타입이나 가장 일반적인 타입은 존재하지 않습니다. 즉, 타입을 얻더라도 그것이 주어진 용도에 맞는 타입이라는 보장은 없습니다. 예를 들어, 14는 Nat일 수도 있고 Int일 수도 있습니다:

14 : Nat#check 14

14 : Nat

14 : Int#check (14 : Int)

14 : Int

타입 표기를 생략하면 이해하기 어려운 오류 메시지가 나타날 수 있습니다. unzip의 정의에서 모든 타입을 생략하면 다음과 같습니다:

def unzip pairs := match pairs with | Invalid match expression: This pattern contains metavariables: [][] => ([], []) | (x, y) :: xys => let unzipped := unzip xys (x :: unzipped.fst, y :: unzipped.snd)

match 표현식에 관한 메시지가 나타납니다:

Invalid match expression: This pattern contains metavariables:
  []

이는 match가 검사 대상 값의 타입을 알아야 하는데, 그 타입을 알 수 없었기 때문입니다. “메타변수(metavariable)”는 프로그램에서 아직 알려지지 않은 부분으로, 오류 메시지에서는 ?m.XYZ로 표시됩니다. 메타변수는 다형성에 관한 절에서 설명합니다. 이 프로그램에서는 인자에 타입 표기를 반드시 붙여야 합니다.

아주 간단한 프로그램에도 타입 표기가 필요한 경우가 있습니다. 예를 들어, 항등 함수는 전달받은 인자를 무엇이든 그대로 반환합니다. 인자와 타입 표기를 붙이면 다음과 같습니다.

def id (x : α) : α := x

Lean은 반환 타입을 스스로 결정할 수 있습니다:

def id (x : α) := x

그러나 인자 타입을 생략하면 오류가 발생합니다:

def Failed to infer type of definition `id`id Failed to infer type of binder `x`x := x

Failed to infer type of binder `x`

패턴 매칭 표현식은 패턴 매칭 정의와 마찬가지로 여러 값을 한 번에 매칭할 수 있습니다. 정의에 쓰이는 문법과 비슷하게, 검사할 표현식들과 그 표현식들을 매칭할 패턴들은 모두 쉼표로 구분하여 작성합니다. 다음은 동시 매칭을 사용하는 drop의 한 버전입니다.

def drop (n : Nat) (xs : List α) : List α := match n, xs with | Nat.zero, ys => ys | _, [] => [] | Nat.succ n , y :: ys => drop n ys

동시 매칭은 쌍에 대한 매칭과 비슷하지만 중요한 차이가 있습니다. Lean은 매칭되는 표현식과 패턴 사이의 연결을 추적하며, 이 정보는 종료 검사와 정적 타입 정보 전파를 비롯한 여러 목적에 사용됩니다. 그 결과, 쌍을 매칭하는 버전의 sameLength는 종료 검사기에 의해 거부됩니다. 중간에 끼어든 쌍 때문에 xs와 x :: xs' 사이의 연결이 가려지기 때문입니다:

def fail to show termination for sameLength with errors failed to infer structural recursion: Not considering parameter α of sameLength: it is unchanged in the recursive calls Not considering parameter β of sameLength: it is unchanged in the recursive calls Cannot use parameter xs: failed to eliminate recursive application sameLength xs' ys' Cannot use parameter ys: failed to eliminate recursive application sameLength xs' ys' Could not find a decreasing measure. The basic measures relate at each recursive call as follows: (<, ≤, =: relation proved, ? all proofs failed, _: no proof attempted) xs ys 1) 1816:28-46 ? ? Please use `termination_by` to specify a decreasing measure.sameLength (xs : List α) (ys : List β) : Bool := match (xs, ys) with | ([], []) => true | (x :: xs', y :: ys') => sameLength xs' ys' | _ => false

fail to show termination for
  sameLength
with errors
failed to infer structural recursion:
Not considering parameter α of sameLength:
  it is unchanged in the recursive calls
Not considering parameter β of sameLength:
  it is unchanged in the recursive calls
Cannot use parameter xs:
  failed to eliminate recursive application
    sameLength xs' ys'
Cannot use parameter ys:
  failed to eliminate recursive application
    sameLength xs' ys'


Could not find a decreasing measure.
The basic measures relate at each recursive call as follows:
(<, ≤, =: relation proved, ? all proofs failed, _: no proof attempted)
              xs ys
1) 1816:28-46  ?  ?
Please use `termination_by` to specify a decreasing measure.

두 리스트를 동시에 매칭하면 허용됩니다:

def sameLength (xs : List α) (ys : List β) : Bool := match xs, ys with | [], [] => true | x :: xs', y :: ys' => sameLength xs' ys' | _, _ => false

데이터 타입과 패턴에 관한 절에서 even은 다음과 같이 정의되었습니다:

def even (n : Nat) : Bool := match n with | Nat.zero => true | Nat.succ k => not (even k)

리스트 패턴을 List.cons와 List.nil을 직접 사용할 때보다 더 읽기 쉽게 만들어 주는 특별한 문법이 있는 것처럼, 자연수도 숫자 리터럴과 +를 사용하여 매칭할 수 있습니다. 예를 들어, even은 다음과 같이 정의할 수도 있습니다:

def even : Nat → Bool | 0 => true | n + 1 => not (even n)

이 표기법에서 + 패턴의 인자들은 서로 다른 역할을 합니다. 내부적으로 왼쪽 인자(위에서는 n)는 몇 개의 Nat.succ 패턴의 인자가 되고, 오른쪽 인자(위에서는 1)는 패턴을 몇 개의 Nat.succ로 감쌀지를 결정합니다. Nat을 2로 나누고 나머지를 버리는 halve의 명시적 패턴은 다음과 같습니다:

def halve : Nat → Nat | Nat.zero => 0 | Nat.succ Nat.zero => 0 | Nat.succ (Nat.succ n) => halve n + 1

숫자 리터럴과 +로 대체할 수 있습니다:

def halve : Nat → Nat | 0 => 0 | 1 => 0 | n + 2 => halve n + 1

내부적으로는 두 정의가 완전히 동일합니다. 기억하십시오. halve n + 1은 halve (n + 1)이 아니라 (halve n) + 1과 같습니다.

이 문법을 사용할 때 +의 두 번째 인자는 항상 Nat 리터럴이어야 합니다. 덧셈은 교환 법칙이 성립하지만, 패턴에서 인자의 순서를 뒤바꾸면 다음과 같은 오류가 발생할 수 있습니다:

def halve : Nat → Nat | 0 => 0 | 1 => 0 Invalid pattern(s): `n` is an explicit pattern variable, but it only occurs in positions that are inaccessible to pattern matching: .(Nat.add 2 n)| 2 + n => halve n + 1

Invalid pattern(s): `n` is an explicit pattern variable, but it only occurs in positions that are inaccessible to pattern matching:
  .(Nat.add 2 n)

이 제한 덕분에 Lean은 패턴 안에서 쓰인 + 표기법을 모두 그 기반이 되는 Nat.succ의 사용으로 변환할 수 있으며, 이를 통해 내부적으로 언어를 더 단순하게 유지할 수 있습니다.

Lean에서 함수를 반드시 최상위 수준에서 정의해야 하는 것은 아닙니다. 표현식으로서의 함수는 fun 문법으로 만듭니다. 함수 표현식은 키워드 fun으로 시작하고, 그 뒤에 하나 이상의 매개변수가 오며, 매개변수와 반환 표현식은 =>로 구분됩니다. 예를 들어, 숫자에 1을 더하는 함수는 다음과 같이 작성할 수 있습니다:

fun x => x + 1 : Nat → Nat#check fun x => x + 1

fun x => x + 1 : Nat → Nat

타입 표기는 def에서와 같은 방식으로 괄호와 콜론을 사용하여 작성합니다:

fun x => x + 1 : Int → Int#check fun (x : Int) => x + 1

fun x => x + 1 : Int → Int

마찬가지로, 암시적 매개변수는 중괄호로 작성할 수 있습니다:

fun {α} x => x : {α : Type} → α → α#check fun {α : Type} (x : α) => x

fun {α} x => x : {α : Type} → α → α

이러한 형태의 익명 함수 표현식은 흔히 람다 표현식이라고 불립니다. 프로그래밍 언어를 수학적으로 기술할 때 쓰는 일반적인 표기법에서는 Lean이 키워드 fun을 쓰는 자리에 그리스 문자 λ(람다)를 사용하기 때문입니다. Lean에서는 fun 대신 λ를 사용할 수도 있지만, fun을 쓰는 것이 가장 일반적입니다.

익명 함수는 def에서 사용하는 다중 패턴 스타일도 지원합니다. 예를 들어, 자연수의 선행자가 존재하면 이를 반환하는 함수는 다음과 같이 작성할 수 있습니다.

fun x => match x with | 0 => none | n.succ => some n : Nat → Option Nat#check fun | 0 => none | n + 1 => some n

fun x =>
  match x with
  | 0 => none
  | n.succ => some n : Nat → Option Nat

Lean이 직접 보여 주는 이 함수의 설명에는 이름 붙은 인자와 match 표현식이 들어 있다는 점에 주목하십시오. Lean의 편리한 문법적 축약 표기 중 상당수는 내부적으로 더 단순한 문법으로 전개되며, 이 추상화는 때때로 새어 나옵니다.

인자를 받는 def 정의는 함수 표현식으로 다시 작성할 수 있습니다. 예를 들어, 인자를 두 배로 만드는 함수는 다음과 같이 작성할 수 있습니다.

def double : Nat → Nat := fun | 0 => 0 | k + 1 => double k + 2

익명 함수가 fun x => x + 1처럼 매우 단순한 경우, 함수를 만드는 문법이 꽤 장황할 수 있습니다. 이 예시에서는 함수를 도입하는 데 공백이 아닌 문자 여섯 개가 쓰이는 반면, 함수 본문은 공백이 아닌 문자 세 개로만 이루어져 있습니다. 이처럼 단순한 경우를 위해 Lean은 축약 표기법을 제공합니다. 괄호로 둘러싸인 표현식 안에서는 가운뎃점 문자 ·가 매개변수를 나타낼 수 있으며, 괄호 안의 표현식은 함수의 본문이 됩니다. 앞의 함수는 (· + 1)로도 쓸 수 있습니다.

가운뎃점은 항상 자신을 둘러싼 가장 가까운 괄호 쌍으로부터 함수를 만듭니다. 예를 들어, (· + 5, 3)은 숫자 쌍을 반환하는 함수인 반면, ((· + 5), 3)은 함수와 숫자로 이루어진 쌍입니다. 점을 여러 개 사용하면 왼쪽에서 오른쪽 순서로 매개변수가 됩니다:

익명 함수는 def나 let으로 정의한 함수와 정확히 같은 방식으로 적용할 수 있습니다. 10#eval (fun x => x + x) 5 명령의 결과는 다음과 같습니다:

10

반면 10#eval (· * 2) 5의 결과는 다음과 같습니다:

10

이름은 네임스페이스 안에서 직접 정의할 수 있습니다. 예를 들어, double이라는 이름을 Nat 네임스페이스 안에 정의할 수 있습니다:

def Nat.double (x : Nat) : Nat := x + x

Nat는 타입의 이름이기도 하므로, 점 표기법을 사용하여 Nat 타입의 표현식에 대해 Nat.double을 호출할 수 있습니다:

8#eval (4 : Nat).double

8

네임스페이스 안에 이름을 직접 정의하는 방법 외에도, namespace와 end 명령을 사용해 일련의 선언을 네임스페이스 안에 넣을 수 있습니다. 예를 들어, 다음 코드는 네임스페이스 NewNamespace 안에 triple과 quadruple을 정의합니다:

namespace NewNamespace def triple (x : Nat) : Nat := 3 * x def quadruple (x : Nat) : Nat := 2 * x + 2 * x end NewNamespace

이들을 참조하려면 이름 앞에 NewNamespace.를 붙이십시오:

NewNamespace.triple (x : Nat) : Nat#check NewNamespace.triple

NewNamespace.triple (x : Nat) : Nat

NewNamespace.quadruple (x : Nat) : Nat#check NewNamespace.quadruple

NewNamespace.quadruple (x : Nat) : Nat

네임스페이스는 열 수 있으며, 이렇게 하면 그 안의 이름을 명시적으로 한정하지 않고도 사용할 수 있습니다. 표현식 앞에 open MyNamespace in을 쓰면 해당 표현식 안에서 MyNamespace의 내용을 사용할 수 있습니다. 예를 들어, timesTwelve는 NewNamespace를 연 뒤 quadruple과 triple을 모두 사용합니다:

def timesTwelve (x : Nat) := open NewNamespace in quadruple (triple x)

네임스페이스는 명령 앞에서 열 수도 있습니다. 이렇게 하면 단일 표현식뿐만 아니라 명령의 모든 부분에서 네임스페이스의 내용을 참조할 수 있습니다. 이렇게 하려면 명령 앞에 open ... in을 두십시오.

open NewNamespace in NewNamespace.quadruple (x : Nat) : Nat#check quadruple

NewNamespace.quadruple (x : Nat) : Nat

함수 시그니처에는 이름의 전체 네임스페이스가 표시됩니다. 또한 네임스페이스를 열어 파일의 나머지 부분에 있는 모든 후속 명령에 적용할 수도 있습니다. 이렇게 하려면 최상위 수준에서 open을 사용할 때 in을 생략하기만 하면 됩니다.

합 타입의 값을 사용할 때는 여러 생성자 중 하나에만 관심이 있는 경우가 많습니다. 예를 들어, Markdown 인라인 요소의 일부를 나타내는 다음 타입이 있다고 합시다.

inductive Inline : Type where | lineBreak | string : String → Inline | emph : Inline → Inline | strong : Inline → Inline

문자열 요소를 인식하여 그 내용을 추출하는 함수는 다음과 같이 작성할 수 있습니다:

def Inline.string? (inline : Inline) : Option String := match inline with | Inline.string s => some s | _ => none

이 함수의 본문은 if와 let을 함께 사용하여 작성할 수도 있습니다:

def Inline.string? (inline : Inline) : Option String := if let Inline.string s := inline then some s else none

이것은 패턴 매칭 let 문법과 매우 비슷합니다. 차이점은 else 경우에 대체 동작이 주어지므로 합 타입에도 사용할 수 있다는 것입니다. 어떤 상황에서는 match 대신 if let을 사용하면 코드를 더 읽기 쉽게 만들 수 있습니다.

이름 붙은 생성자 인자를 위한 중괄호 표기법과 마찬가지로, 이 위치 기반 문법은 타입 표기나 프로그램의 다른 타입 정보를 통해 Lean이 구조체의 타입을 결정할 수 있는 문맥에서만 사용할 수 있습니다. 예를 들어, #eval ⟨1, 2⟩를 실행하면 다음과 같은 오류가 발생합니다:

Invalid `⟨...⟩` notation: The expected type of this term could not be determined

이 오류는 사용할 수 있는 타입 정보가 없기 때문에 발생합니다. #eval (⟨1, 2⟩ : Point)와 같이 타입 표기를 추가하면 문제가 해결됩니다:

{ x := 1.000000, y := 2.000000 }

Lean에서는 문자열 앞에 s!를 붙이면 보간이 일어나며, 문자열 안의 중괄호로 감싼 표현식이 그 값으로 대체됩니다. 이는 Python의 f-문자열이나 C#의 $ 접두사 문자열과 비슷합니다. 예를 들어,

"three fives is 15"#eval s!"three fives is {NewNamespace.triple 5}"

다음과 같은 출력을 생성합니다

"three fives is 15"

모든 표현식을 문자열에 보간할 수 있는 것은 아닙니다. 예를 들어, 함수를 보간하려고 하면 오류가 발생합니다.

toString "three fives is " ++ sorry : String#check s!"three fives is {failed to synthesize instance of type class ToString (Nat → Nat) Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command.NewNamespace.triple}"

다음 오류가 발생합니다.

failed to synthesize instance of type class
  ToString (Nat → Nat)

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

이는 함수를 문자열로 변환하는 표준적인 방법이 없기 때문입니다. 컴파일러는 다양한 타입의 표현식을 평가한 결과를 어떻게 표시할지 기술하는 표를 유지하는 것과 마찬가지로, 다양한 타입의 값을 문자열로 어떻게 변환할지 기술하는 표도 유지합니다. failed to synthesize instance 메시지는 Lean 컴파일러가 이 표에서 주어진 타입에 해당하는 항목을 찾지 못했다는 뜻입니다. 타입 클래스에 관한 장에서는 표에 새 항목을 추가하는 방법을 포함하여 이 메커니즘을 더 자세히 설명합니다.