모듈과 네임스페이스

모듈과 네임스페이스 (Modules and Namespaces)

Idris 프로그램은 모듈들의 모음으로 구성돼요. 각 모듈은 모듈의 이름을 주는 선택적 모듈 선언(module declaration), 가져올 다른 모듈들을 주는 import 문 목록, 그리고 타입·인터페이스·함수의 선언과 정의 모음으로 구성돼요. 예를 들어 아래 목록은 (파일 Btree.idr에서) 이진 트리 타입 BTree를 정의하는 모듈이에요:

module Btree

public export
data BTree a = Leaf
             | Node (BTree a) a (BTree a)

export
insert : Ord a => a -> BTree a -> BTree a
insert x Leaf = Node Leaf x Leaf
insert x (Node l v r) = if (x < v) then (Node (insert x l) v r)
                                   else (Node l v (insert x r))

export
toList : BTree a -> List a
toList Leaf = []
toList (Node l v r) = Btree.toList l ++ (v :: Btree.toList r)

export
toTree : Ord a => List a -> BTree a
toTree [] = Leaf
toTree (x :: xs) = insert x (toTree xs)

수정자 export와 public export는 어떤 이름이 다른 모듈에서 보이는지를 말해줘요. 이는 아래에서 더 설명할게요.

그리고 (파일 bmain.idr에서) Btree 모듈을 사용해 리스트를 정렬하는 메인 프로그램이 있어요:

module Main

import Btree

main : IO ()
main = do let t = toTree [1,8,2,7,9,3]
          print (Btree.toList t)

같은 이름이 여러 모듈에서 정의될 수 있어요: 이름은 모듈 이름으로 한정(qualified)돼요. Btree 모듈에서 정의된 이름은 정확히는 다음과 같아요:

  • Btree.BTree

  • Btree.Leaf

  • Btree.Node

  • Btree.insert

  • Btree.toList

  • Btree.toTree

이름이 다른 방식으로 모호하지 않다면, 완전히 한정된 이름을 줄 필요가 없어요. 이름은 명시적인 한정을 주거나 타입에 따라 모호성을 해소할 수 있어요.

모듈 이름과 파일 이름 사이의 공식적인 연결은 없지만, 각각에 같은 이름을 사용하는 것이 일반적으로 권장돼요. import 문은 디렉터리를 점으로 구분해 파일 이름을 가리켜요. 예를 들어 import foo.bar는 파일 foo/bar.idr를 가져오며, 관례적으로 module foo.bar 모듈 선언을 갖게 돼요. 모듈 이름에 대한 유일한 요구 사항은 main 함수를 가진 메인 모듈을 Main이라고 불러야 한다는 것이에요 — 파일 이름이 Main.idr일 필요는 없어요.

내보내기 수정자 (Export Modifiers)

Idris는 모듈 내용의 가시성에 대한 세밀한 제어를 허용해요. 기본적으로 모듈에 정의된 모든 이름은 private(비공개)로 유지돼요. 이것은 최소한의 인터페이스 명세와 내부 세부 사항을 숨기는 데 도움이 돼요. Idris는 함수, 타입, 인터페이스가 private, export, public export로 표시되는 것을 허용해요. 일반적인 의미는 다음과 같아요:

  • private — 전혀 내보내지 않음을 의미함. 기본값이에요.

  • export — 최상위 타입이 내보내짐을 의미함.

  • public export — 전체 정의가 내보내짐을 의미함.

가시성 수정의 추가 제한은, 정의가 더 낮은 가시성 수준의 어떤 것도 참조해서는 안 된다는 것이에요. 예를 들어 public export 정의는 private 이름을 사용할 수 없고, export 타입은 private 이름을 사용할 수 없어요. 이는 private 이름이 모듈 인터페이스로 새어 나가는 것을 막기 위한 것이에요.

함수에 대한 의미 (Meaning for Functions)

  • export — 타입이 내보내짐

  • public export — 타입과 정의가 내보내지고, 정의는 가져온 후 사용될 수 있음. 다시 말해, 정의 자체가 모듈 인터페이스의 일부로 간주됨. 긴 이름 public export는 이것을 두 번 생각하게 하려는 의도가 있음.

참고 (Note)

Idris에서 타입 동의어(synonym)는 함수를 작성해 만들어져요. 모듈의 가시성을 설정할 때, 타입 동의어가 모듈 밖에서 사용될 것이라면 모두 public export하는 것이 좋을 수 있어요. 그렇지 않으면 Idris가 동의어가 무엇의 동의어인지 알 수 없어요.

