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의 경우 재귀 호출의 결과는 쌍이다. 쌍에는 생성자가 하나뿐이므로 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가 검사할 값의 타입을 알아야 하지만 그 타입을 알 수 없기 때문이다. “메타변수”는 프로그램에서 알려지지 않은 부분이며 오류 메시지에서는 ?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의 내용을 사용할 수 있다. 예를 들어 NewNamespace를 연 뒤 timesTwelve는 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

이 함수의 본문을 작성하는 다른 방법은 let과 함께 if를 사용하는 것이다:

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 컴파일러가 주어진 타입에 대한 표의 항목을 찾지 못했다는 뜻이다. 타입 클래스 절에서는 표에 새 항목을 추가하는 방법을 포함해 이 메커니즘을 더 자세히 설명한다.