アトリビュート#

Attributes are annotations placed before structures in source code. They take the form #attribute(...). An attribute occupies the entire line, and newlines are not allowed within it. Attributes do not normally affect the meaning of programs. Unused attributes will be reported as warnings.

アトリビュートの構文は次のとおりです:

attribute ::= '#' attribute-name
            | '#' attribute-name '(' attribute-arguments ')'

attribute-name ::= LIDENT | LIDENT '.' LIDENT

attribute-arguments ::= attribute-argument (',' attribute-argument )*

attribute-argument ::= expr | LIDENT '=' expr

expr ::= LIDENT | UIDENT | STRING | 'true' | 'false'
       | LIDENT '.' LIDENT
       | LIDENT '(' attribute-arguments ')'
       | LIDENT '.' LIDENT '(' attribute-arguments ')'

アトリビュートには 2 種類あります。組み込みアトリビュートとユーザー定義アトリビュートです。例えば:

#deprecated("message")
#custom.attribute(key="value", flag=true)

最初のアトリビュートは組み込みアトリビュートです。アトリビュート名に名前空間プレフィックスはありません。組み込みアトリビュートは MoonBit コンパイラに認識され、特定の意味を持ちます。

2 つ目のアトリビュートはユーザー定義アトリビュートです。アトリビュート名に custom. という名前空間プレフィックスがあります。ユーザー定義アトリビュートはコンパイラには無視されますが、外部ツールはソースコードを解析して利用できます。

注釈

MoonBit はランタイムリフレクションをサポートしない設計です。これは悪用されやすく、ツールチェーン(たとえばコンパイラ)がコンパイル時にエラーを検出できなくなり、コードの保守性が下がります。また、性能最適化にも悪影響があります。

私たちはコンパイル時コード生成を使うことを好みます。これにより静的型付けと性能の利点を保てます(ただし、不要な複雑さを避けるため慎重に使うべきです)。

非推奨アトリビュート#

The #deprecated attribute is used to mark an API as deprecated. MoonBit emits a warning when the deprecated API is used, and if the API is listed in completion, it will be shown with a strikethrough style. For example:

#deprecated
pub fn foo() -> Unit {
  ...
}

#deprecated("Use Bar2 instead")
pub(all) enum Bar {
  Ctor1
  Ctor2
}

#deprecated アトリビュートは次の文脈で使えます:

  • トップレベルの値宣言(fnletconst を含む)

  • トップレベルの型宣言(typestructenum を含む)

  • trait メソッド宣言

  • trait のデフォルト実装

  • extend 宣言

一般的な形式は次のとおりです:

  • #deprecated

    項目を非推奨にし、デフォルトの警告メッセージを使います。

  • #deprecated("Use new_function instead")

    項目を非推奨にし、カスタム警告メッセージを使います。非推奨 API が使われるたびに、指定したメッセージが警告として表示されます。

  • #deprecated("Use new_function instead", skip_current_package=true)

    項目を非推奨にし、カスタム警告メッセージを使いますが、同じパッケージ内で非推奨 API が使われた場合は警告を出しません。

  • #deprecated(skip_current_package=true)

    Marks the item as deprecated with a default warning message, but skips emitting warnings within the same package. When both a message and skip_current_package are present, either argument order is accepted.

Alert Attribute#

#alert アトリビュートは API にカテゴリとメッセージを付与します。その API が使われると、MoonBit は alert 警告を出します。

#alert(unsafe, "This function is unsafe.")
fn[A] alert_unsafe_get(arr : Array[A], index : Int) -> A {
  arr[index]
}

第 1 引数は alert のカテゴリで、第 2 引数はユーザーに表示されるメッセージです。この警告は alertalert_unsafe などの警告名で設定できます。

For more detail, see alert warning.

エイリアスアトリビュート#

