정적 인자와 부분 평가
정적 인자와 부분 평가 (Static Arguments and Partial Evaluation)
버전 0.9.15부터 Idris는 정적으로 알려진 인자(statically known arguments)의 부분 평가(partial evaluation)를 지원해요. 이는 %static으로 주석이 달린 인자를 가진 함수의 특수화된 버전을 만드는 작업을 포함해요.
(이것은 이 ICFP 2010 논문에 기술된 부분 평가기의 한 구현이에요. 뒤따르는 내용의 더 정밀한 정의는 그 논문을 참조하세요.)
부분 평가는 Idris 1.0부터 기본적으로 꺼져 있어요. 그것은 --partial-eval 플래그로 활성화할 수 있어요.
출처: 문서
본문
입문 예시 (Introductory Example)
자연수에 대한 거듭제곱 함수를 고려해보세요 (Prelude에 pow가 이미 있으므로 my_pow라고 부를게요):
my_pow : Nat -> Nat -> Nat
my_pow x Z = 1
my_pow x (S k) = mult x (my_pow x k)
이것은 두 번째 인자에 대한 재귀로 구현돼요. 그리고 두 번째 인자가 알려져 있다면, 첫 번째가 알려지지 않았더라도 정의를 더 평가할 수 있어요. 예를 들어, REPL에서 수를 세제곱하는 함수를 다음과 같이 만들 수 있어요.
*pow> \x => my_pow x 3
\x => mult x (mult x (mult x 1)) : Nat -> Nat
*pow> it 3
27 : Nat
결과 함수에서 재귀가 제거되었음을 주목하세요. my_pow가 알려진 인자에 대한 재귀로 구현되기 때문이에요. 첫 번째 인자가 알려지고 두 번째가 알려지지 않았다면 그런 운은 없어요:
*pow> \x => my_pow 2 x
\x => my_pow 2 x : Nat -> Nat
이제 x^2 + 1을 계산하는 다음 정의를 고려해보세요:
powFn : Nat -> Nat
powFn x = plus (my_pow x (S (S Z))) (S Z)
여기서 my_pow의 두 번째 인자는 정적으로 알려져 있으므로, 매번 재귀 호출을 해야 한다는 것은 아쉬운 일이에요. 그러나 Idris는 일반적으로 재귀 정의를 인라인하지 않아요. 특히 더 깊은 분석 없이는 발산하거나 작업을 중복할 수 있기 때문이에요. 하지만 여기서 정말로 my_pow의 특수화된 버전을 만들고 싶다는 힌트를 Idris에 줄 수 있어요.
pow의 자동 특수화 (Automatic specialisation of pow)
요령은 정적으로 알려진 인자를 %static 플래그로 표시하는 것이에요:
my_pow : Nat -> %static Nat -> Nat
my_pow k Z = 1
my_pow k (S j) = mult k (my_pow k j)
인자가 이런 식으로 주석이 달리면, Idris는 %static 위치에서 구체적인 값(즉 상수, 생성자 형태, 또는 전역에서 정의된 함수)을 가진 호출을 만날 때마다 특수화된 버전을 만들려고 시도해요. my_pow가 이런 식으로 정의되고, powFn이 위와 같이 정의되면, REPL에서 :printdef powFn을 입력해 그 효과를 볼 수 있어요.
*pow> :printdef powFn
powFn : Nat -> Nat
powFn x = plus (PE_my_pow_3f3e5ad8 x) 1
이 신비한 PE_my_pow_3f3e5ad8는 무엇일까요? 정적으로 알려진 인자가 특수화되어 제거된 특수화된 거듭제곱 함수예요. 그 이름은 특수화된 인자의 해시에서 생성되며, 그 정의도 :printdef로 볼 수 있어요:
*petest> :printdef PE_my_pow_3f3e5ad8
PE_my_pow_3f3e5ad8 : Nat -> Nat
PE_my_pow_3f3e5ad8 (0arg) = mult (0arg) (mult (0arg) (PE_fromInteger_7ba9767f 1))
(0arg)는 내부 인자 이름이에요 (어쨌든 프로그래머는 숫자로 시작하는 변수 이름을 줄 수 없으니까요). 또한 fromInteger의 특수화된 버전이 Nat에 대해 있음을 주목하세요. 타입 클래스 사전(type class dictionaries)이 그 자체로 정적으로 알려진 인자의 특히 흔한 경우이기 때문이에요!
타입 클래스 특수화 (Specialising Type Classes)
타입 클래스 사전은 매우 자주 정적으로 알려져 있어요. 그래서 Idris는 어떤 타입 클래스 제약도 자동으로 %static으로 표시하고, 클래스가 인스턴스화된 최상위 함수들의 특수화된 버전을 만들어요. 예를 들어, 다음이 주어졌을 때:
calc : Int -> Int
calc x = (x * x) + x
이 정의를 출력하면 +의 특수화된 버전이 사용되는 것을 볼 수 있어요:
*petest> :printdef calc
calc : Int -> Int
calc x = PE_+_954510b4 (PE_*_954510b4 x x) x
더 흥미롭게도, 수치형 벡터에서 대응하는 원소들을 더하는 vadd를 고려해보세요:
vadd : Num a => Vect n a -> Vect n a -> Vect n a
vadd [] [] = []
vadd (x :: xs) (y :: ys) = x + y :: vadd xs ys
이것을 다음과 같이 구체적인 것에 사용한다면…
test : List Int -> List Int
test xs = let xs' = fromList xs in
toList $ vadd xs' xs'
…실제로 test의 정의에서 vadd의 특수화된 버전을 얻고, 실제로 toList의 특수화된 버전도 얻어요:
test : List Int -> List Int
test xs = let xs' = fromList xs
in PE_toList_888ae67 (PE_vadd_33f98d3d xs' xs')
vadd의 특수화된 버전은 다음과 같아요:
PE_vadd_33f98d3d : Vect n Int -> Vect n Int -> Vect n Int
PE_vadd_33f98d3d [] [] = []
PE_vadd_33f98d3d (x :: xs) (y :: ys) = ((PE_+_954510b4 x y) ::
(PE_vadd_33f98d3d xs ys))
재귀 구조가 보존되고, vadd에 대한 재귀 호출이 특수화된 버전에 대한 재귀 호출로 대체되었음을 주목하세요. 또한 위의 calc에서와 같은 +의 특수화된 버전도 얻었어요.
고차 함수 특수화 (Specialising Higher Order Functions)
부분 평가가 유용할 수 있는 또 다른 경우는 고차 함수의 특수화된 버전을 자동으로 만드는 것이에요. 타입 클래스 사전과 달리, 이것은 자동으로 이루어지지 않지만, map을 다음과 같이 작성하는 것을 고려할 수 있어요:
my_map : %static (a -> b) -> List a -> List b
my_map f [] = []
my_map f (x :: xs) = f x :: my_map f xs
그러면 my_map을 사용하면 특수화된 버전이 산출돼요. 예를 들어 Int들의 리스트에서 모든 값을 두 배로 만들기 위해 다음과 같이 쓸 수 있어요:
doubleAll : List Int -> List Int
doubleAll xs = my_map (*2) xs
이것은 doubleAll에서 다음과 같이 사용되는 my_map의 특수화된 버전을 산출해요:
doubleAll : List Int -> List Int
doubleAll xs = PE_my_map_1f8225c4 xs
PE_my_map_1f8225c4 : List Int -> List Int
PE_my_map_1f8225c4 [] = []
PE_my_map_1f8225c4 (x :: xs) = ((PE_*_954510b4 x 2) :: (PE_my_map_1f8225c4 xs))
인터프리터 특수화 (Specialising Interpreters)
부분 평가가 효과적이 되는 특히 유용한 상황은 잘 타입된 표현식 언어에 대한 인터프리터를 정의하는 것이에요. 그것은 다음과 같이 정의돼요 (이것이 어떻게 작동하는지에 대한 자세한 내용은 Idris 튜토리얼 섹션 4를 참조하세요):
data Expr : Vect n Ty -> Ty -> Type where
Var : HasType i gamma t -> Expr gamma t
Val : (x : Int) -> Expr gamma TyInt
Lam : Expr (a :: gamma) t -> Expr gamma (TyFun a t)
App : Lazy (Expr gamma (TyFun a t)) -> Expr gamma a -> Expr gamma t
Op : (interpTy a -> interpTy b -> interpTy c) -> Expr gamma a -> Expr gamma
Expr gamma c
If : Expr gamma TyBool -> Expr gamma a -> Expr gamma a -> Expr gamma a
dsl expr
lambda = Lam
variable = Var
index_first = stop
index_next = pop
이 언어로 몇 가지 테스트 함수를 쓸 수 있어요. dsl 표기법을 사용해 람다를 오버로드해요; 먼저 두 입력을 곱하는 함수:
eMult : Expr gamma (TyFun TyInt (TyFun TyInt TyInt))
eMult = expr (\x, y => Op (*) x y)
그 다음, 입력의 팩토리얼을 계산하는 함수:
eFac : Expr gamma (TyFun TyInt TyInt)
eFac = expr (\x => If (Op (==) x (Val 0))
(Val 1)
(App (App eMult (App eFac (Op (-) x (Val 1)))) x))
인터프리터의 타입은 평가될 표현식을 %static으로 표시해 다음과 같이 작성돼요:
interp : (env : Env gamma) -> %static (e : Expr gamma t) -> interpTy t
즉, eFac에 대해 interp를 호출함으로써 팩토리얼을 계산하는 Idris 프로그램을 작성하면, 결과 정의는 특수화되어 인터프리터를 부분적으로 평가해버려요:
runFac : Int -> Int
runFac x = interp [] eFac x
interp에 대한 호출이 부분적으로 평가되어 제거되었음을 다음과 같이 볼 수 있어요:
*interp> :printdef runFac
runFac : Int -> Int
runFac x = PE_interp_ed1429e [] x
PE_interp_ed1429e를 보면 인터프리터가 평가되어 제거된 상태로 eFac의 구조를 정확히 따르는 것을 볼 수 있어요:
*interp> :printdef PE_interp_ed1429e
PE_interp_ed1429e : Env gamma -> Int -> Int
PE_interp_ed1429e (3arg) = \x =>
boolElim (x == 0)
(Delay 1)
(Delay (PE_interp_b5c2d0ff (x :: (3arg))
(PE_interp_ed1429e (x :: (3arg)) (x - 1)) x))
가독성을 위해 이것을 약간 단순화했어요: 실제로 보게 될 것에는 ==, -, fromInteger의 특수화된 버전도 포함돼요. eFac를 나타내는 PE_interp_ed1429e가 eFac의 구조를 따르는 재귀 함수가 되었음을 주목하세요. 또한 eMult에 대한 특수화된 인터프리터인 PE_interp_b5c2d0ff에 대한 호출도 있어요.
이 정의들은 부분 평가기가 특정 구체적인 인자에 의한 정의의 특수화를 한 번만 수행하고, 그 후에는 미래의 사용을 위해 캐시하기 때문에 생겨요. 따라서 interp의 eFac에 대한 미래의 어떤 적용도 PE_interp_ed1429e로 번역될 거예요.
가독성을 위한 단순화 없이 eMult의 특수화된 버전은 다음과 같아요:
PE_interp_b5c2d0ff : Env gamma -> Int -> Int -> Int
PE_interp_b5c2d0ff (3arg) = \x => \x1 => PE_*_954510b4 x x1