public export는 함수의 정의가 내보내짐을 의미하므로, 이는 효과적으로 함수 정의를 모듈 API의 일부로 만들어요. 따라서 일반적으로 완전한 정의를 내보내려는 것이 아니라면 함수에 public export를 사용하지 않는 것이 좋아요.

데이터 타입에 대한 의미 (Meaning for Data Types)

데이터 타입에 대해 의미는 다음과 같아요:

  • export — 타입 생성자가 내보내짐

  • public export — 타입 생성자와 데이터 생성자가 내보내짐

인터페이스에 대한 의미 (Meaning for Interfaces)

인터페이스에 대해 의미는 다음과 같아요:

  • export — 인터페이스 이름이 내보내짐

  • public export — 인터페이스 이름, 메서드 이름, 기본 정의가 내보내짐

%access 지시어 (%access Directive)

기본 export 모드는 %access 지시어로 바꿀 수 있어요. 예를 들어:

module Btree

%access export

public export
data BTree a = Leaf
             | Node (BTree a) a (BTree a)

insert : Ord a => a -> BTree a -> BTree a
insert x Leaf = Node Leaf x Leaf
insert x (Node l v r) = if (x < v) then (Node (insert x l) v r)
                                   else (Node l v (insert x r))

toList : BTree a -> List a
toList Leaf = []
toList (Node l v r) = Btree.toList l ++ (v :: Btree.toList r)

toTree : Ord a => List a -> BTree a
toTree [] = Leaf
toTree (x :: xs) = insert x (toTree xs)

이 경우 접근 수정자가 없는 어떤 함수든 private으로 남는 대신 export로 내보내져요.

내부 모듈 API 전파하기 (Propagating Inner Module API's)

추가로, 모듈은 import에 public 수정자를 사용해 자신이 가져온 모듈을 다시 내보낼 수 있어요. 예를 들어:

module A

import B
import public C

모듈 A는 이름 a와 모듈 C의 public 또는 abstract 이름을 내보낼 거지만, 모듈 B의 어떤 것도 다시 내보내지 않을 거예요.

명시적 네임스페이스 (Explicit Namespaces)

모듈을 정의하면 암시적으로 네임스페이스도 정의돼요. 하지만 네임스페이스는 명시적으로도 주어질 수 있어요. 이는 같은 모듈 안에서 이름을 오버로드하고 싶을 때 가장 유용해요:

module Foo

namespace x
  test : Int -> Int
  test x = x * 2

namespace y
  test : String -> String
  test x = x ++ x

이 (아마 인위적인) 모듈은 완전히 한정된 이름 Foo.x.test과 Foo.y.test를 가진 두 함수를 정의하며, 타입으로 구분할 수 있어요:

*Foo> test 3
6 : Int
*Foo> test "foo"
"foofoo" : String

매개변수화된 블록 (Parameterised blocks)

함수 그룹은 parameters 선언을 사용해 여러 인자에 대해 매개변수화할 수 있어요. 예를 들어:

parameters (x : Nat, y : Nat)
  addAll : Nat -> Nat
  addAll z = x + y + z

parameters 블록의 효과는 블록 안의 모든 함수, 타입, 데이터 생성자에 선언된 매개변수를 추가하는 것이에요. 구체적으로는 인자 목록의 앞에 매개변수를 추가하는 것이에요. 블록 밖에서는 매개변수를 명시적으로 주어야 해요. 따라서 REPL에서 호출할 때 addAll 함수는 다음 타입 시그니처를 가질 거예요.

*params> :t addAll
addAll : Nat -> Nat -> Nat -> Nat

그리고 다음 정의를 가져요.

addAll : (x : Nat) -> (y : Nat) -> (z : Nat) -> Nat
addAll x y z = x + y + z

parameters 블록은 중첩될 수 있고, 데이터 선언도 포함할 수 있어요. 이 경우 매개변수가 모든 타입·데이터 생성자에 명시적으로 추가돼요. 묵시적 인자를 가진 의존 타입일 수도 있어요:

parameters (y : Nat, xs : Vect x a)
  data Vects : Type -> Type where
    MkVects : Vect y a -> Vects a

  append : Vects a -> Vect (x + y) a
  append (MkVects ys) = xs ++ ys

블록 밖에서 Vects나 append를 사용하려면 xs와 y 인자도 주어야 해요. 여기서 타입 검사기가 추론할 수 있는 값에는 자리표시자(placeholder)를 사용할 수 있어요:

*params> show (append _ _ (MkVects _ [1,2,3] [4,5,6]))
"[1, 2, 3, 4, 5, 6]" : String

출처: 문서