3.6. Coercions
수학에서는 문맥에 따라 한 객체의 서로 다른 측면을 같은 기호로 나타내는 일이 흔하다.
예를 들어 집합을 기대하는 문맥에서 환을 가리키면 환의 바탕 집합을 뜻한다고 이해한다.
프로그래밍 언어에서는 한 타입의 값을 다른 타입의 값으로 자동 변환하는 규칙을 두는 일이 흔하다.
Java에서는 byte를 int로 자동 승격할 수 있고, Kotlin에서는 nullable 타입을 기대하는 문맥에 non-nullable 타입을 사용할 수 있다.
Lean에서는 이 두 목적을 강제 변환이라는 메커니즘으로 달성한다. Lean은 다른 타입을 기대하는 문맥에서 한 타입의 표현식을 만나면 타입 오류를 보고하기 전에 표현식을 강제 변환하려 한다. Java, C, Kotlin과 달리 강제 변환은 타입 클래스 인스턴스를 정의해 확장할 수 있다.
3.6.1. Strings and Paths
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. Positive Numbers
모든 양수에는 대응하는 자연수가 있다.
앞서 정의한 Pos.toNat 함수는 Pos를 대응하는 Nat으로 변환한다.
def Pos.toNat : Pos → Nat
| Pos.one => 1
| Pos.succ n => n.toNat + 1
{α : Type} → Nat → List α → List α 타입의 List.drop 함수는 리스트의 접두사를 제거한다.
그러나 Pos에 List.drop을 적용하면 타입 오류가 난다.
[1, 2, 3, 4].drop (2 : Pos)
List.drop의 작성자가 이를 타입 클래스 메서드로 만들지 않았으므로 새 인스턴스를 정의해 오버라이딩할 수 없다.
3.6.3. Chaining Coercions
강제 변환을 검색할 때 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 표준 라이브러리는 임의의 타입 α에서 값을 some으로 감싸는 Option α로의 강제 변환을 정의한다.
따라서 some을 생략해 nullable 타입과 더 비슷하게 Option 타입을 사용할 수 있다.
예를 들어 리스트의 마지막 원소를 찾는 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"강제 변환은 추론된 타입과 프로그램 나머지에서 부과된 타입이 불일치할 때만 자동으로 활성화된다. 다른 오류가 있는 경우에는 강제 변환이 활성화되지 않는다. 예를 들어 인스턴스가 없다는 오류에는 강제 변환을 사용하지 않는다.
def perhapsPerhapsPerhapsNat : Option (Option (Option Nat)) :=
3923.6.4. Non-Empty Lists and Dependent Coercions
β 타입에 α의 모든 값을 표현할 수 있는 값이 있을 때 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. Coercing to Types
수학에서는 추가 구조를 갖춘 집합으로 이루어진 개념을 자주 사용한다.
예를 들어 모노이드는 집합 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 클래스는 강제 변환의 대상이 sort, 즉 Type이나 Prop이어야 한다는 점을 제외하면 Coe 클래스와 같다.
Lean에서 sort는 다른 타입을 분류하는 타입을 뜻한다. Type은 데이터를 분류하는 타입을 분류하고, Prop은 참이라는 증거를 분류하는 명제를 분류한다.
타입 불일치가 발생할 때 Coe를 검사하듯, sort를 기대하는 문맥에 sort가 아닌 것이 주어지면 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이 아니라 결정 가능한 명제를 기대한다.
하지만 프로그램은 보통 불리언 값에 따라 분기해야 한다.
if 표현식을 두 종류로 나누는 대신 Lean 표준 라이브러리는 Bool에서 해당 Bool이 true와 같다는 명제로의 강제 변환을 정의한다.
instance : CoeSort Bool Prop where
coe b := b = true
이 경우 해당 sort는 Type이 아니라 Prop이다.
3.6.6. Coercing to Functions
프로그래밍에서 자주 등장하는 많은 데이터 타입은 함수와 그 함수에 관한 추가 정보로 이루어진다.
예를 들어 함수에 로그에 표시할 이름이나 구성 데이터가 함께 있을 수 있다.
또한 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. Aside: JSON as a String
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. Messages You May Meet
자연수 리터럴은 OfNat 타입 클래스로 오버로딩된다.
강제 변환은 인스턴스가 없을 때가 아니라 타입이 일치하지 않을 때 작동하므로, 타입에 OfNat 인스턴스가 없어도 Nat에서의 강제 변환이 적용되지는 않는다.
def perhapsPerhapsPerhapsNat : Option (Option (Option Nat)) :=
3923.6.8. Design Considerations
강제 변환은 책임 있게 사용해야 하는 강력한 도구다. 한편 강제 변환은 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 사용자에게도 이 차이가 보인다.