alias アトリビュートは、添字に関係する演算子をオーバーロードしたり、トップレベル関数や変数に別名を付けたりするために使います。形式は 2 種類あります:

  • #alias("op")。ここで op は次の添字演算子を表す文字列のいずれかです:

    • _[_]: 添字演算子

    • _[_]=_: 添字代入演算子

    • _[_:_]: as view 演算子

  • #alias(id)。ここで id は別名を表す識別子です。

どちらの形式でも追加引数を指定できます:

  • visibility="modifier"

    ラベル付き引数で、別名の可視性を変更します。modifierpub または priv です。指定しない場合、別名の可視性は元の関数または変数と同じになります。

  • deprecated または deprecated="message"

    別名を非推奨としてマークします。メッセージを指定した場合、別名が使われると警告として表示されます。

To graceful migration from old API to new API, you can rename the old API directly, and create an alias with the old name, mark it as deprecated. For example:

#alias(old_name, deprecated)
fn new_name() -> Unit {
  ()
}

label_migration アトリビュート#

The #label_migration attribute is used to help you safely evolve your API by warning users during the transition period.

形式は次の 3 種類です:

  • #label_migration(id, fill=true, msg="message")

    The fill argument is used when you want to refactor an optional parameter. You can use fill=true when you want to eventually make an optional parameter required. You can use fill=false when you want to eventually remove an optional parameter.

    msg 引数は、移行に関する追加情報を提供する文字列です。

    #label_migration(x, fill=true)
    #label_migration(y, fill=false)
    fn label_migration_fill(x? : Int = 0, y? : Int = 1) -> Int {
      x + y
    }
    
  • #label_migration(id, allow_positional=true, msg="message")

    The allow_positional argument is used when you want a labelled parameter to be used without its label being provided. When the parameter is used positionally (without a label), the compiler reports a warning. This is useful when you want to change a positional parameter to a labelled parameter without breaking the downstream code.

    msg 引数は、移行に関する追加情報を提供する文字列です。

    #label_migration(x, allow_positional=true)
    fn label_migration_allow_positional(x~ : Int) -> Int {
      x
    }
    
  • #label_migration(id, alias=new_id, msg="message")

    The alias argument allows you to provide an alternative name to a labelled parameter. This is useful when renaming a parameter to maintain backward compatibility. If a warning message is provided, the compiler warns when using the alias; otherwise, the alias can be used without warnings.

    msg 引数は、移行に関する追加情報を提供する文字列です。

    #label_migration(x, alias=xx)
    #label_migration(x, alias=y, msg="warning")
    fn label_migration_alias(x~ : Int) -> Int {
      x
    }
    

可視性アトリビュート#

注釈

このトピックではアクセス制御は扱いません。pubpub(all)priv について詳しくは Access Control を参照してください。

The #visibility attribute is similar to the #deprecated attribute, but it is used to hint that a type will change its visibility in the future. For outside usages, if the usage will be invalidated by the visibility change in future, a warning will be emitted.

// in @util package
#visibility(change_to="readonly", "Point will be readonly in the future.")
pub(all) struct Point {
  x : Int
  y : Int
}

#visibility(change_to="abstract", "Use new_text and new_binary instead.")
pub(all) enum Resource {
  Text(String)
  Binary(Bytes)
}

pub fn new_text(str : String) -> Resource {
  ...
}

pub fn new_binary(bytes : Bytes) -> Resource {
  ...
}

// in another package
fn main {
  let p = Point::{ x: 1, y: 2 } // warning
  let { x, y } = p // ok
  println(p.x) // ok
  match Resource::Text("") { // warning
    Text(s) => ... // waning
    Binary(b) => ... // warning
  }
}

The #visibility attribute takes a required change_to argument and an optional message argument.

  • change_to 引数は、型の新しい可視性を表す文字列です。値は "abstract" または "readonly" のどちらかです。

    change_to

    無効になる使い方

    "readonly"

    型のインスタンスを生成すること、またはそのフィールドを変更すること。

    "abstract"

    型のインスタンスを生成すること、インスタンスのフィールドを変更すること、パターンマッチ、またはラベルによるフィールドアクセス。

  • The optional message argument is a string that provides additional information about the visibility change.

