모듈 시스템
모듈 시스템 (Module System)
기초 (Basics)
먼저 몇 가지 용어를 소개할게요. 정의(definition)는 함수나 데이터 타입 같은 개체를 정의하는 구문적 구성이에요. 이름(name)은 정의를 식별하는 데 사용되는 문자열이에요. 같은 정의가 많은 이름을 가질 수 있고 프로그램의 다른 지점에서 다른 이름을 가질 수 있어요. 두 정의가 같은 이름을 가질 수도 있는데, 이 경우 그 이름이 사용되면 오류가 발생해요.
모듈 시스템의 주요 목적은 프로그램에서 이름이 사용되는 방식을 구조화하는 것이에요. 이것은 프로그램을 각 모듈이 많은 정의와 하위 모듈을 포함하는 모듈의 계층 구조로 조직함으로써 이루어져요. 예를 들어:
module Main where
module B where
f : Nat → Nat
f n = suc n
g : Nat → Nat → Nat
g n m = m
들여쓰기를 사용해 어떤 정의가 모듈의 일부인지 나타낸다는 점에 유의하세요. 예제에서 f는 모듈 Main.B에 있고 g는 Main에 있어요. 특정 정의를 어떻게 참조하는지는 그것이 모듈 계층의 어디에 위치하는지에 따라 결정돼요. 둘러싸는 모듈의 정의는 위 f의 타입에서 보았듯이 주어진 이름으로 참조돼요. 정의하는 모듈 밖에서 정의에 접근하려면 한정된 이름(qualified name)을 사용해야 해요.
module Main₂ where
module B where
f : Nat → Nat
f n = suc n
ff : Nat → Nat
ff x = B.f (B.f x)
모듈의 정의에 짧은 이름을 사용하려면 그 모듈을 열어야(open) 해요.
module Main₃ where
module B where
f : Nat → Nat
f n = suc n
open B
ff : Nat → Nat
ff x = f (f x)
만약 A.qname이 정의 d를 가리키면, open A 후에는 qname도 d를 가리켜요. qname 자체가 한정된 이름일 수 있다는 점에 유의하세요. 모듈을 여는 것은 정의에 대해 새 이름만 도입할 뿐, 옛 이름을 제거하지는 않아요. 정책은 모호한 이름의 도입을 허용하지만, 모호한 이름이 사용되면 오류를 주는 것이에요.
모듈은 also open B를 where 절 안에 둠으로써 로컬 스코프 안에서 열릴 수 있어요:
ff₁ : Nat → Nat
ff₁ x = f (f x) where open B
Private 정의 (Private definitions)
정의를 정의하는 모듈 밖에서 접근할 수 없게 만들려면 private으로 선언할 수 있어요. private 정의는 그것을 정의하는 모듈 안에서는 일반 정의로 취급되지만, 모듈 밖에서는 그 정의에 이름이 없어요. 의존 타입 설정에서 private 정의에는 몇 가지 문제가 있어요 — 타입 체커가 계산을 수행하므로 private 이름이 목표와 오류 메시지에 나타날 수 있기 때문이에요. 다음 (인위적인) 예제를 생각해 봐요:
module Main₄ where
module A where
private
IsZero’ : Nat → Set
IsZero’ zero = ⊤
IsZero’ (suc n) = ⊥
IsZero : Nat → Set
IsZero n = IsZero’ n
open A
prf : (n : Nat) → IsZero n
prf n = ?
목표 ?0의 타입은 IsZero n으로, IsZero’ n으로 정규화돼요. 이 정규 형태를 사용자에게 어떻게 표시할지가 문제예요. ?0의 지점에서 IsZero’에 대한 이름이 없어요. 한 가지 옵션은 항을 접어서 IsZero n이라고 출력하려고 하는 것일 수 있어요. 이것은 일반적으로 매우 어려운 문제이므로, 이것을 하려고 하기보다는 IsZero’가 스코프에 없는 것임을 사용자에게 분명히 하고 목표를 ;Main₄.A.IsZero’ n으로 출력해요. 앞의 세미콜론은 그 개체가 스코프에 없음을 나타내요. 같은 기법이 모호한 이름만 있는 정의에도 사용돼요.
실제로 private 정의를 사용하는 것은 사용자 관점에서 주체 축약(subject reduction)이 없다는 것을 의미해요. 하지만 이것은 착각일 뿐이에요 — 타입 체커는 모든 정의에 완전히 접근할 수 있어요.
이름 수식어 (Name modifiers)
정의들을 private으로 만드는 대안은 모듈을 열 때 어떤 이름이 도입되는지에 대해 더 세밀한 제어를 가하는 것이에요. 이것은 open(또는 open import 또는 module X (args : Args) = ...) 문을 using, hiding, renaming 수식어 중 하나 이상으로 한정함으로써 이루어져요.
using뒤에는 세미콜론으로 구분된 식별자 목록이 오며, 그 식별자들과 renaming 절에 이름이 있는 것들만 도입하는 효과가 있어요.hiding도 마찬가지로 세미콜론으로 구분된 식별자 목록이 오며, hiding 절에 이름이 있는 것들만 제외한 모든 식별자를 도입하는 효과가 있어요.renaming뒤에는 세미콜론으로 구분된<식별자> to <식별자>목록이 오며, 언급된 식별자를 그것들의 새 이름으로 도입하는 효과가 있어요. 생략된 renaming 수식어는 빈 renaming과 동등해요.
예를 들어
open A using (xs) renaming (ys to zs)
의 효과는 xs와 zs 이름을 도입하는 것인데, xs는 A.xs와 같은 정의를 가리키고 zs는 A.ys를 가리켜요. xs, ys, zs가 겹치는 것은 허용하지 않아요.
hiding 절에서 x를 명시적으로 숨기면서 동시에 using 절에서 x를 사용하거나 renaming 절에서 x를 y로 바꾸는 것은 오류예요.
renaming 절은 using이나 hiding 절 중 하나와 결합될 수 있어요. using과 hiding 절은 결합될 수 있지만 using 절이 우선하여 언급되지 않은 모든 것을 숨기므로, 모듈과 관련된 특수한 상황을 제외하면 hiding 절이 추가로 숨길 수 있는 것은 없어요.
열어지는 모듈의 하위 모듈에 대해 세 가지 상황을 구분해야 해요:
M이 (객체가 아니라) 모듈일 뿐이면, 그것을 참조하려면module M을 사용하고, 이름을 바꾸려면module M to N을 사용해요. 단순히M을 언급하는 것은 경고와 함께 무시돼요. 예를 들어:open A using (module M)M이 (모듈이 아니라) 객체일 뿐이면, 그것을 참조하려면M을 사용하고 이름을 바꾸려면M to N을 사용해요.module M을 언급하는 것은 경고와 함께 무시돼요.M이 객체와 모듈 둘 다이면(M이 data 또는 record 정의로 도입된 경우 자동으로 그렇게 됨),module M이 별도로 언급되지 않는 한M은 객체와 모듈 둘 다에 영향을 미쳐요. 모듈만 도입하려면using (module B)을 쓸 수 있어요. 객체만 도입하려면using (B) hiding (module B)을 쓸 수 있어요. 모듈만 제외한 전부를 도입하려면hiding (module B)을 쓸 수 있어요. 객체만 제외한 전부를 도입하는 것은 가능해 보이지 않아요:hiding (B) using (module B)을 쓰면 using 절이 우선해서 모듈B만 도입돼요.
2.6.1부터: 연산자의 고정성(fixity)이 renaming 지시어에서 설정되거나 바뀔 수 있어요:
module ExampleRenamingFixity where
module ArithFoo where
postulate
A : Set
_&_ _^_ : A → A → A
infixr 10 _&_
open ArithFoo renaming (_&_ to infixl 8 _+_; _^_ to infixl 10 _^_)
여기서 _&_를 _+_로 이름을 바꾸면서 고정성을 바꾸고, ArithFoo 모듈에서 기본 고정성을 가진 _^_에 새 고정성을 할당해요.
이름 재-내보내기 (Re-exporting names)
유용한 기능은 다른 모듈의 이름을 재-내보낼(re-export) 수 있는 능력이에요. 예를 들어 몇몇 다른 모듈의 정의를 모으는 모듈을 만들고 싶을 수 있어요. 이것은 open 문을 public 키워드로 한정하면 이루어져요:
module Example where
module Nat₁ where
data Nat₁ : Set where
zero : Nat₁
suc : Nat₁ → Nat₁
module Bool₁ where
data Bool₁ : Set where
true false : Bool₁
module Prelude where
open Nat₁ public
open Bool₁ public
isZero : Nat₁ → Bool₁
isZero zero = true
isZero (suc _) = false
위 Prelude 모듈은 isZero에 더해 Nat, zero, Bool 등의 이름을 내보내요.
매개변수화된 모듈 (Parameterised modules)
지금까지 논의된 모듈 시스템 기능들은 전적으로 스코프 조작을 다뤄왔어요. 이제 우리의 관심을 더 고급 기능으로 돌려봐요.
모듈을 선언할 때 모듈의 모든 정의로부터 추상화되는 모듈 매개변수의 텔레스코프를 줄 수 있어요. 이것은 주어진 시그니처에서 일시적으로 작업할 수 있게 해줘요.
예를 들어 리스트 정렬 함수를 정의할 때 리스트 원소의 집합 A와 A 위의 순서 _≤_를 가정하는 것이 편리해요. 따라서 정렬 함수의 간단한 구현은 다음과 같아요:
module Sort (A : Set)(_≤_ : A → A → Bool) where
insert : A → List A → List A
insert x [] = x ∷ []
insert x (y ∷ ys) with x ≤ y
insert x (y ∷ ys) | true = x ∷ y ∷ ys
insert x (y ∷ ys) | false = y ∷ insert x ys
sort : List A → List A
sort [] = []
sort (x ∷ xs) = insert x (sort xs)
언급했듯이 모듈을 매개변수화하는 것은 모듈의 정의에 대해 매개변수를 추상화하는 효과가 있어서, Sort 모듈 밖에서 우리는 다음을 가져요:
Sort.insert : (A : Set)(_≤_ : A → A → Bool) →
A → List A → List A
Sort.sort : (A : Set)(_≤_ : A → A → Bool) →
List A → List A
함수 정의에 대해 명시적 모듈 매개변수는 추상화된 함수의 명시적 인자가 되고, 암시적 매개변수는 암시적 인자가 돼요. 하지만 생성자에 대해서는 매개변수가 항상 암시적 인자예요. 이것은 모듈 매개변수가 데이터 타입 매개변수로 바뀌고, 데이터 타입 매개변수는 생성자에 대한 암시적 인자라는 사실의 결과예요.
모듈 적용 (Module application)
매개변수화된 모듈은 모듈 적용 문으로 인스턴스화될 수 있어요. 우리의 예제를 계속하여,
module SortNat = Sort Nat leqNat
이것은 다음과 같이 새 모듈 SortNat를 정의해요:
module SortNat where
insert : Nat → List Nat → List Nat
insert = Sort.insert Nat leqNat
sort : List Nat → List Nat
sort = Sort.sort Nat leqNat
새 모듈은 매개변수화될 수도 있고, 이름 수식어를 사용해 원래 모듈의 어떤 정의가 적용되는지와 새 모듈에서 어떤 이름을 가지는지 제어할 수도 있어요.
모듈 적용의 일반적인 형태는:
module M1 Δ = M2 terms modifiers
일반적인 패턴은 모듈을 인자에 적용한 다음 결과 모듈을 여는 것이에요. 이것을 단순화하기 위해 축약형을 도입해요:
open module M1 Δ = M2 terms [public] modifiers
다음에 대한:
module M1 Δ = M2 terms modifiers
open M1 [public]
인픽스 모듈 적용은 없음 (No infix module application)
모듈 이름은 일반 이름과 같은 구문 규칙을 따르지만, 인픽스 형태(그리고 전치·후치·믹스픽스 형태에서도)로 사용될 수 없어요. 위 예제를 계속하여, 비록 다음을 정의했더라도:
module _Sort_ (A : Set)(_≤_ : A → A → Bool) where
인픽스 표기로 그것을 인스턴스화할 수 없어요:
module SortNat = Nat Sort leqNat
익명 모듈 (Anonymous modules)
익명 모듈은 이름이 _(밑줄)인 모듈이에요. 익명 모듈은 많은 정의가 같은 인자를 공유할 때 특히 유용해요. 예를 들어:
module _ (A : Set) where
f : A → A
-- ...
g : A → A → A
-- ...
익명 모듈은 정의 직후 자동으로 열리고, 적용될 수 없어요.
프로그램을 여러 파일로 나누기 (Splitting a program over multiple files)
큰 프로그램을 만들 때 프로그램을 여러 파일로 나누고 모든 변경에 대해 모든 파일을 타입 체크하고 컴파일하지 않아도 되는 것이 중요해요. 모듈 시스템은 이것을 할 수 있는 구조화된 방법을 제공해요. 우리는 프로그램을 모듈의 모임으로 정의하며, 각 모듈은 별도의 파일에 정의돼요. 다른 파일에 정의된 모듈에 접근하려면 모듈을 임포트할 수 있어요:
import M
이것을 구현하려면 모듈이 정의된 파일을 찾을 수 있어야 해요. 이를 위해 최상위 모듈 A.B.C가 디렉터리 A/B/의 파일 C.agda에 정의되어야 한다고 요구해요. 대신 import 문에 파일 이름을 주는 것을 상상할 수도 있지만, 그러면 프로그램에 파일 시스템에 대한 세부사항을 어지럽히게 되어 좋지 않아요.
모듈 M을 임포트할 때, 모듈과 그 내용은 현재 파일에 정의된 것처럼 스코프로 가져와져요. 모듈 내용의 한정되지 않은 이름에 접근하려면 열어야 해요. 모듈 적용과 유사하게 축약형을 도입해요:
open import M
다음에 대한:
import M
open M
때때로 임포트된 모듈의 이름이 로컬 모듈과 충돌할 수 있어요. 이 경우 모듈을 다른 이름으로 임포트하는 것이 가능해요.
import M as M’
import 문에 수식어를 붙여 모듈 안에서 어떤 이름이 보이는지 제한하거나 바꿀 수도 있어요. open import 문에 붙은 수식어는 import 문이 아니라 open 문에 적용된다는 점에 유의하세요.
데이터 타입 모듈과 레코드 모듈 (Datatype modules and record modules)
데이터 타입을 정의하면 모듈도 정의되어, 생성자가 이제 그 데이터 타입에 의해 한정되어 참조될 수 있어요. 예를 들어 주어졌을 때:
module DatatypeModules where
data Nat₂ : Set where
zero : Nat₂
suc : Nat₂ → Nat₂
data Fin : Nat₂ → Set where
zero : ∀ {n} → Fin (suc n)
suc : ∀ {n} → Fin n → Fin (suc n)
Nat₂.zero, Nat₂.suc, Fin.zero, Fin.suc로 생성자를 모호함 없이 참조할 수 있어요 (Nat₂와 Fin은 각각의 생성자를 포함하는 모듈이에요). 예제:
inj : (n m : Nat₂) → Nat₂.suc n ≡ suc m → n ≡ m
inj .m m refl = refl
이전에는 타입 체커가 이 경우 자연수 suc를 원한다는 것을 알아내도록 하려면 다음과 같이 써야 했어요:
inj₁ : (n m : Nat₂) → _≡_ {A = Nat₂} (suc n) (suc m) → n ≡ m
inj₁ .m m refl = refl
또한 레코드 선언도 대응하는 모듈을 정의하는데, 레코드 모듈(Record modules) 참고.
참고 문헌 (References)
Agda 2 모듈 시스템의 최초 설계는 Ulf Norell의 논문에 덮여 있어요. 모듈 시스템 구현과 그것의 현재 의미론 및 성능 문제에 대한 조사는 최근(2023) Ivar de Bruin에 의해 이루어졌어요.