3.6. 강제 변환
수학에서는 어떤 대상의 서로 다른 측면을 나타내기 위해 문맥에 따라 같은 기호를 사용하는 것이 흔합니다. 예를 들어 집합이 기대되는 맥락에서 환(ring)이 참조된다면, 그 환의 밑바탕 집합(underlying set)이 의도된 것으로 이해됩니다. 프로그래밍 언어에서는 한 타입의 값을 다른 타입의 값으로 자동 변환하는 규칙을 두는 것이 일반적입니다. Java는 byte가 int로 자동 승격되는 것을 허용하며, Kotlin은 널이 될 수 없는 타입을 널이 될 수 있는 버전의 타입을 기대하는 문맥에서 사용하는 것을 허용합니다.
Lean에서는 강제 변환이라는 메커니즘을 통해 두 가지 목적이 모두 충족됩니다. Lean은 어떤 타입의 표현식이 다른 타입을 기대하는 문맥에서 발견되면, 타입 오류를 보고하기 전에 해당 표현식을 강제 변환하려고 시도합니다. Java, C, Kotlin과 달리, 강제 변환은 타입 클래스의 인스턴스를 정의하여 확장할 수 있습니다.
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 α 타입을 가지며, 목록의 앞부분을 제거합니다. 그러나 Pos에 List.drop을 적용하면 타입 오류가 발생합니다:
[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의 축약형입니다. Repr B 인스턴스를 deriving instance Repr for B로 파생시킨 후,
#eval coercedToB결과는 다음과 같습니다:
Option 타입은 C#과 Kotlin의 nullable 타입과 비슷하게 사용할 수 있습니다. none 생성자는 값의 부재를 나타냅니다. Lean 표준 라이브러리는 임의의 타입 α에서 값을 some으로 감싸는 Option α로의 강제 변환을 정의합니다. 이를 통해 옵션 타입을 널 허용 타입과 더 유사한 방식으로 사용할 수 있는데, some을 생략할 수 있기 때문입니다. 예를 들어, 리스트의 마지막 항목을 찾는 함수 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 α β의 인스턴스는 타입 β가 타입 α의 각 값을 나타낼 수 있는 값을 가질 때 의미가 있습니다. Nat에서 Int로의 강제 변환은 타당한데, 이는 Int 타입이 모든 자연수를 포함하기 때문입니다. 하지만 Int에서 Nat로의 강제 변환은 좋지 않은 생각인데, 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는 모노이드의 "받침 집합(carrier set)"이라고 불립니다. 0과 덧셈을 갖춘 자연수는 모노이드를 이룹니다. 덧셈은 결합적이고, 어떤 수에 0을 더하는 것도 항등원이기 때문입니다. 마찬가지로, 1과 곱셈을 가진 자연수 또한 모노이드를 이룹니다. 모노이드는 함수형 프로그래밍에서도 널리 사용됩니다. 리스트, 빈 리스트, 그리고 이어붙이기(append) 연산자가 모노이드를 이루며, 문자열, 빈 문자열, 그리고 문자열 이어붙이기 역시 마찬가지입니다.
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의 원소라 하자"라고 말하는 것이 일반적입니다. 이러한 관행은 모노이드에서 그 반송 집합(carrier set)으로의 새로운 종류의 강제 변환을 정의함으로써 Lean에서 인코딩할 수 있습니다.
CoeSort 클래스는 Coe 클래스와 거의 같지만, 강제 변환의 대상이 반드시 소트, 즉 Type 또는 Prop이어야 한다는 점에서 차이가 있습니다. Lean에서 sort라는 용어는 다른 타입을 분류하는 이러한 타입들을 가리킵니다—Type은 그 자체로 데이터를 분류하는 타입들을 분류하고, Prop은 그 자체로 참임을 나타내는 증거를 분류하는 명제들을 분류합니다. Coe가 타입 불일치가 발생할 때 검사되는 것과 마찬가지로, CoeSort는 정렬(sort)이 예상되는 문맥에서 정렬이 아닌 다른 것이 제공될 때 사용됩니다.
모노이드에서 그 캐리어 집합으로의 강제 변환은 캐리어를 추출합니다:
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
이 경우 문제가 되는 소트는 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이 adder를 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라고 불립니다.
마지막으로, "Hello!"를 포함하는 Lean 문자열이 "\"Hello!\""로 출력될 수 있도록 JSON 문자열을 위한 문자열 이스케이프 절차가 필요합니다. 다행히도 Lean 컴파일러에는 JSON 문자열을 이스케이프하기 위한 내부 함수가 이미 존재하며, 이는 Lean.Json.escape라고 불립니다. 이 함수에 접근하려면 파일 맨 앞에 import Lean을 추가하십시오.
JSON 값에서 문자열을 만들어내는 함수는 partial로 선언되는데, 이는 Lean이 이 함수가 종료됨을 알 수 없기 때문입니다. 이는 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 사용자에게 드러난다는 것을 의미합니다.