namespace

namespace は、定義に階層構造を与えて整理するためのコマンドです。名前空間 Foo の中で bar を定義すると、それは Foo.bar という名前になり、名前空間 Foo の中では短い名前 bar でアクセスできますが、名前空間を出るとアクセスにフルネームが必要になります。

なおここでは説明のために namespace の中をインデントしていますが、これは一般的なコード規約ではありません。

-- namespace の外で定義された関数
def greet (name : String) := "Hello, " ++ name

namespace Nat

  def isEven (n : Nat) : Bool := n % 2 == 0

  -- 同じ名前空間の中なら短い名前でアクセスできる
  #check isEven

  -- 名前空間の外にある名前にアクセスできる
  #check greet

end Nat

-- 名前空間の外に出ると、短い名前ではアクセスできない
#check_failure isEven

-- フルネームならアクセスできる
#check Nat.isEven

名前空間は入れ子にすることができます。

namespace Nat

  namespace Even

    def thirty := 30

  end Even

  #check Even.thirty

end Nat

#check Nat.Even.thirty

名前空間を一時的に抜ける

名前空間を一時的に抜けたいとき、_root_ が使用できます。名前空間 Hoge の中で foo を定義すると Hoge.foo という名前になりますが、_root_.foo と定義すればこの挙動を避けて foo という名前にすることができます。

たとえば以下のように名前空間の中で List 配下の関数を定義し、フィールド記法を使おうとしてもうまくいきません。こういう場合に _root_ を使用すると、名前空間を閉じることなくエラーを解消できます。

namespace Root -- 名前空間 `Root` の宣言

variable {α : Type}

def List.unpack (l : List (List α)) : List α :=
  match l with
  | [] => []
  | x :: xs => x ++ unpack xs

/--
error: invalid field 'unpack', the environment does not contain 'List.unpack'
  [[1, 2], [3]]
has type
  List (List Nat)
-/
#guard_msgs (whitespace := lax) in
#check ([[1, 2], [3]] : List (List Nat)).unpack

-- エラーになる原因は、名前空間 `Root` の中で宣言したので
-- 関数名が `Root.List.unpack` になってしまっているから
#check Root.List.unpack

-- `_root_` を頭につけて再度定義する
def _root_.List.unpack (l : List (List α)) : List α :=
  match l with
  | [] => []
  | x :: xs => x ++ unpack xs

-- 今度は成功する
#eval [[1, 2], [3]].unpack

end Root