사용 분석에 의한 소거
사용 분석에 의한 소거 (Erasure By Usage Analysis)
이 작업은 이 기능 제안(이 페이지에 의해 폐기됨)에서 시작됐어요. 제안 속의 정보는 시대에 뒤처졌으며 — 때로는 최종 구현과 직접 모순되기도 하니 — 주의하세요.
출처: 문서
본문
동기 (Motivation)
전통적인 의존 타입 언어(Agda, Coq)는 증명을 지우는 데 능숙해요 (비관련성(irrelevance)이나 추가 유니버스를 통해).
half : (n : Nat) -> Even n -> Nat
half Z EZ = Z
half (S (S n)) (ES pf) = S (half n pf)
예를 들어 위 스니펫에서 두 번째 인자는 증명인데, 그것은 단지 함수가 전체(total)임을 컴파일러에게 납득시키는 데만 사용돼요. 이 증명은 런타임에 결코 검사되지 않으므로 지울 수 있어요. 이 경우, 증명의 단순한 존재만으로 충분하며, 소거를 얻기 위해 비관련성 관련 방법을 사용할 수 있어요.
그러나 때로는 인덱스(index)를 지우고 싶을 때가 있어요. 그리고 전통적인 접근이 쓸모없게 되는 곳이 바로 여기예요. 주로 원래 제안에 기술된 이유 때문이에요.
uninterleave : {n : Nat} -> Vect (n * 2) a -> (Vect n a, Vect n a)
uninterleave [] = ([] , [])
uninterleave (x :: y :: rest) with (unzipPairs rest)
| (xs, ys) = (x :: xs, y :: ys)
이 경우 두 번째 인자가 중요한 것이고, 프로그램의 모양은 일반적으로 이전 경우와 같지만, 대신 n을 없애고 싶다는 점을 주목하세요.
Brady, McBride, McKinna가 [BMM04]에서 기술한, 데이터 구조에서 인덱스를 제거하는 방법이 있어요. 이것은 그들 위에서 작동하는 함수들이 이미 적절한 인덱스의 복사본을 가지고 있거나, 필요할 때 인덱스를 빠르게 재구성할 수 있다는 사실을 활용해요.
그러나 우리는 재구성이 불가능한 경우조차, 전체 프로그램에서 인덱스를 완전히 지우고 싶어하는 경우가 많아요. 다음 두 섹션은 그렇게 함으로써 런타임 성능이 점근적으로(asymptotically) 향상되는 두 경우를 설명해요.
이진수 (Binary numbers)
- O(log n) 대신 O(n)
Nat로 인덱스된, 이진수를 나타내는 다음 타입 패밀리를 고려해보세요:
data Bin : Nat -> Type where
N : Bin 0
O : {n : Nat} -> Bin n -> Bin (0 + 2*n)
I : {n : Nat} -> Bin n -> Bin (1 + 2*n)
이것들은 (적어도 점근적으로는) 빠르고 메모리 효율적이 되어야 하는데, 그 크기가 그것들이 나타내는 숫자에 비해 로그적(logarithmic)이기 때문이에요.
안타깝게도 그렇지 않아요. 문제는 이 이진수들이 여전히 단항(unary) 인덱스들을 갖고 다니며, 이진수 자체에 대해 산술이 행해질 때마다 인덱스에 대한 산술도 수행한다는 거예요. 따라서 15라는 숫자의 실제 표현은 다음과 같아 보여요:
I -> I -> I -> I -> N
S S S Z
S S Z
S S
S Z
S
S
S
Z
사용되는 메모리는 실제로 선형이며 로그적이지 않으므로, 시간 복잡도에서 O(n) 아래로 내려갈 수 없어요.
Idris가 실제로 Nat을 GMP로 컴파일한다고 주장할 수도 있겠지만, 그것은 두 가지 이유로 무의미한 주장이에요:
- 첫째,
Nat이외의 것으로 데이터 구조를 인덱스하려고 하면, 컴파일러가 구원해주지 않아요. - 둘째,
Nat의 경우조차 GMP 정수는 여전히 존재하며 런타임을 느리게 해요.
Nat이 런타임에 절대 사용되지 않고 타입 체킹 목적으로만 존재하므로 이렇게 되면 안 돼요. 따라서 그것들을 없애고, Idris 프로그래머가 쓰는 것과 유사한 런타임 코드를 얻어야 해요.
리스트의 U-뷰 (U-views of lists)
- O(n) 대신 O(n^2)
리스트의 U-뷰 타입을 고려해보세요:
data U : List a -> Type where
nil : U []
one : (z : a) -> U [z]
two : {xs : List a} -> (x : a) -> (u : U xs) -> (y : a) -> U (x :: xs ++ [y])
더 나은 직관을 위해, [x0,x1,x2,z,y2,y1,y0]의 U-뷰의 모양은 다음과 같아요:
x0 y0 (two)
x1 y1 (two)
x2 y2 (two)
z (one)
이 구조를 재귀할 때, xs의 값들은 [x0,x1,x2,z,y2,y1,y0], [x1,x2,z,y2,y1], [x2,z,y2], [z]에 걸쳐 있어요. 이 리스트들이 저장되든 요청 시 만들어지든, 그것들은 노드를 공유할 수 없으므로 2차(quadratic) 양의 메모리를 차지해요. 따라서 이 인덱스만의 값을 만드는 데에도 2차의 시간이 걸려요.
그러나 합리적인 기대는 U-뷰로 하는 연산이 선형 시간이 걸린다는 거예요 — 그래서 이 목표를 달성하려면 인덱스 xs를 지워야 해요.
Idris에 대한 변경 (Changes to Idris)
사용 분석(usage analysis)은 매 컴파일마다 실행되며, 그 출력은 여러 목적으로 사용돼요. 이것은 실제로 사용자에게는 보이지 않지만, 상대적으로 크고 중요한 변경이며, 새로운 기능들을 가능하게 해요.
사용되지 않는 것으로 발견된 모든 것이 지워져요. 어떤 주석도 필요 없어요. 그냥 그 객체를 사용하지 않으면 생성된 코드에서 사라질 거예요. 그러나 원한다면, 그 객체가 우연히 사용되었을 때 경고를 받기 위해 점(dot) 주석을 사용할 수 있어요.
이 맥락에서 "사용된다"는 것은 그 "객체"의 값이 프로그램의 런타임 동작에 영향을 줄 수 있다는 뜻이에요. (더 정확히는, 사용 분석 알고리즘에 의해 런타임 동작에 비관련적이라고 발견되지 않았다는 뜻이에요.)
소거에 의해 제거 후보로 고려되는 "객체들"에는 다음이 포함돼요:
- 함수 인자
- 데이터 생성자 필드 (레코드 필드와 인터페이스 구현의 사전(dictionary) 필드 포함)
예를 들어, Either은 종종 Bool과 같은 런타임 표현으로 컴파일돼요. 생성자 필드 제거는 때로 newtype 최적화와 결합해 꽤 강한 효과를 내요.
--warnreach라는 새로운 컴파일러 옵션이 있어요. 이것은 소거에서 오는 경고를 활성화해요. 완전한 사용 분석이 있으므로, 소거 주석을 위반하는 프로그램조차 컴파일할 수 있어요 — 단지 바이너리가 예상보다 느리게 실행될 뿐이에요. 경고는 미래의 Idris 버전에서 기본으로 활성화될 거예요 (가능하면 오류로 바뀔 수도 있어요). 그러나 이 과도기 동안에는, 더 나은 문서가 쓰여질 때까지 혼란을 피하기 위해 경고를 요청 시에만 열어두기로 했어요.
case-트리 정교화(case-tree elaboration)는 가능할 때마다 점이 찍힌 "객체들"을 사용하는 것을 피하려 해요. (주: 이것은 아직 완벽하지 않으며 작업 중이에요: https://gist.github.com/ziman/10458331)
포스튤레이트(postulates)는 더 이상 접을 수 있어야(collapsible) 하지 않아요. 이제는 대신 사용되지 않아야 해요.
언어에 대한 변경 (Changes to the language)
점(dot)을 사용해 런타임에 사용할 의도가 없는 필드를 표시할 수 있어요.
data Bin : Nat -> Type where
N : Bin 0
O : .{n : Nat} -> Bin n -> Bin (0 + 2*n)
I : .{n : Nat} -> Bin n -> Bin (1 + 2*n)
이 필드들이 런타임에 사용되는 것으로 발견되면, 점은 경고를 유발해요 (--warnreach와 함께).
자유(묶이지 않은) 묵시적 인자는 기본적으로 점이 찍히므로, 예를 들어 생성자 O는 다음과 같이 정의할 수 있어요:
O : Bin n -> Bin (0 + 2*n)
그리고 이것이 실제로 선호되는 형태예요.
런타임에 사용되도록 의도된 자유 묵시적 인자가 있다면, 그것을 (점이 없는) {bound : implicit}으로 바꿔야 해요.
더 많은 보장을 얻기 위해 함수 타입에도 점을 넣을 수 있어요.
half : (n : Nat) -> .(pf : Even n) -> Nat
여기서도 자유 묵시적 인자는 자동으로 점이 찍혀요.
그것이 의미하는 것 (What it means)
점 주석은 두 가지 목적을 제공해요:
- 점이 찍힌 변수를 피하도록 case-트리 정교화에 영향을 줌
- 점이 찍힌 변수가 사용될 때 경고를 유발함
그러나 점이 찍혔는지와 지워졌는지 사이에 직접적인 연결은 없어요. 컴파일러는 점이 찍혔든 아니든 가능한 모든 것을 지워요. 점은 주로 프로그래머(와 컴파일러)가 지우고 싶은 값들의 사용을 자제하게 도와주기 위해 있어요.
사용하는 방법 (How to use it)
이상적으로는 추가 주석이 거의 또는 전혀 필요하지 않아요 – 실제로는 자유 묵시적 인자가 자동으로 점이 찍히는 것으로 충분히 좋은 소거를 얻을 수 있다는 것이 밝혀졌어요.
따라서 그냥 --warnreach로 컴파일해서 소거가 프로그램의 일부를 제거하지 못하는지 경고를 보면 돼요.
그러나 런타임 동작을 고려하지 않고 작성된 프로그램들은 합리적인 바이너리로 컴파일되는 형태를 얻기 위해 약간의 도움이 필요할 거예요. 일반적으로 소거 경고(가끔은 지금은 도움이 안 될 수도 있지만)를 따르는 것으로 충분해요.
벤치마크 (Benchmarks)
소거에 의해 점근성이 향상되는 것을 분명히 볼 수 있어요.
단점 (Shortcomings)
사용 분석이 Main.main에서 시작하므로 라이브러리에서는 경고를 받을 수 없어요. 이것은 계획된 %default_usage 프래그마로 해결될 거예요.
사용 경고는 현재 꽤 나쁘고 도움이 안 돼요. 더 많은 정보를 포함하고 적어도 인자 번호를 이름으로 변환해야 해요.
아직 제대로 된 문서가 없어요. 이 페이지가 첫 번째예요.
일반적으로 받아들여지는 용어가 없어요. 우리는 "dotted", "unused", "erased", "irrelevant", "inaccessible" 사이를 오가는데, 각각은 약간씩 다른 의미를 가져요. 더 일관되고 이해 가능한 명명이 필요해요.
같은 타입이 지워진 컨텍스트와 지워지지 않은 컨텍스트 둘 다에서 사용되면, 그것은 최소 공통 분모 — 지워지지 않은 컨텍스트 —를 수용하기 위해 필드들을 유지할 거예요. 이것은 (의존) 쌍의 타입의 경우 특히 골치 아픈데, 실제로는 어떤 소거도 수행되지 않을 것이라는 뜻이기 때문이에요. 우리는 아마도 데이터 타입의 분리된 사용을 찾아서 그것들을 "서브-타입(sub-types)"으로 나눠야 해요. 이제 의존 타입에는 세 가지 형태가 있어요: Sigma (아무것도 지워지지 않음), Exists (첫 구성요소 지워짐), Subset (두 번째 구성요소 지워짐).
case-트리 구축은 패턴 매칭된 생성자에서 오는 점이 찍힌 값들을 피하지 않아요 (https://gist.github.com/ziman/10458331). 이것은 곧 고쳐질 예정이에요. (고쳐졌어요.)
고차 함수 인자와 불투명한 함수 변수는 모든 인자를 사용하는 것으로 간주돼요. 이를 우회하려면 Erased 래퍼를 사용해 타입 시스템을 통해 소거를 강제할 수 있어요: https://github.com/idris-lang/Idris-dev/blob/master/libs/base/Data/Erased.idr
인터페이스 메서드는 모든 구현들의 합집합을 사용하는 것으로 간주돼요. 다시 말해, 메서드의 인자는 프로그램에서 발생하는 메서드의 모든 구현에서 사용되지 않는 경우에만 사용되지 않는 것이에요.
계획된 기능 (Planned features)
- 위 단점들에 대한 수정을 일반적으로.
- case-트리 정교화기에 대한 개선으로 데이터 생성자의 점이 찍힌 필드를 제대로 피하기. 끝났어요.
- 컴파일러 프래그마
%default_usage(used/unused)와 함수별 재정의(used와 unused)로, 프로그래머가 함수의 반환 값을 사용됨(used)으로 표시할 수 있게 해줘요. 함수가 main에서 사용되지 않더라도(라이브러리 코드를 쓸 때 그렇듯) 말이에요. 이 주석들은 라이브러리 작성자가 코드를 실제로 발표하고 컴파일된 프로그램에서 사용하기 전에 코드의 사용 위반을 발견하는 데 도움이 될 거예요.
문제 해결 (Troubleshooting)
내 프로그램이 더 느려요
사용 분석에 의한 소거를 도입한 패치는 그 전에 있던 일부 최적화도 비활성화했어요; 그것들은 새로운 소거에 포함되어요. 그러나 소거를 인식하지 못하는 일부 프로그램에서는, 사용 분석에 의한 소거가 완전한 잠재력을 발휘하지 못할 때(하지만 이전 최적화가 작동했을 때는), 런타임에 필요하지 않아야 할 정보의 보유와 계산으로 인해 특정 속도 저하(예비 벤치마킹에 따르면 최대 ~10%)가 관찰될 수 있어요.
이것이 그 경우인지 확인하는 간단한 방법은 --warnreach로 컴파일하는 것이에요. 경고가 보이면, 불필요한 코드가 바이너리로 컴파일되고 있는 것이에요.
해결책은 경고가 없도록 코드를 바꾸는 것이에요.
사용 경고가 도움이 안 돼요
이것은 알려진 이슈이며 작업 중이에요. 지금은, 소거 경고를 읽고 해결하는 방법 섹션을 보세요.
이 함수에는 경고가 없어야 해요
가능한 원인은 함수의 비-전체성(non-totality)(더 정확히는 비-커버링(non-coverage))이에요. 함수가 non-covering이면, 프로그램은 런타임에 커버리지 실패를 감지하기 위해 모든 인자를 검사해야 해요. 함수가 모든 인자를 검사하므로, 어떤 것도 지울 수 없고, 이것은 전이적으로 사용 위반을 일으킬 수 있어요. 해결책은 함수를 total로 만들거나, 인자를 사용한다는 사실을 받아들이고 적절한 생성자 필드와 함수 인자에서 일부 점을 제거하는 것이에요. (이것은 소거의 단점이 아니며 우리가 할 수 있는 일이 없다는 점을 주의하세요.)
또 다른 가능한 원인은 현재 불완전한 case-트리 정교화인데, 그것은 점이 찍힌 생성자 필드를 피하지 않아요 (https://gist.github.com/ziman/10458331 참조). 함수를 바꾸거나 곧, 바라건대 좋아질 때까지 기다리면 돼요. 고쳐졌어요.
컴파일러가 이 객체를 지워진 것으로 인식하지 못해요
Erased 모나드로 감싸 어떤 것이든 지워지도록 강제할 수 있어요. 이 프로그램이 사용 경고를 유발하는 반면,
f : (g : Nat -> Nat) -> .(x : Nat) -> Nat
f g x = g x -- WARNING: g uses x
다음 프로그램은 그렇지 않아요:
f : (g : Erased Nat -> Nat) -> .(x : Nat) -> Nat
f g x = g (Erase x) -- OK
소거 경고를 읽고 해결하는 방법 (How to read and resolve erasure warnings)
예시 1 (Example 1)
다음 프로그램을 고려해보세요:
vlen : Vect n a -> Nat
vlen {n = n} xs = n
sumLengths : List (Vect n a) -> Nat
sumLengths [] = 0
sumLengths (v :: vs) = vlen v + sumLengths vs
main : IO ()
main = print . sumLengths $ [[0,1],[2,3]]
이것을 --warnreach로 컴파일하면 경고가 하나 있어요:
Main.sumLengths: inaccessible arguments reachable:
n (no more information available)
이 시점에서 경고는 세부 정보를 많이 포함하지 않으므로, --dumpcases cases.txt로 컴파일해 cases.txt에서 컴파일된 정의를 찾아볼 수 있어요:
Main.sumLengths {e0} {e1} {e2} =
case {e2} of
| Prelude.List.::({e6}) => LPlus (ATInt ITBig)({e0}, Main.sumLengths({e0}, ____, {e6}))
| Prelude.List.Nil() => 0
경고의 이유는 sumLengths가 인라인되는 vlen을 호출하기 때문이에요. 그러면 sumLengths의 두 번째 절은 {e0}으로 컴파일된 변수 n에 접근해요. n은 자유 묵시적 인자이므로 자동으로 점이 찍힌 것으로 간주되고, 이것이 경고를 유발해요.
해결책은 인자 n을 묶인 묵시적 매개변수로 만들어 런타임에 유지하고 싶다는 것을 나타내는 것이거나,
sumLengths : {n : Nat} -> List (Vect n a) -> Nat
vlen을 인덱스를 사용하지 않도록 고치는 것이에요:
vlen : Vect n a -> Nat
vlen [] = Z
vlen (x :: xs) = S (vlen xs)
어느 해결책이 적절한지는 사용 사례에 달려 있어요.
예시 2 (Example 2)
값으로 인덱스된 이진수를 조작하는 다음 프로그램을 고려해보세요.
data Bin : Nat -> Type where
N : Bin Z
O : Bin n -> Bin (0 + n + n)
I : Bin n -> Bin (1 + n + n)
toN : (b : Bin n) -> Nat
toN N = Z
toN (O {n} bs) = 0 + n + n
toN (I {n} bs) = 1 + n + n
main : IO ()
main = print . toN $ I (I (O (O (I N))))
함수 toN에서 우리는 "속임수"를 시도했어요. 전체 구조를 순회하는 대신, 생성자 I와 O에서 값 인덱스 n을 그냥 투영(project)했어요. 그러나 이 인덱스는 자유 묵시적 인자이므로 점이 찍힌 것으로 간주돼요.
그것을 검사하면 --warnreach로 컴파일할 때 다음 경고가 생겨요:
Main.I: inaccessible arguments reachable:
n from Main.toN arg# 1
Main.O: inaccessible arguments reachable:
n from Main.toN arg# 1
I와 O 둘 다의 인자 n이 함수 toN, 인자 1에서 사용되는 것을 볼 수 있어요.
개발의 이 단계에서 경고는 인자 이름이 아니라 번호만 포함해요; 이것은 바라건대 고쳐질 거예요. 인자에 번호를 매길 때, 우리는 0부터 시작하며, 자유 묵시적 인자를 먼저, 왼쪽에서 오른쪽으로; 그 다음 묶인 인자를 번호를 매겨요. 따라서 toN 함수는 실제로 두 개의 인자를 가져요: n (인자 0)과 b (인자 1). 그리고 실제로, 경고가 말하듯이, 우리는 b에서 점이 찍힌 필드를 투영해요.
다시 말해, 해결책 중 하나는 toN 함수를 결과를 정직하게 계산하도록 고치는 것이에요; 다른 하나는 Bin의 모든 생성자와 함께 Nat을 운반한다는 것을 받아들이고 그것을 묶인 묵시적으로 만드는 것이에요:
O : {n : Nat} -> Bin n -> Bin (0 + n + n)
I : {n : Nat} -> bin n -> Bin (1 + n + n)
참고문헌 (References)
[BMM04] Edwin Brady, Conor McBride, James McKinna: Inductive families need not store their indices