内部アトリビュート#

The #internal attribute is used to mark a function, type, or trait as internal. Any usage of the internal function or type in other modules will emit an alert warning.

#internal(unsafe, "This is an unsafe function")
fn[A] internal_unsafe_get(arr : Array[A], index : Int) -> A {
  arr[index]
}

The internal attribute takes a required category argument and an optional message argument. category is a identifier that indicates the category of the alert, and message is a string that provides additional message for the alert.

alert 警告は moon.pkgwarnings フィールドを設定することで無効化できます。詳しくは alert warning を参照してください。

Doc Hidden Attribute#

#doc(hidden) アトリビュートは生成されるドキュメントから API を隠します。

#doc(hidden)
pub fn hidden_helper() -> Unit {
  ()
}

コードからは利用可能なままにする必要がある一方で、ドキュメント化された API としては表示したくない公開宣言に使います。

警告アトリビュート#

The #warnings attribute is used to configure warning settings for a specific top-level declaration. It can enable, disable or treat an enabled warning as error for specific warnings in that declaration.

The argument is a string that specifies the warning list. It can contain multiple warning names, each prefixed with a sign:

#warnings("-unused_value")
fn warnings_example() -> Unit {
  let x = 42
}

プレフィックスの意味は次のとおりです:

  • +warning_name: 警告を有効化

  • -warning_name: 警告を無効化

  • @warning_name: 有効な警告をエラーとして扱う(非推奨)

@ スイッチは v0.10.4 で非推奨になりました。個別の警告は + または - で設定し、警告によって CI ビルドを失敗させる場合は moon check --deny-warn または各コマンドの同等オプションを使用してください。

現在、このアトリビュートは一部の特定の警告にのみ対応しています。

To learn more about warning names, see warning list.

Must Implement One アトリビュート#

#must_implement_one アトリビュートは trait に付けて、各実装がデフォルトメソッド実装だけに依存せず、少なくとも 1 つのメソッドを明示的に定義することを要求します。

引数を指定しない場合、その trait の少なくとも 1 つのメソッドを明示的に実装する必要があります:

#must_implement_one
pub(open) trait RequireAnyMethod {
  f(Self) -> Unit = _
  g(Self) -> Unit = _
}

impl RequireAnyMethod with f(_) { () }

impl RequireAnyMethod with g(_) { () }

type AnyImpl

impl RequireAnyMethod for AnyImpl with f(_) { () }

メソッド名を指定した場合、列挙されたメソッドのうち少なくとも 1 つを明示的に実装する必要があります:

#must_implement_one(f, g)
pub(open) trait RequireSelectedMethod {
  f(Self) -> Unit = _
  g(Self) -> Unit = _
  h(Self) -> Unit = _
}

impl RequireSelectedMethod with f(_) { () }

impl RequireSelectedMethod with g(_) { () }

impl RequireSelectedMethod with h(_) { () }

type SelectedImpl

impl RequireSelectedMethod for SelectedImpl with g(_) { () }

同じ trait に複数の #must_implement_one アトリビュートを付けることで、複数のメソッドグループから明示的な実装を要求できます。

Inline Attribute#

#inline アトリビュートは関数に対する最適化ヒントです。可能であればその関数をインライン化するようコンパイラに依頼します:

#inline
fn add_one(x : Int) -> Int {
  x + 1
}

#inline(never) を使うと、関数をインライン化しないようコンパイラに依頼できます:

#inline(never)
fn keep_stack_frame(x : Int) -> Int {
  x + 1
}

これらのアトリビュートはヒントです。関数のソースレベルの振る舞いは変わりません。

外部アトリビュート#

#external アトリビュートは、抽象型を外部型としてマークするために使います。

  • Wasm および Wasm GC バックエンドでは、これは externref と解釈されます。

  • JavaScript バックエンドでは、これは any と解釈されます。

  • ネイティブバックエンドでは、これは void* と解釈されます。

