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에 대한 이 정의는 그 설명을 정확히 따릅니다:

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의 경우, 재귀 호출의 결과는 순서쌍입니다. 쌍(pair)은 생성자가 하나뿐이므로, 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)

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

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

동시 매칭(simultaneous matching)은 쌍(pair)에 대한 매칭과 유사하지만, 중요한 차이점이 있습니다. 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로 감쌀지를 결정합니다. halve의 명시적 패턴은 Nat을 2로 나누고 나머지를 버립니다:

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

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

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을 생략하기만 하면 됩니다.

합 타입을 가진 값을 사용할 때는 단 하나의 생성자만 관심 대상인 경우가 흔합니다. 예를 들어, 마크다운 인라인 요소의 부분집합을 나타내는 다음 타입이 주어졌을 때:

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 케이스에서 대체값이 제공되기 때문에 합 타입(sum type)에도 사용할 수 있다는 것입니다. 어떤 맥락에서는 match 대신 if let을 사용하면 코드를 더 읽기 쉽게 만들 수 있습니다.

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

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

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

{ x := 1.000000, y := 2.000000 }

Lean에서는 문자열 앞에 s!를 붙이면 interpolation(보간)이 실행되며, 이는 문자열 안의 중괄호로 감싸인 표현식이 해당 값으로 치환되는 것을 말합니다. 이는 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 컴파일러가 주어진 타입에 대해 이 테이블에서 항목을 찾지 못했음을 의미합니다. 타입 클래스에 관한 장에서는 표에 새 항목을 추가하는 방법을 포함하여 이 메커니즘을 더 자세히 설명합니다.