Algebraic Effects に触れてみたくて Koka に入門した

## はじめに

最近話題の Algebraic Effects に触れてみたくて、Koka に入門した。
記憶があるうちに、Algebraic Effects について学べるだけの Koka の最低限の文法や所感を記事にしておく。

ちゃんと探していないけれど、たぶん Koka の日本語の資料はない。よって何から何まで、公式の入門記事に頼ることになる。
そしてこの記事が、これから Koka に入門する人の助けになれば幸いだ。

https://koka-lang.github.io/koka/doc/book.html

私は以下のバックグラウンドを持ち、この記事にはそのバイアスがかかっている。予めご了承いただきたい。

* Koka歴は 2日
* Haskell はある程度使った。Extensible Effects にも触れている
* OCaml, Eff は未経験

タグに Haskell を入れたのは Koka のタグをフォローしている人は皆無だと思ったからだ。
ほんの少しだけ Haskell 成分があるので、許してほしい。

## Koka の紹介

簡単に Koka について紹介する。

Koka は「作用型 (Effect types)」と「作用ハンドラ (Effect handlers)」を特徴とする、研究用の関数型プログラミング言語だ。

名前の Koka は 'effect'の日本語訳「効果」に由来している[^1]が、一般的に effect は効果ではなく作用と訳されるので、この記事ではあくまで「作用」を訳語として充てさせてもらう。

コンパイラのインストール手順は下記参照だ。

https://koka-lang.github.io/koka/doc/book.html#install

## 基本文法

Koka は 'Minimal but General' という信念に基づいて設計されており[^2]、コア機能が非常に小さい。その代わりにしばしば糖衣構文が使われるので、最終的にどのような形のプログラムになるのか常に意識しながらプログラムを書く必要がある。

前置きが長くなったが、Koka での Hello World は次の通りだ。

プログラミング言語 Koka と Algebraic effects の世界へようこそ。

```koka
fun main()
  println("Hello World")
```

シンタクスハイライトはない。
ぜひ、プラグインを入れた VSCode にコピペして、そして実行してみてほしい。

https://marketplace.visualstudio.com/items?itemName=koka.language-koka

### 定数と変数

Koka では次のように定数と変数を定義する。


```koka
val a = "Hello"
var b := "World"
b := "Monde"
```

一般的な習慣に倣い、基本的には不変な定数を使うのが良いだろう。

### 関数定義

Koka では次のように関数定義を行う。

```koka
fun greeting(name)
  "Hello, " ++ name
```

上のコードは、次のコードと等価だ。

```koka
fun greeting(name : string) : <total> string {
  return "Hello, " ++ name;
}
```

重要な点は概ね次の2点である:

1. 引数と、作用(後述)を含めた戻り値の型が補われる
2. 字下げされたブロックには波括弧(curly braces)が補完される

### 関数呼び出し

Koka では次のように関数を呼び出す。

```koka
println(greeting("John"))
```