#external
type AttrPtr

Borrow/Owned アトリビュート#

#borrow#owned アトリビュートは FFI 宣言で使い、参照カウントされる MoonBit 引数を外部コードへどのように渡すかを記述します。これは BytesStringFixedArray[T]、抽象型などのボックス化された MoonBit 値で重要です。これらの値のライフタイムは C および Wasm バックエンドで参照カウントにより管理されます。

外部関数が呼び出し中に param を読むだけで、それを保存したり返したりしない場合は #borrow(param) を使います。borrow された引数の所有権は MoonBit に残るため、外部関数はその引数に対して moonbit_decref$moonbit.decref を呼ぶ必要がありません。

外部関数が param の所有権を受け取る場合、たとえば保存して後で解放する場合は #owned(param) を使います。owned 引数は不要になった時点で、最終的に外部側が解放する必要があります。

#borrow(filename)
extern "C" fn open(filename : Bytes, flags : Int) -> Int = "open"

完全な呼び出し規約のルールについては FFI ライフタイム管理 を参照してください。

Unsafe Cycle-Free アトリビュート#

#unsafe_cycle_free アトリビュートは、struct、enum、newtype の宣言に対する高度な最適化アサーションです。注釈を付けた型の値が参照サイクルに決して加わらないことをコンパイラに伝えます。コンパイラはサイクル可能性の解析でこのアサーションを信頼し、検証しません。

#unsafe_cycle_free
pub(all) struct CycleFreeNode {
  mut next : CycleFreeNode?
}

危険

プログラムがサイクルフリー不変条件を保証できる場合にのみ、このアトリビュートを使ってください。誤ったアサーションにより、この型を含む参照サイクルが存在しないものとして扱われ、回収されなくなる可能性があります。

as_free_fn アトリビュート#

#as_free_fn アトリビュートは、メソッドを free 関数としても宣言することを示すために使います。free 関数の可視性や名前を変更したり、別個の非推奨警告を与えたりすることもできます。

#as_free_fn(dec, visibility="pub", deprecated="use `Int::decrement` instead")
#as_free_fn(visibility="pub")
fn Int::decrement(i : Self) -> Self {
  i - 1
}

test {
  let _ = decrement(10)
  let _ = (10).decrement()
}

Callsite アトリビュート#

#callsite アトリビュートは、呼び出し元で起こる属性を示すために使います。

autofill を指定でき、呼び出し元で引数 SourceLoc と ArgLoc を自動補完します。

Skip アトリビュート#

The #skip attribute is used to skip a single test block. It can be written as #skip or with a reason, such as #skip("blocked by external service"). The type checking will still be performed.

Coverage Skip Attribute#

#coverage.skip アトリビュートは関数内のカバレッジ操作をスキップします。

#coverage.skip
fn platform_specific_helper() -> Unit {
  ()
}

プラットフォーム固有のフォールバックコードや、意図的にカバレッジ測定から除外するコードパスなど、カバレッジレポートに影響させたくない関数に使います。詳しくは Skipping coverage を参照してください。

設定アトリビュート#

#cfg アトリビュートは条件付きコンパイルを行うために使います。例は次のとおりです:

#cfg(true)
fn cfg_true() -> Unit {
  ()
}

#cfg(false)
fn cfg_false() -> Unit {
  ()
}

#cfg(target="wasm")
fn cfg_wasm() -> Unit {
  ()
}

#cfg(not(target="wasm"))
fn cfg_not_wasm() -> Unit {
  ()
}

#cfg(all(target="wasm", true))
fn cfg_all() -> Unit {
  ()
}

#cfg(any(target="wasm", target="native"))
fn cfg_any() -> Unit {
  ()
}

モジュールアトリビュート#

module アトリビュートは、JavaScript バックエンド向けのモジュール依存を宣言するために使います。

cjs 形式では require として解釈され、esm 形式では import として解釈されます。

