유일성 타입
유일성 타입 (Uniqueness Types)
유일성 타입(Uniqueness Types)은 Idris 0.9.15부터 사용할 수 있는 실험적인 기능이에요. 유일한 타입(unique type)을 가진 값은 런타임에 그 값을 가리키는 참조가 기껏해야 하나라는 것이 보장돼요. 이는 메모리를 제자리에서 안전하게 갱신할 수 있다는 뜻이며, 메모리 할당과 가비지 컬렉션의 필요를 줄여줘요. 동기(motivation)는 제한된 메모리 환경에서 실행되는 프로그램, 반응형 시스템(reactive systems), 디바이스 드라이버, 그리고 하드 실시간 요구사항이 있는 다른 어떤 시스템을 — 되도록 높은 수준의 편의성을 거의 포기하지 않으면서 — 작성하고 싶기 때문이에요.
이것들은 선형 타입(linear types), Clean 프로그래밍 언어의 유일성 타입, 그리고 Rust 프로그래밍 언어의 소유권 타입(ownership types)과 빌린 포인터(borrowed pointers)에서 영감을 받았어요.
유일성 타입으로 언젠가 가능해지길 바라는 것들에는 다음이 포함돼요.
- 배열, 리스트 등의 안전하고 순수한 제자리 갱신
- 올바른 리소스 사용, 상태 전이(state transitions) 등을 보장
- 중요한 프로그램 조각이 절대 할당하지 않는다는 보장
출처: 문서
유일성 사용하기 (Using Uniqueness)
x : T이고 T : UniqueType이면, 런타임 실행 중 어떤 시점에도 x를 가리키는 참조가 기껏해야 하나예요. 예를 들어, 유일한 리스트의 타입은 다음과 같이 선언할 수 있어요.
data UList : Type -> UniqueType where
Nil : UList a
(::) : a -> UList a -> UList a
xs : UList a 값을 가진다면, 런타임에 xs를 가리키는 참조가 기껏해야 하나예요. 타입 검사기는 패턴 절(clause)에서 유일한 타입의 어떤 값에도 참조가 기껏해야 하나라는 것을 보장함으로써 이 보장을 지켜요. 예를 들어, 다음 함수 정의는 유효해요.
umap : (a -> b) -> UList a -> UList b
umap f [] = []
umap f (x :: xs) = f x :: umap f xs
두 번째 절에서 xs는 유일한 타입의 값이고, 오른쪽 편에 한 번만 나타나므로 이 절은 유효해요. 그뿐 아니라, UList a 인자에 대한 다른 참조가 있을 수 없다는 것을 알기 때문에, 그 공간을 결과를 만드는 데 재사용할 수 있어요! 컴파일러는 이것을 알고, 이 정의를 리스트의 제자리 갱신으로 컴파일해요.
반면 다음 함수 정의는 (++의 구현이 있다고 가정해도) xs가 두 번 나타나므로 유효하지 않아요.
dupList : UList a -> UList a
dupList xs = xs ++ xs
이것은 xs에 대한 공유 포인터를 만들게 되므로, 타입 검사기는 다음과 같이 보고해요.
unique.idr:12:5:Unique name xs is used more than once
그러나 명시적으로 복사한다면, 타입 검사기는 만족해요.
dup : UList a -> UList a
dup [] = []
dup (x :: xs) = x :: x :: dup xs
x를 두 번 사용해도 괜찮다는 점에 주의하세요. 그 이유는 a가 UniqueType이 아니라 Type이기 때문이에요.
유일성 속성을 보존하기 위해, UniqueType이 나타날 수 있는 곳에는 몇 가지 다른 제약도 있어요. 특히, 함수 타입 (x : a) -> b의 타입은 a 또는 b의 타입에 의존해요 — 둘 중 하나가 UniqueType이면 함수 타입도 UniqueType이 돼요. 그리고 데이터 선언에서, 타입 생성자가 Type을 만들면 어떤 생성자도 UniqueType을 가질 수 없어요. 예를 들어, 다음 정의는 유일한 값을 잠재적으로 유일하지 않은 값 안에 넣을 수 있으므로 유효하지 않아요.
data BadList : UniqueType -> Type where
Nil : {a : UniqueType} -> BadList a
(::) : {a : UniqueType} -> a -> BadList a -> BadList a
마지막으로, 타입들은 제한된 범위까지 유일성에 대해 다형일(polymorphic) 수 있어요. Type과 UniqueType은 서로 다른 타입이므로, 유일한 타입에 대해 다형 함수를 사용할 수 있는 범위는 제한적이에요. 예를 들어, 함수 합성이 다음과 같이 정의되어 있다면:
(.) : {a, b, c : Type} -> (b -> c) -> (a -> b) -> a -> c
(.) f g x = f (g x)
그리고 유일한 타입에 대한 함수가 있다면:
foo : UList a -> UList b
bar : UList b -> UList c
UList가 Type을 계산하지 않으므로, foo와 bar를 bar . foo로 합성할 수 없어요. 대신 합성을 다음과 같이 정의할 수 있어요.
(.) : {a, b, c : Type*} -> (b -> c) -> (a -> b) -> a -> c
(.) f g x = f (g x)
Type* 타입은 유일한 타입이거나 유일하지 않은 타입을 나타내요. 그런 함수는 UniqueType을 전달받을 수 있으므로, 타입 Type*의 어떤 값도 오른쪽 편에 기껏해야 한 번 나타나야 한다는 요구사항을 만족해야 해요.
빌린 타입 (Borrowed Types)
유일성 타입으로 작업하다 보면, 한 번에 하나의 참조만 갖는 것이 불편할 수 있다는 것이 곧 명확해져요. 예를 들어, 리스트를 갱신하기 전에 그 리스트를 표시하고 싶다면 어떨까요?
showU : Show a => UList a -> String
showU xs = "[" ++ showU' xs ++ "]" where
showU' : UList a -> String
showU' [] = ""
showU' [x] = show x
showU' (x :: xs) = show x ++ ", " ++ showU' xs
이것은 showU의 유효한 정의지만, 안타깝게도 리스트를 소비해버려요! 그래서 다음 함수는 유효하지 않아요.
printAndUpdate : UList Int -> IO ()
printAndUpdate xs = do putStrLn (showU xs)
let xs' = umap (*2) xs -- xs no longer available!
putStrLn (showU xs')
그래도 유일한 리스트는 단지 검사만 할 뿐 갱신은 없으므로, 문제없이 표시할 수 있길 바랄 수 있어요. 우리는 빌림(borrowing)이라는 개념으로 이것을 달성할 수 있어요. Borrowed 타입은 최상위에서 (패턴 매칭으로, 또는 다른 함수에 빌려줌으로써) 검사할 수 있지만 그 이상은 할 수 없는 유일한 타입이에요. 이는 내부(즉 최상위 패턴의 인자들)가 그것을 갱신할 어떤 함수에도 전달되지 않도록 보장해요.
Borrowed는 UniqueType을 BorrowedType으로 변환해요. 그것은 다음과 같이 정의돼요 (타입 검사기에 몇 가지 추가 규칙과 함께):
data Borrowed : UniqueType -> BorrowedType where
Read : {a : UniqueType} -> a -> Borrowed a
implicit
lend : {a : UniqueType} -> a -> Borrowed a
lend x = Read x
값은 lend를 사용해 다른 함수에 "빌려줄" 수 있어요. lend의 인자는 타입 검사기가 유일한 값에 대한 참조로 세지 않아요. 따라서 값을 원하는 만큼 여러 번 빌려줄 수 있어요. 이것으로 showU를 다음과 같이 쓸 수 있어요.
showU : Show a => Borrowed (UList a) -> String
showU xs = "[" ++ showU' xs ++ "]" where
showU' : Borrowed (UList a) -> String
showU' [] = ""
showU' [x] = show x
showU' (Read (x :: xs)) = show x ++ ", " ++ showU' (lend xs)
유일한 값과 달리, 빌린 값은 원하는 만큼 여러 번 참조될 수 있어요. 그러나 빌린 값을 어떻게 사용할 수 있는지에는 제한이 있어요. 어쨌든, 도서관의 책이나 이웃의 잔디 깎는 기계처럼, 함수가 값을 빌렸다면 그것을 받았을 때와 정확히 같은 상태로 반환할 것이 기대되니까요!
그 제한은, Borrowed 타입이 매칭될 때 Read 아래에 있는 유일한 타입의 패턴 변수들은 (그것들이 다른 함수에 빌려지지 않는 한) 오른쪽 편에서 전혀 참조될 수 없다는 것이에요.
유일성 정보는 타입에, 특히 함수 타입에 저장돼요. 유일한 컨텍스트 안에 들어서면, 새로 구성되는 어떤 함수도 유일한 타입을 가질 것이 요구되며, 이는 다음 종류의 나쁜 프로그램이 구현되는 것을 막아줘요.
foo : UList Int -> IO ()
foo xs = do let f = \x : Int => showU xs
putStrLn $ free xs
putStrLn $ f 42
pure ()
lend가 묵시적이므로, 실제로 함수가 값을 빌리고 빌려주기 위해서는 단지 인자가 Borrowed로 표시되기만 하면 돼요. 따라서 showU를 다음과 같이 쓸 수 있어요.
showU : Show a => Borrowed (UList a) -> String
showU xs = "[" ++ showU' xs ++ "]" where
showU' : Borrowed (UList a) -> String
showU' [] = ""
showU' [x] = show x
showU' (x :: xs) = show x ++ ", " ++ showU' xs
문제점/단점/앞으로 할 일 (Problems/Disadvantages/Still to do…)
이것은 진행 중인 작업이라 할 일이 많아요. 가장 분명한 문제는 추상화의 상실이에요. 한편으로 UniqueType과 BorrowedType으로 메모리 사용을 더 정밀하게 제어할 수 있지만, 그들은 일반적으로 Type에 대해 다형인 함수들과 호환되지 않아요. 단기적으로는 이것으로 반응형 및 저메모리 시스템을 쓰기 시작할 수 있지만, 장기적으로는 더 많은 추상화를 지원하는 것이 좋을 거예요.
또한 메타이론(metatheory)을 전혀 검사하지 않았으므로, 이 모든 것이 치명적으로 결함이 있을 수도 있어요! 구현은 대체로 de Vries 등의 Uniqueness Typing Simplified에 기반하므로, 괜찮을 것이라고 믿을 이유는 있지만, 여전히 그 작업을 해야 해요.
선형 타입에서와 마찬가지로, 유일한 타입을 가진 함수의 속성을 증명하려고 할 때 (예를 들어, 무엇이 값을 사용한 것으로 세는지) 약간 성가신 점들이 있어요. 우리는 값을 정확히 한 번이 아니라 기껏해야 한 번 사용해야 하므로, 실제로는 이것이 문제가 덜 되는 것 같지만, 여전히 생각이 필요해요.