3.6. 강제 변환
수학에서는 같은 기호를 서로 다른 맥락에서 어떤 객체의 서로 다른 측면을 나타내는 데 사용하는 경우가 흔합니다. 예를 들어 집합이 필요한 맥락에서 환을 언급한다면, 그 환의 기반 집합을 의도한 것으로 이해합니다. 프로그래밍 언어에서는 한 타입의 값을 다른 타입의 값으로 자동 변환하는 규칙을 두는 경우가 흔합니다. Java는 byte가 int로 자동 승격되도록 허용하며, Kotlin은 nullable 타입을 기대하는 맥락에서 그 타입의 non-nullable 버전을 사용할 수 있도록 허용합니다.
Lean에서는 강제 변환이라는 메커니즘이 이 두 가지 목적을 모두 담당합니다. Lean은 어떤 타입의 표현식이 다른 타입을 기대하는 문맥에 나타나면, 타입 오류를 보고하기 전에 그 표현식을 강제 변환하려고 시도합니다. Java, C, Kotlin과 달리 Lean의 강제 변환은 타입 클래스의 인스턴스를 정의하여 확장할 수 있습니다.
3.6.1. 문자열과 경로
feline의 소스 코드에서는 익명 생성자 문법을 사용하여 String을 FilePath로 변환합니다. 사실 이 변환은 필요하지 않았습니다. Lean은 String에서 FilePath로의 강제 변환을 정의하므로, 경로가 필요한 자리에 문자열을 사용할 수 있습니다. 함수 IO.FS.readFile의 타입은 System.FilePath → IO String이지만, Lean은 다음 코드를 받아들입니다:
def fileDumper : IO Unit := do
let stdin ← IO.getStdin
let stdout ← IO.getStdout
stdout.putStr "Which file? "
stdout.flush
let f := (← stdin.getLine).trimAscii.copy
stdout.putStrLn s!"'The file {f}' contains:"
stdout.putStrLn (← IO.FS.readFile f)
String.trimAscii는 문자열 앞뒤의 공백을 제거하고 문자열 슬라이스를 반환합니다. 이 슬라이스는 String.Slice.copy를 사용해 다시 문자열로 변환됩니다. fileDumper의 마지막 줄에서는 String에서 FilePath로의 강제 변환이 f를 자동으로 변환하므로 IO.FS.readFile ⟨f⟩라고 쓸 필요가 없습니다.
3.6.2. 양수
모든 양수는 자연수에 대응합니다. 앞서 정의한 함수 Pos.toNat은 Pos를 그에 대응하는 Nat으로 변환합니다:
def Pos.toNat : Pos → Nat
| Pos.one => 1
| Pos.succ n => n.toNat + 1
List.drop 함수는 {α : Type} → Nat → List α → List α 타입을 가지며, 리스트의 앞부분을 제거합니다. 그러나 List.drop을 Pos에 적용하면 타입 오류가 발생합니다:
[1, 2, 3, 4].drop (2 : Pos)
List.drop의 작성자가 이 함수를 타입 클래스의 메서드로 만들지 않았기 때문에, 새 인스턴스를 정의하는 방식으로는 이 함수를 재정의할 수 없습니다.
타입 클래스 Coe는 한 타입을 다른 타입으로 강제 변환하는 여러 오버로드된 방법을 기술합니다:
class Coe (α : Type) (β : Type) where
coe : α → β
Coe Pos Nat 인스턴스 하나만 있으면 앞의 코드가 동작합니다:
instance : Coe Pos Nat where
coe x := x.toNat#eval [1, 2, 3, 4].drop (2 : Pos)
#check를 사용하면 내부적으로 사용된 인스턴스 검색의 결과를 볼 수 있습니다:
#check [1, 2, 3, 4].drop (2 : Pos)3.6.3. 강제 변환 연쇄하기
강제 변환을 찾을 때 Lean은 더 작은 강제 변환들을 연쇄적으로 이어 붙여 하나의 강제 변환을 구성하려고 시도합니다. 예를 들어, Nat에서 Int로 가는 강제 변환은 이미 존재합니다. 이 인스턴스가 Coe Pos Nat 인스턴스와 결합되므로 다음 코드가 받아들여집니다:
def oneInt : Int := Pos.one
이 정의는 강제 변환을 두 번 사용합니다. 먼저 Pos에서 Nat으로, 그다음 Nat에서 Int로 변환합니다.
Lean 컴파일러는 순환하는 강제 변환이 있어도 멈추지 않습니다. 예를 들어, 두 타입 A와 B가 서로 강제 변환될 수 있더라도, 이들 사이의 상호 강제 변환을 이용해 경로를 찾을 수 있습니다:
inductive A where
| a
inductive B where
| b
instance : Coe A B where
coe _ := B.b
instance : Coe B A where
coe _ := A.a
instance : Coe Unit A where
coe _ := A.a
def coercedToB : B := ()
기억하십시오: 이중 괄호 ()는 생성자 Unit.unit의 축약형입니다. deriving instance Repr for B로 Repr B 인스턴스를 파생한 후,
#eval coercedToB결과는 다음과 같습니다:
Option 타입은 C#과 Kotlin의 nullable 타입과 비슷하게 사용할 수 있습니다. none 생성자는 값이 없음을 나타냅니다. Lean 표준 라이브러리는 임의의 타입 α에서 Option α로의 강제 변환을 정의하며, 이 강제 변환은 값을 some으로 감쌉니다. 이 강제 변환 덕분에 some을 생략할 수 있으므로, 옵션 타입을 nullable 타입과 한층 더 비슷한 방식으로 사용할 수 있습니다. 예를 들어, 리스트의 마지막 항목을 찾는 함수 List.last?는 반환값 x를 some으로 감싸지 않고도 작성할 수 있습니다:
def List.last? : List α → Option α
| [] => none
| [x] => x
| _ :: x :: xs => last? (x :: xs)
인스턴스 검색은 강제 변환을 찾아 coe 호출을 삽입하며, 이 호출은 인자를 some으로 감쌉니다. 이러한 강제 변환은 연쇄적으로 적용될 수 있으므로, Option을 중첩해서 사용하더라도 some 생성자를 중첩할 필요가 없습니다:
def perhapsPerhapsPerhaps : Option (Option (Option String)) :=
"Please don't tell me"강제 변환은 Lean이 추론된 타입과 프로그램의 나머지 부분에서 요구하는 타입이 서로 맞지 않음을 발견했을 때에만 자동으로 활성화됩니다. 다른 오류가 있는 경우에는 강제 변환이 활성화되지 않습니다. 예를 들어 인스턴스가 없다는 오류인 경우에는 강제 변환이 사용되지 않습니다:
def perhapsPerhapsPerhapsNat : Option (Option (Option Nat)) :=
392
이 문제는 OfNat에 사용할 타입을 직접 지정하면 우회할 수 있습니다:
def perhapsPerhapsPerhapsNat : Option (Option (Option Nat)) :=
(392 : Nat)또한 위쪽 화살표를 사용하여 강제 변환을 직접 삽입할 수도 있습니다:
def perhapsPerhapsPerhapsNat : Option (Option (Option Nat)) :=
↑(392 : Nat)경우에 따라서는 이를 사용해 Lean이 올바른 인스턴스를 찾도록 보장할 수 있습니다. 또한 프로그래머의 의도를 더 분명하게 드러낼 수도 있습니다.
3.6.4. 비어 있지 않은 리스트와 의존 강제 변환
Coe α β 인스턴스는 β 타입이 α 타입의 각 값을 나타낼 수 있는 값을 가질 때 타당합니다. Int 타입은 모든 자연수를 포함하므로 Nat에서 Int로 강제 변환하는 것은 타당하지만, Nat는 음수를 포함하지 않으므로 Int에서 Nat로의 강제 변환은 좋지 않은 생각입니다. 마찬가지로, List 타입은 비어 있지 않은 모든 리스트를 나타낼 수 있으므로 비어 있지 않은 리스트에서 일반 리스트로의 강제 변환은 타당합니다:
instance : Coe (NonEmptyList α) (List α) where
coe
| { head := x, tail := xs } => x :: xs
이를 통해 비어 있지 않은 리스트를 List API 전체와 함께 사용할 수 있습니다.
반면, 빈 리스트를 나타낼 수 있는 비어 있지 않은 리스트는 없기 때문에 Coe (List α) (NonEmptyList α)의 인스턴스는 작성할 수 없습니다. 이 한계는 의존 강제 변환이라고 불리는 또 다른 형태의 강제 변환을 사용하여 우회할 수 있습니다. 의존 강제 변환은 한 타입에서 다른 타입으로 강제 변환할 수 있는지가 강제 변환되는 특정 값에 따라 달라질 때 사용할 수 있습니다. OfNat 타입 클래스가 오버로드되는 특정 Nat을 매개변수로 받는 것처럼, 의존 강제 변환은 강제 변환되는 값을 매개변수로 받습니다:
class CoeDep (α : Type) (x : α) (β : Type) where
coe : β
이것은 값에 추가적인 타입 클래스 제약을 부과하거나 특정 생성자를 직접 작성하여 특정 값만을 선택할 수 있는 기회입니다. 예를 들어, 실제로 비어 있지 않은 List는 모두 NonEmptyList로 강제 변환될 수 있습니다:
instance : CoeDep (List α) (x :: xs) (NonEmptyList α) where
coe := { head := x, tail := xs }3.6.5. 타입으로 강제 변환하기
수학에서는 추가적인 구조를 갖춘 집합으로 이루어진 개념을 흔히 볼 수 있습니다. 예를 들어, 모노이드는 어떤 집합 S, S의 원소 s, 그리고 S 위의 결합적인 이항 연산자로 이루어지며, 이때 s는 연산자의 왼쪽과 오른쪽 모두에서 항등원입니다. S를 모노이드의 “캐리어 집합”이라고 부릅니다. 0과 덧셈을 갖춘 자연수는 모노이드를 이룹니다. 덧셈은 결합적이고, 어떤 수에 0을 더해도 그 수가 그대로 나오기 때문입니다. 마찬가지로, 1과 곱셈을 갖춘 자연수도 모노이드를 이룹니다. 모노이드는 함수형 프로그래밍에서도 널리 사용됩니다. 리스트, 빈 리스트, 이어 붙이기 연산자는 모노이드를 이루며, 문자열, 빈 문자열, 문자열 이어 붙이기도 마찬가지입니다.
structure Monoid where
Carrier : Type
neutral : Carrier
op : Carrier → Carrier → Carrier
def natMulMonoid : Monoid :=
{ Carrier := Nat, neutral := 1, op := (· * ·) }
def natAddMonoid : Monoid :=
{ Carrier := Nat, neutral := 0, op := (· + ·) }
def stringMonoid : Monoid :=
{ Carrier := String, neutral := "", op := String.append }
def listMonoid (α : Type) : Monoid :=
{ Carrier := List α, neutral := [], op := List.append }
모노이드가 주어지면 foldMap 함수를 작성할 수 있습니다. 이 함수는 리스트를 단 한 번 순회하면서 각 항목을 모노이드의 캐리어 집합으로 변환한 다음, 모노이드의 연산자로 결합합니다. 모노이드에는 항등원이 있으므로 리스트가 비어 있을 때 반환할 자연스러운 결과가 존재하며, 연산자가 결합 법칙을 만족하므로 함수의 클라이언트는 재귀 함수가 원소를 왼쪽에서 오른쪽으로 결합하는지 오른쪽에서 왼쪽으로 결합하는지 신경 쓸 필요가 없습니다.
def foldMap (M : Monoid) (f : α → M.Carrier) (xs : List α) : M.Carrier :=
let rec go (soFar : M.Carrier) : List α → M.Carrier
| [] => soFar
| y :: ys => go (M.op soFar (f y)) ys
go M.neutral xs모노이드는 서로 다른 세 가지 정보로 이루어져 있지만, 그 집합을 가리킬 때는 흔히 모노이드의 이름만 사용합니다. “A가 모노이드이고 x와 y가 그 캐리어 집합의 원소라고 합시다”라고 말하는 대신, “A가 모노이드이고 x와 y가 A의 원소라고 합시다”라고 말하는 것이 일반적입니다. 이러한 관행은 모노이드에서 그 캐리어 집합으로 가는 새로운 종류의 강제 변환을 정의함으로써 Lean에서 표현할 수 있습니다.
CoeSort 클래스는 Coe 클래스와 똑같지만, 강제 변환의 대상이 반드시 소트(sort), 즉 Type 또는 Prop이어야 한다는 점만 다릅니다. Lean에서 소트(sort)라는 용어는 다른 타입을 분류하는 이러한 타입들을 가리킵니다—Type은 그 자체로 데이터를 분류하는 타입들을 분류하고, Prop은 그 자체로 자신이 참이라는 증거를 분류하는 명제들을 분류합니다. 타입 불일치가 발생할 때 Coe를 확인하는 것처럼, 소트가 와야 하는 맥락에 소트가 아닌 것이 주어지면 CoeSort가 사용됩니다.
모노이드를 캐리어 집합으로 바꾸는 강제 변환은 캐리어를 꺼냅니다:
instance : CoeSort Monoid Type where
coe m := m.Carrier이 강제 변환을 사용하면 타입 시그니처가 덜 번거로워집니다:
def foldMap (M : Monoid) (f : α → M) (xs : List α) : M :=
let rec go (soFar : M) : List α → M
| [] => soFar
| y :: ys => go (M.op soFar (f y)) ys
go M.neutral xs
CoeSort의 또 다른 유용한 예시는 Bool과 Prop 사이의 간극을 메우는 데 사용됩니다. 순서와 동등성에 관한 절에서 논의했듯이, Lean의 if 표현식은 조건이 Bool이 아니라 결정 가능한 명제이기를 기대합니다. 하지만 프로그램은 일반적으로 불리언 값에 따라 분기할 수 있어야 합니다. Lean 표준 라이브러리는 두 종류의 if 표현식을 두는 대신, Bool에서 해당 Bool이 true와 같다는 명제로의 강제 변환을 정의합니다:
instance : CoeSort Bool Prop where
coe b := b = true
이 경우 해당 소트는 Type이 아니라 Prop입니다.
3.6.6. 함수로의 강제 변환
프로그래밍에서 자주 등장하는 많은 데이터 타입은 함수와 그 함수에 대한 추가 정보로 구성됩니다. 예를 들어, 함수에는 로그에 표시할 이름이나 어떤 설정 데이터가 함께 딸려 있을 수 있습니다. 또한 Monoid 예제처럼 구조체의 필드에 타입을 넣는 방식은, 어떤 연산을 구현하는 방법이 여러 가지이고 타입 클래스가 허용하는 것보다 더 많은 수동 제어가 필요한 상황에서 타당할 수 있습니다. 예를 들어, 다른 애플리케이션이 특정 형식을 기대하기 때문에 JSON 직렬화기가 내보내는 값의 구체적인 세부 사항이 중요할 수 있습니다. 때로는 함수 자체를 설정 데이터만으로 도출할 수도 있습니다.
CoeFun이라는 타입 클래스는 함수가 아닌 타입의 값을 함수 타입으로 변환할 수 있습니다. CoeFun에는 매개변수가 두 개 있습니다. 첫 번째는 값을 함수로 변환할 대상 타입이고, 두 번째는 정확히 어떤 함수 타입으로 변환할지를 결정하는 출력 매개변수입니다.
class CoeFun (α : Type) (makeFunctionType : outParam (α → Type)) where
coe : (x : α) → makeFunctionType x두 번째 매개변수는 그 자체로 타입을 계산하는 함수입니다. Lean에서 타입은 일급 값이므로, 다른 모든 것과 마찬가지로 함수에 전달하거나 함수에서 반환할 수 있습니다.
예를 들어, 인자에 일정한 값을 더하는 함수는 실제 함수를 정의하는 대신 더할 값을 감싸는 래퍼로 표현할 수 있습니다:
structure Adder where
howMuch : Nat
인자에 5를 더하는 함수의 howMuch 필드에는 5가 들어 있습니다:
def add5 : Adder := ⟨5⟩
이 Adder 타입은 함수가 아니므로 인자에 적용하면 오류가 발생합니다:
#eval add5 3
CoeFun 인스턴스를 정의하면 Lean은 덧셈기를 Nat → Nat 타입의 함수로 변환합니다:
instance : CoeFun Adder (fun _ => Nat → Nat) where
coe a := (· + a.howMuch)#eval add5 3
모든 Adder는 Nat → Nat 함수로 변환되어야 하므로, CoeFun의 두 번째 매개변수에 전달된 인자는 무시되었습니다.
올바른 함수 타입을 결정하는 데 값 자체가 필요한 경우에는 CoeFun의 두 번째 매개변수가 더 이상 무시되지 않습니다. 예를 들어, JSON 값을 다음과 같이 표현한다고 합시다:
inductive JSON where
| true : JSON
| false : JSON
| null : JSON
| string : String → JSON
| number : Float → JSON
| object : List (String × JSON) → JSON
| array : List JSON → JSONJSON 직렬화기는 자신이 직렬화할 수 있는 타입과 직렬화 코드 자체를 함께 추적하는 구조체입니다:
structure Serializer where
Contents : Type
serialize : Contents → JSON
문자열 직렬화기는 주어진 문자열을 JSON.string 생성자로 감싸기만 하면 됩니다:
def Str : Serializer :=
{ Contents := String,
serialize := JSON.string
}JSON 직렬화기를 자신의 인자를 직렬화하는 함수로 보려면 직렬화 가능한 데이터의 내부 타입을 추출해야 합니다:
instance : CoeFun Serializer (fun s => s.Contents → JSON) where
coe s := s.serialize이 인스턴스가 있으면 직렬화기를 인자에 직접 적용할 수 있습니다:
def buildResponse (title : String) (R : Serializer)
(record : R.Contents) : JSON :=
JSON.object [
("title", JSON.string title),
("status", JSON.number 200),
("record", R record)
]
이 직렬화기는 buildResponse에 직접 전달할 수 있습니다:
#eval buildResponse "Functional Programming in Lean" Str "Programming is fun!"3.6.6.1. 여담: 문자열로서의 JSON
JSON이 Lean 객체로 인코딩되어 있으면 이해하기가 다소 어려울 수 있습니다. 직렬화된 응답이 예상한 대로인지 확인하는 데 도움이 되도록 JSON을 String으로 변환하는 간단한 변환기를 작성해 두면 편리할 수 있습니다. 첫 번째 단계는 숫자 표시를 단순화하는 것입니다. JSON은 정수와 부동소수점 수를 구별하지 않으며, 둘 다 Float 타입으로 표현합니다. Lean에서 Float.toString의 결과에는 뒤따르는 0이 여러 개 포함됩니다:
#eval (5 : Float).toString해결책은 뒤따르는 0을 모두 제거하고 그 뒤에 남는 소수점까지 제거하여 표시를 깔끔하게 정리하는 작은 함수를 작성하는 것입니다:
def dropDecimals (numString : String) : String :=
if numString.contains '.' then
let noTrailingZeros := numString.dropEndWhile (· == '0')
(noTrailingZeros.dropEndWhile (· == '.')).copy
else numString
이 정의를 사용하면 dropDecimals (5 : Float).toString의 결과는 5이고, dropDecimals (5.2 : Float).toString의 결과는 5.2입니다.
다음 단계는 문자열 리스트의 각 문자열 사이에 구분자를 넣어 이어 붙이는 보조 함수를 정의하는 것입니다:
def String.separate (sep : String) (strings : List String) : String :=
match strings with
| [] => ""
| x :: xs => String.join (x :: xs.map (sep ++ ·))
이 함수는 JSON 배열과 객체에서 쉼표로 구분된 요소를 처리할 때 유용합니다. ", ".separate ["1", "2"]의 결과는 "1, 2"이고, ", ".separate ["1"]의 결과는 "1"이며, ", ".separate []의 결과는 ""입니다. Lean 표준 라이브러리에서는 이 함수를 String.intercalate라고 부릅니다.
마지막으로, JSON 문자열을 위한 문자열 이스케이프 절차가 필요합니다. 그래야 "Hello!"를 담은 Lean 문자열을 "\"Hello!\""로 출력할 수 있습니다. 다행히 Lean 컴파일러에는 JSON 문자열을 이스케이프하는 내부 함수 Lean.Json.escape가 이미 들어 있습니다. 이 함수를 사용하려면 파일 맨 앞에 import Lean을 추가하십시오.
JSON 값에서 문자열을 만들어 내는 함수는 Lean이 이 함수가 종료된다는 사실을 알 수 없기 때문에 partial로 선언되어 있습니다. asString에 대한 재귀 호출이 List.map이 적용하는 함수 안에서 일어나는데, 이 재귀 패턴이 꽤 복잡해서 Lean은 재귀 호출이 실제로 더 작은 값에 대해 수행된다는 것을 알아낼 수 없기 때문입니다. JSON 문자열을 생성하기만 하면 되고 그 과정을 수학적으로 추론할 필요가 없는 애플리케이션에서는 함수가 partial이더라도 문제가 생길 가능성이 낮습니다.
partial def JSON.asString (val : JSON) : String :=
match val with
| true => "true"
| false => "false"
| null => "null"
| string s => "\"" ++ Lean.Json.escape s ++ "\""
| number n => dropDecimals n.toString
| object members =>
let memberToString mem :=
"\"" ++ Lean.Json.escape mem.fst ++ "\": " ++ asString mem.snd
"{" ++ ", ".separate (members.map memberToString) ++ "}"
| array elements =>
"[" ++ ", ".separate (elements.map asString) ++ "]"이 정의를 사용하면 직렬화 출력을 더 쉽게 읽을 수 있습니다:
#eval (buildResponse "Functional Programming in Lean" Str "Programming is fun!").asString3.6.7. 마주칠 수 있는 메시지
자연수 리터럴은 OfNat 타입 클래스를 통해 오버로딩됩니다. 강제 변환은 인스턴스가 없는 경우가 아니라 타입이 일치하지 않는 경우에 일어나므로, 어떤 타입에 대한 OfNat 인스턴스가 없다고 해서 Nat으로부터의 강제 변환이 적용되지는 않습니다:
def perhapsPerhapsPerhapsNat : Option (Option (Option Nat)) :=
3923.6.8. 설계 고려 사항
강제 변환은 책임감 있게 사용해야 하는 강력한 도구입니다. 한편으로 강제 변환을 사용하면 API가 모델링 대상 도메인의 일상적인 규칙을 자연스럽게 따르도록 할 수 있습니다. 이는 수동 변환 함수가 뒤엉킨 관료적인 혼란과 명료한 프로그램을 가르는 차이가 될 수 있습니다. Abelson과 Sussman이 Structure and Interpretation of Computer Programs (MIT Press, 1996)의 서문에서 썼듯이,
프로그램은 사람이 읽을 수 있도록 작성되어야 하며, 기계가 실행하는 것은 부차적인 일일 뿐입니다.
강제 변환을 현명하게 사용하면 가독성 높은 코드를 작성할 수 있으며, 그러한 코드는 도메인 전문가와 소통하는 기반이 될 수 있습니다. 강제 변환은 이를 위한 귀중한 수단입니다. 하지만 강제 변환에 크게 의존하는 API에는 몇 가지 중요한 한계가 있습니다. 직접 작성하는 라이브러리에서 강제 변환을 사용하기 전에 이러한 한계를 신중하게 검토하십시오.
우선, 강제 변환 타입 클래스에는 출력 매개변수가 없기 때문에 강제 변환은 Lean이 관련된 모든 타입을 알 수 있을 만큼 타입 정보가 충분한 맥락에서만 적용됩니다. 따라서 함수에 반환 타입 표기가 있느냐 없느냐에 따라 타입 오류가 발생할 수도 있고, 강제 변환이 성공적으로 적용될 수도 있습니다. 예를 들어, 비어 있지 않은 리스트에서 리스트로의 강제 변환 덕분에 다음 프로그램이 동작합니다:
def lastSpider : Option String :=
List.getLast? idahoSpiders반면 타입 표기를 생략하면 결과 타입을 알 수 없으므로 Lean은 강제 변환을 찾을 수 없습니다:
def lastSpider :=
List.getLast? idahoSpiders더 일반적으로 말하면, 어떤 이유로 강제 변환이 적용되지 않으면 사용자는 원래의 타입 오류를 받게 되며, 이 때문에 연쇄된 강제 변환을 디버깅하기가 어려워질 수 있습니다.
마지막으로, 필드 접근자 표기법의 맥락에서는 강제 변환이 적용되지 않습니다. 이는 강제 변환이 필요한 표현식과 그렇지 않은 표현식 사이에 여전히 중요한 차이가 있으며, 이 차이가 여러분이 만든 API의 사용자에게 드러난다는 것을 의미합니다.