#module("math-utils")
pub extern "js" fn add_from_module(x : Int, y : Int) -> Int = "add"

Export Name Attribute#

The #export_name attribute assigns a stable exported symbol name to a public function in a package declared with pkgtype(kind: "foreign_library"). The name is used in generated Wasm, JavaScript, or C output:

#export_name("add")
pub fn add_one(value : Int) -> Int {
  value + 1
}

MoonBit currently requires the exported name to be unique within the package and to be a valid C symbol identifier, regardless of the selected backend.

警告

Known compiler issue: #export_name currently applies its C-symbol-identifier restriction to every backend. WebAssembly export names are UTF-8 strings and are not limited to C identifiers.

The attribute cannot be used on generic functions, functions with optional arguments, methods, or declarations without a body.

Prefer #export_name over backend-specific exports link configuration for new exports. It keeps the exported name next to the function and applies to every backend that supports foreign-library output. Use exports when the export set or names must differ by backend, or when the source cannot be annotated.

Export declarations are scoped to the package that produces the artifact. An attribute in a dependency applies when that dependency is built as its own artifact, but it does not add a symbol to a downstream package's artifact. To expose dependency functionality, define and export a wrapper in the exporting package.

注釈

native バックエンドは現在、foreign_library パッケージをリンク可能なライブラリアーティファクトとしてエクスポートできません。これには .dll.so などの共有ライブラリも含まれます。エクスポート可能なライブラリが必要な場合は、Wasm または JavaScript を使用してください。

See Export Functions for backend-specific alternatives.

Proof Pure アトリビュート#

#proof_pure アトリビュートは、副作用のない関数を実行可能コードと証明向けロジックの両方で利用できるようにします。

#proof_pure
fn height(t : Tree) -> Int {
  match t {
    Empty => 0
    Node(_, _, _, h) => h
  }
}

現在、通常のトップレベル関数と通常のメソッドをサポートしています。#proof_pure 定義では、検証契約、直接再帰、相互再帰はまだサポートされていません。

仕様における役割と完全な例については、形式検証を参照してください。

Proof External アトリビュート#

#proof_external(module, symbol) アトリビュートは、検証時の変換で抽象 MoonBit 型を Why3 モジュール内の型として表現するよう指定します。

///|
#proof_external("set.Fset", "fset")
pub type ProofSet[T]

この例では、証明向けロジック内の ProofSet[T] は Why3 型 set.Fset.fset T に変換されます。このアトリビュートは MoonBit 型を実装せず、実行時の値も提供せず、その型を FFI ABI に接続することもありません。

モジュールとシンボルの対応付けは、信頼される検証境界の一部です。対応する演算のインポートと証明例については、形式検証を参照してください。

Proof Import アトリビュート#

#proof_import(module) アトリビュートは、.mbtp ファイル内の証明専用ロジック宣言を Why3 モジュールのシンボルに対応付けます。宣言の文字列本体は Why3 シンボルを指定するもので、実行可能な MoonBit 式ではありません。

#proof_import("set.Fset")
fn proof_set_mem(x : Int, set : ProofSet[Int]) -> Bool = "mem"

#proof_import("set.Fset")
fn proof_set_empty() -> ProofSet[Int] = "empty"

#proof_import("set.Fset")
fn proof_set_add(x : Int, set : ProofSet[Int]) -> ProofSet[Int] = "add"

lemma proof_set_add_contains(x : Int) where {
  proof_ensure: proof_set_mem(
    x,
    proof_set_add(x, proof_set_empty()),
  ),
} {}

ここで、set.Fset は Why3 のモジュールパスであり、"mem""empty""add" はそのモジュール内のシンボルを指定します。これらの宣言は検証時の変換だけに影響し、実行時の実装や FFI バインディングは提供しません。最後の補題は証明義務を生成しますが、インポート宣言自体は生成しません。

宣言したシグネチャとシンボルの対応付けは、信頼される検証境界の一部です。完全な例と利用方法については、形式検証を参照してください。