引数の一つ目を前置することもできる。これを [Dot selection](https://koka-lang.github.io/koka/doc/book.html#sec-dot) と呼ぶ。

```koka
greeting("John").println()
```

### 高階関数

Koka では次のように高階関数を定義する。`e` は任意の作用、`a` は任意の型だ。

なお、公式ドキュメントを見た感じ、Koka では命名に kebab-case を使うのが一般的なようである。

```koka
fun do-action(action : () -> e a) : e a
  action()
```

受け取る関数の引数が1つのときは、丸括弧を省略することが可能だ。

```Koka
fun single-arg(value : a, mapper : a -> e b) : e b
  mapper(value)
```

受け取る関数が2つ引数を取る場合には、引数の型を囲む括弧が必要だ。

```koka
fun double-args(a : a, b : b, mapper : (a, b) -> e c) : e c
  mapper(a, b)
```

### 匿名関数と Trailing Lambdas

匿名関数の定義には、`fn`キーワードを使う。

```koka
do-action(fn() {
  println("Hello, anonymous functions")
})
```

ここでは、様々な糖衣構文が利用できる。

```koka
// 引数末尾の匿名関数は、関数呼び出しの丸括弧の外に置くことができる。
// またその結果、丸括弧の中が空になった場合には、丸括弧を省略することができる。
do-action fn() {
  println("Hello, trailing lambdas")
}

// 特別に、引数なしの匿名関数は `fn ()` を省略することができる。
do-action {
  println("Hello, anonymous functions with no parameters")
}

// 字下げをすれば、波括弧を省略することができる。
do-action
  println("Hello again, omitted curly braces")
```

だいぶ見た目の印象が変わることが分かる。DSL を作る道具は一通り揃っていそうだ。

なお、引数を持つ関数は、`fn()`を省略することができない。

```koka
"Lambda with a parameter".single-arg fn(a)
  println("Hello, " ++ a)
double-args("Hello", "World") fn(a, b)
  println(a ++ ", " ++ b)
```

### with 文

With 文 (With statements) は、Koka にとって非常に重要な構文だ。

With 文は高階関数を受け取り、以降の文を Trailing Lambda としてその高階関数に渡す。

次のような高階関数を用意した。この高階関数は `action` を受け取り実行するが、その前後でログメッセージを出力する。

```koka
fun with-greeting(action : () -> <console | e> a) : <console | e> a
  println("Hello, with-greeting")
  val ret = action()
  println("Bye, with-greeting")
  ret
```

これは [匿名関数と Trailing Lambdas](#匿名関数と-Trailing-Lambdas) で学んだ知識を用いて、次のように呼び出せる。

```koka
fun use-with-greeting() : console ()
  with-greeting
    println("A brown fox jumps over the lazy dog")
```

これを、with 文を使って、次のように書き直すことができる。

```koka
fun use-with-greeting-sugared() : console ()
  with with-greeting
  println("A brown fox jumps over the lazy dog")
```

インデントがなくなったことが分かるだろう。
すなわち、これは Koka におけるコールバック地獄の回避策だ。

引数が1つある高階関数では、次のように引数を束縛して利用することができる。

```koka
fun with-single-arg() : console list<()>
  with s <- single-arg("Lambda with a parameter")
  println("Hello " ++ s)
```

なお、引数が2つ以上ある高階関数では、with 文を使う例を見つけることができなかった。

## 作用 (Effects)

ここからが本題だ。

私は、Koka での作用とは Haskell でしばしば文脈と呼ばれるもの、あるいはその文脈で利用できる演算のことだと理解している。
そのため、文脈や環境という単語を使うかもしれないが、ご了承いただきたい。

早速 Koka で作用を利用する方法を確認していこう。
Koka の作用 (Effect) で定義できる演算 (Operation) は3種類存在する。といっても、例によって2つは糖衣構文で、本質的には1つしかない。

### 値演算 (Value Operations)

作用に定義できる演算のうち、最も簡単なものがこの値演算だ。

次のコードでは `is-verbose` という値を利用できる作用 `is-verbose` を定義している。

```koka
effect is-verbose
  val is-verbose : bool
```

ある作用が提供する演算が1つで、その演算が作用と同名である場合には、糖衣構文を利用できる。
すなわち、上のコードは、次のコードと等価である。

```koka
effect val is-verbose : bool
```

作った作用を使ってみよう。
これは、詳細モードが有効化されているかどうかによってログを出力するかどうかが変わる関数だ。

```koka
fun log-verbose(msg : string) : <is-verbose, console> ()
  if is-verbose
    println("DEBUG - " ++ msg)
```

この関数は、引数で `is-verbose` 変数を受け取っていないし、グローバル変数なども利用していない。
その代わり、この関数を実行するには `is-verbose` という文脈を持つ必要がある。

#### 作用ハンドラ (Effect handlers)

次の`run-server` 関数は、サーバー起動中であることをデバッグログに残している。

```koka
fun run-server(port : int) : <is-verbose, console> ()
  log-verbose("Server is preparing for running...")
  // ...
```

`log-verbose` 関数を利用するには、`is-verbose` 作用と `console` 作用が必要だから、`log-verbose` 関数を利用する `run-server` 関数にも同様の文脈が必要だ。

このように、例えば Java でいう検査例外 (Checked exceptions) のように、あるいはソフトウェアの GPL ライセンスのように、作用は利用者に「感染」していく。

しかし、作用は最終的には必ずハンドルされなければならない。

`is-verbose` 作用でいえば、最終的には文脈が持つ `is-verbose` という値に 必ず `True` か `False` が設定されなければならないのだ。
さもなくば、最終的には `main` 関数で作用の不一致によるコンパイルエラーが起こる。

文脈を作り出すには、作用ハンドラ (Effect handlers) を使う。

```koka
val h = handler
  val is-verbose = True
h {
  log-verbose("Hello, effect handlers")
}
```

`handler` キーワードに続けて、ハンドルしたい演算に具体的な値を与える。
作用ハンドラは、ハンドルした作用を文脈に持つコールバックを受け取るような高階関数を返すので、コールバック関数内では作用を持つ関数を呼び出しができる、という寸法だ。

これは、あたかもモナドスタックを積み上げているかのようだ。

例によって、糖衣構文が利用できる。

```koka
// ハンドル作用の演算が1つの場合には、インデントを用いずともよい。
val h' = handler val is-verbose = True
h' {
  log-verbose("Hello, effect handlers without indentations")
}

// そして、作用ハンドラは高階関数を返すため、with文 を利用することができる。
with handler val is-verbose = True
log-verbose("Hello, effect handlers with 'with statement'")

// `with handler` は頻出であるため、with 文と一緒に使う場合に限り、`handler` キーワードを省略することができる。
with val is-verbose = True
log-verbose("Hello, effect handlers without the handler keyword")
```

### 関数演算 (Tail-Resumptive Operations)

値演算に続いて、関数演算だ。
これは DI コンテナのような使い心地のものを提供する。

ためしに複数の演算を持つ作用を定義してみよう。

ログ出力を抽象化する作用だ。

```koka
effect log
  fun log-debug(msg : string) : ()
  fun log-info(msg : string) : ()
```

`run-server` を書き直してみよう。
`console` 作用はもはや書く必要はない。なぜなら、コンソールに出力するもファイルに出力するも `log` 作用が決めることだからだ。

```koka
fun run-server() : log ()
  log-debug("Server is preparing for running...")
  // ...
  log-info("Server is running")
```

作用ハンドラ側には、特別新しいことはない。

```koka
with handler
  fun log-debug(msg) log-verbose(msg)
  fun log-info(msg)  println("INFO - " ++ msg)
run-server()
```

### 制御演算 (General Control Operations)

作用を Koka の目玉機能たらしめるのは、この制御演算 (General Control Operations) だ。

値演算や関数演算は、実際のところ、制限をかけた制御演算である。
それはあたかも goto文 に制限をかけて if文 や for文 を作るかのようだ。

例外を投げる作用を定義する。

```koka
effect ctl throw-string(msg : string) : a
```

早速使ってみよう。

見ての通り、ゼロ除算で例外を投げる関数だ。

```koka
fun safe-div(m : int, n : int) : throw-string int
  if n == 0
    then throw-string("ZeroDivision")
    else m / n
```

当然 `safe-div` を呼び出すには `throw-string` の文脈が必要だ。
作用ハンドラを書こう。

次のように、例外が起こったらエラーメッセージを標準出力に書くようにする。

```koka
with ctl throw-string(msg) println("Fatal: " ++ msg)
val result = safe-div(1, 0) + 10
println("1 / 0 + 10 = " ++ show(result))
```

すると、`safe-div(1, 0)` が呼び出された時点で制御が作用ハンドラに移り、以後の文は無視される。

ここでの作用ハンドラは、まさに例外ハンドラだ。ただし、ハンドラの位置はちょっぴり上に上がってしまっているが。

```java:見慣れた疑似コード
try {
  int result = safeDiv(1, 0) + 10;
  println("1 / 0 + 10 = " + result);
} catch (msg) {
  println("Fatal: " + msg);
}
```

#### 制御演算の振る舞いは、型によって制限される

`throw-string` 演算は、戻り値の型が「任意の型」である。
しかし Koka には「任意の型に代入可能な値」は存在しない。つまり、`throw-string` 演算内で `resume` を実行することは決してないのだ。

#### 制御演算の resume 関数

制御演算は、必ずしも例外機構というわけではない。

制御演算のハンドラに暗黙に渡される `resume` 関数を呼び出せば、制御ハンドラによって区切られた限定継続を再開することができる。

言い換えれば、 `resume` 関数を使えば、制御演算の呼び出し元に値を返すことができる。
呼び出し元に値を返すといえば関数であるからして、制御演算は関数演算と同じこともできるというわけだ。

例えば、任意の値を取り出せる制御演算を持つ作用を定義しよう。

```koka
effect<a> ctl get() : a
```

この `get` 作用は、(`throw-string` 作用とは異なり) ジェネリックな作用だ。すなわち、`get` 作用が持つ演算は、作用に与えられた型引数の値を返すということだ。

この作用から値を2つ取ってきて、割り算をする関数を考えよう。

```koka
fun get-and-div() : <get<int>, throw-string, console> ()
  val m = get()
  val n = get()
  val result = safe-div(m, n)
  println(m.show() ++ " / " ++ n.show() ++ " = " ++ result.show())
```

この関数を、次のようにして呼び出す。
繰り返しになるが、呼び出し側は、`get<int>` と `throw-string` の2つの作用をハンドルする必要がある。
(ずっと黙ってきたが、`console` 作用はランタイムがハンドルしてくれるので、明示的にハンドルする必要はない)

```koka
with ctl throw-string(msg) println("Fatal: " ++ msg)
with ctl get() resume(10)
get-and-div()
```

`get` 演算が `10` を `resume` していることに注目してほしい。
すなわちこの処理からは `10 / 10 = 1` という出力が得られる。

これは、例外処理で例えると、例外の発生元から処理を再開できる、と捉えてもよい。

```java:疑似コード
try {
  int m = get();
  int n = get();
  println("10 / 10 = " + m / n);
} catch get() { // get() が呼び出されるとここに飛ぶ
  resume(10);   // try の中身を再開する
}
```

当然、`resume` を呼び出さなければ `try` 節の残りは捨てられる。

#### resume 関数を複数回呼び出す

`resume` 関数を呼び出すと、ハンドラーで限定された継続を再開することができると説明した。

しかし一方で `resume` はただの関数だ。
では `resume` を複数回呼び出したらどうなるだろうか？

```koka
with ctl throw-string(msg) println("Fatal: " ++ msg)
with ctl get()
  resume(1)
  resume(2)
get-and-div()
```

驚くかもしれないが、出力は次の通りだ。

```
1 / 1 = 1
1 / 2 = 0
2 / 1 = 2
2 / 2 = 1
```

`get-and-div` 関数の中では `get` 制御が2度呼び出されている。
その `get` 制御の中では `resume` が2度呼び出されているから、`safe-div` が4回実行されるのだ。

あるいは、次のように、resumeした後にメッセージを表示するようにすると分かりやすいかもしれない。

```koka
with ctl throw-string(msg) println("Fatal: " ++ msg)
with ctl get()
  resume(1)
  resume(2)
  println("Ok")
get-and-div()
```

出力は次の通りだ。

```
1 / 1 = 1
1 / 2 = 0
Ok
2 / 1 = 2
2 / 2 = 1
Ok
Ok
```

`get-and-div` 関数を再掲しよう。じっくりにらめっこしてほしい。

```koka
fun get-and-div() : <get<int>, throw-string, console> ()
  val m = get()
  val n = get()
  val result = safe-div(m, n)
  println(m.show() ++ " / " ++ n.show() ++ " = " ++ result.show())
```

#### 値ハンドラ (Value Handlers)

ハンドラには、特別な演算 `return` を定義することができる。

これは特別な演算で、ハンドラが返す高階関数が受け取るコールバックの戻り値に変更を加える演算だ。

例えば、次のようなコードを見てみよう。
これは `throw-string` 作用を `maybe` 型にする関数だ。

```koka
fun to-maybe(action :() -> <throw-string | e> a) : e maybe<a>
  with handler
    return(x)          Just(x)
    ctl raise(message) Nothing
  action()
```

ここで `return` は値ハンドラ (Value Handler) と呼ばれる特別な演算である。
何か作用をハンドルしているわけではないことに注意しよう。

ここでは `return` はハンドラが返す戻り値を `maybe` に揃えるために使われている。
さて、ハンドラが返す戻り値はどこで決定されるだろうか。

ハンドラが返す高階関数の型を確認してみよう。ハンドラが高階関数を返すことを思い出して、少しだけ脱糖しよう。

```koka
fun to-maybe(action :() -> <throw-string | e> a) : e maybe<a>
  val h = handler
    return(x)          Just(x)
    ctl raise(message) Nothing
  h(action) // h { action() } と等価
```

`action` の型は `() -> <throw-string | e> a` である。
つまり `h` の引数たるコールバック関数の型も `() -> <throw-string | e> a` である。
一方で、`to-maybe` 関数の戻り値の型から、`h(action)` の評価結果の型は `e maybe<a>` であることが分かる。

これらを踏まえると、`h` の型は `(() -> <throw-string | e> a) -> e maybe<a>` だ。

これを見れば、コールバックが無事最後まで実行された場合に得られる値 `a` を `maybe<a>` に持ち上げる存在が必要なことが分かる。
これが値ハンドラ、すなわち `return` 演算だ。

私の理解が正しければ、`return` 演算を明示しない場合、値に何も変更を加えない `id : a -> a` が暗黙的に与えられる。

#### resume 関数の戻り値

繰り返しになるが、`resume` はハンドラで限定された継続を再開することができる関数だ。

そしてその戻り値は `return` 演算で手を加えられた後の値となる。
すなわち、`return` 演算はハンドラで限定された継続の中で行われる、ということだ。

あまり面白い例ではないが、 `use-get-and-div` をまた使おう。

`return` 演算でリストを返すようにする。
すると `resume` の戻り値もリストになるため、resume の呼び出しを結合させられるようになる。

```koka
fun use-get-and-div3() : console list<()>
  with
    final ctl throw-string(msg)
      println("Fatal: " ++ msg)
      []
  with
    return(x) [x]
    ctl get()
      resume(1) ++ resume(2)
  get-and-div()
```

`get-and-div()`が実行された回数ぶん `()` が入ったリストが戻り値となる。

## 終わりに

Koka を特徴づける Effects についてと、それに触れるのに必要最低限な文法を学んだ。

個人的には、Koka のドキュメントを非常に楽しく読むことができて、満足している。
Algebraic Effects についての解説などはいくつか読んだが、やはり手で触って動かせるのがよい。
Effects は非常に直感的に動いてくれるし、Haskell のモナドスタックに苦労した身としては、Effects 抽象化の力を存分に味わうことができた。

しかしながら Koka は研究用の言語ということで、普段親切な環境に慣れ切った私には独特の苦労があった。

* コンパイルエラーの内容が読みづらい (何ならコンパイラが例外で落ちる)
  * これが一番困る
* 公式のドキュメント以外の資料が見つからない
  * その公式のドキュメントもあまり網羅されていない
  * パターンマッチのような基本的な文法を手探りした
  * named effects の良さはまだよく理解できていない
* 標準ライブラリが貧弱
  * 当然、バイナリの共有サービスやパッケージマネージャーもない
* 依然として型クラスは欲しいと感じた
  * 作用以外の抽象化機構は、研究用言語にとって蛇足になるからだろうか
  * それとも作用は型クラスの役割を完全に包含するものなのだろうか
    * 私はそうは思わないが、型クラスがない理由が知りたいと感じた

一本小さなアプリを書いてみたら、次の週末は Eff にも触ってみようと思う。

ここで紹介した文法は作用に触れるための必要最低限のものなので、もし興味を持ったら、公式の本を読んでみるといいだろう。

https://koka-lang.github.io/koka/doc/book.html

<details>
<summary>コード全文は以下</summary>

```koka
module main

fun main()
  // Hello, World
  println("Hello World")

  // 関数呼び出し
  println(greeting("John"))
  greeting("James").println()

  // 変数
  val hello = "Hello"
  var world := "World"
  world := "Monde"
  println(hello ++ " " ++ world)

  // サンプルの呼び出し
  anonymous-functions-and-trailing-lambdas()
  use-with-greeting()
  use-effect-handlers()
  use-run-server()
  use-safe-div()
  use-get-and-div()
  use-get-and-div2()
  use-to-maybe()
  use-get-and-div3().show().println()

// 関数定義
fun greeting(name : string) : total string
  "Hello, " ++ name

// 高階関数
fun do-action(action : () -> e a) : e a
  action()

fun single-arg(value : a, mapper : a -> e b) : e b
  mapper(value)

fun double-args(a : a, b : b, mapper : (a, b) -> e c) : e c
  mapper(a, b)

// 匿名関数と trailing lambda
fun anonymous-functions-and-trailing-lambdas() : console ()
  do-action fn() {
    println("Hello, trailing lambdas")
  }
  do-action {
    println("Hello, anonymous functions with no parameters")
  }
  do-action
    println("Hello again, omitted curly braces")
  "Lambda with a parameter".single-arg fn (a)
    println("Hello, " ++ a)
  double-args("Hello", "World") fn(a, b)
    println(a ++ ", " ++ b)

// with 文
fun use-with-greeting() : console ()
  with with-greeting
  println("A brown fox jumps over the lazy dog")

fun with-greeting(action : () -> <console | e> a) : <console | e> a
  println("Hello, with-greeting")
  val ret = action()
  println("Bye, with-greeting")
  ret

fun with-single-arg() : console ()
  with s <- single-arg("Lambda with a parameter")
  println("Hello " ++ s)

// ==============
// 作用 (Effects)
// ==============

// 値演算
effect val is-verbose : bool

fun log-verbose(msg : string) : <is-verbose, console> ()
  if is-verbose then
    println("DEBUG - " ++ msg)

fun use-effect-handlers() : console ()
  val h = handler
    val is-verbose = True // CLI オプションから与えられると仮定する
  h {
    log-verbose("Hello, effect handlers")
  }
  // ハンドル作用の演算が1つの場合には、インデントを用いずともよい。
  val h' = handler val is-verbose = True
  h' {
    log-verbose("Hello, effect handlers without indentations")
  }
  // そして、作用ハンドラは高階関数を返すため、with 文を利用することができる。
  with handler val is-verbose = True
  log-verbose("Hello, effect handlers with 'with statement'")
  // 最後に `with handler` は頻出であるため、with 文と一緒に使う場合に限り、`handler` キーワードを省略することができる。
  with val is-verbose = True
  log-verbose("Hello, effect handlers without the handler keyword")

// 関数演算
effect log
  fun log-debug(msg : string) : ()
  fun log-info(msg : string) : ()

fun run-server() : <log> ()
  log-debug("Server starts running...")
  // ...
  log-info("Server is running")

fun use-run-server() : console ()
  with val is-verbose = True
  with handler
    fun log-debug(msg) log-verbose(msg)
    fun log-info(msg) println("INFO - " ++ msg)
  run-server()

// 制御演算
effect ctl throw-string(msg : string) : a

fun safe-div(m : int, n : int) : throw-string int
  if n == 0
    then throw-string("ZeroDivision")
    else m / n

fun use-safe-div()
  with final ctl throw-string(msg) println("Fatal: " ++ msg)
  val result = safe-div(1, 0) + 10
  println("1 / 0 + 10 = " ++ show(result))

// 制御演算の resume 関数
effect<a> ctl get() : a

fun get-and-div() : <get<int>, throw-string, console> ()
  val m = get()
  val n = get()
  val result = safe-div(m, n)
  println(m.show() ++ " / " ++ n.show() ++ " = " ++ result.show())

fun use-get-and-div() : console ()
  with final ctl throw-string(msg) println("Fatal: " ++ msg)
  with ctl get() resume(10)
  get-and-div()

fun use-get-and-div2() : console ()
  with final ctl throw-string(msg) println("Fatal: " ++ msg)
  with ctl get()
    resume(1)
    resume(2)
    println("Ok")
  get-and-div()

// 値ハンドラ (Value Handlers)
fun to-maybe(action :() -> <throw-string | e> a) : e maybe<a>
  with handler
    return(x)                 Just(x)
    ctl throw-string(message) Nothing
  action()

fun use-to-maybe()
  to-maybe {
    safe-div(1, 0)
  }.show().println()

fun show(m : maybe<int>) : string
  match m
    Just(a) -> "Just(" ++ a.show() ++ ")"
    Nothing -> "Nothing"

// resume 関数の戻り値
fun use-get-and-div3() : console list<()>
  with
    final ctl throw-string(msg)
      println("Fatal: " ++ msg)
      []
  with
    return(x) [x]
    ctl get()
      resume(1) ++ resume(2)
  get-and-div()

fun show(l : list<()>) : console string
  match l
    Nil         -> "[]"
    Cons(x, xs) -> x.show() ++ ":" ++ xs.show()
```

</details>

[^1]: (Given the importance of effect typing, the name Koka was derived from the Japanese word for effective (効果, こうか, Kōka)).

[^2]: https://koka-lang.github.io/koka/doc/book.html#why-mingen