AtCoderでKokaを使うときのTips ::

2023年8月に行なわれた言語アップデートにより AtCoder で Koka が使えるようになりました。この記事では Koka を使って問題を解くときに役に立ちそうな情報を書いていきます。

注意

最初に筆者は Koka にそこまで詳しくなく、公式ドキュメントも通読していません。Koka が AtCoder に入ってから少しだけ真面目に書くようになりました。なので、記述に誤りがあるかもしれません。

次に本記事で使っている Koka コンパイラのバージョンは AtCoder にインストールされている v2.4.0 です。Koka は開発途中のプログラミング言語であり、バージョンを重ねていくと、ここに書かれているプログラムのコンパイルが通らなくなる可能性があります。

また、Koka コンパイラは JavaScript バックエンドや WASM バックエンドを持ちますが、ここでは AtCoder と同じく C バックエンドを使う (一旦 C 言語に変換してからバイナリファイルを生成する) ことを想定しています¹。

最後に本記事では Koka 自体の説明はしません。ご興味のある方は公式ドキュメントをご覧ください。

シンタックスハイライトを使いたい

Visual Studio Code を使っている場合は Koka Syntax Highlighting という拡張機能が公式から提供されていて、インストールすることでシンタックスハイライトが有効になります。注意として、似た拡張機能に koka がありますが、最後に更新されたのが6年前 (2023年10月24日時点) と古いです。

また、Emacs や Vim など他のエディタもサポートされているようで、support ディレクトリに必要なファイルが置かれているようです。

parseは速くない

std/text/parseが提供しているパーサーコンビネーターはあまり速くありません。空白区切りの値を読み込むときはsplitで分割して、分割された文字列を適切な型に変換した方が速いです。

例えば、新ジャッジテストコンテスト -Algorithm-で出題された Add One Edge において、パーサーコンビネーターを用いた実装は TLE しましたが、split を用いた実装 (入力を受け取る部分以外は同じ実装) は TLE せず、十分早い時間で AC しました。

パーサーコンビネーターを用いた実装: 2183 ms で TLE (https://atcoder.jp/contests/newjudge-2308-algorithm/submissions/44338567)
split、parse-intを用いた実装: 189 ms で AC (https://atcoder.jp/contests/newjudge-2308-algorithm/submissions/44346224)

入力を受け取る処理は何度も書くことになるので、次のような関数を用意しておくと良さそうです。

fun read-ints(): <console,exn> list<int>
    readline().split(" ").map(fn(s) { s.parse-int.unjust })

readline関数は最大 1022 文字しか読まない

std/os/readlineのreadline関数は必ずしも1行分の文字列を読み取るとは限りません。このことは標準ライブラリのドキュメントに記載があります (引用元, 2023年8月16日に確認)。

Read chararacters until either a newline is encountered (not included in the result), or 1023 characters have been read.

改行文字を読んでいなくても一定文字数を読んでいたらそれまでの文字列を返します。なお、上の文章では 1023 文字までと書かれていますが、正確には 1022 文字です²。

この仕様は1行に長い文字列や大量の整数が書かれているときに問題になります。例えば、Language Test 202301 で出題された Shift only を解くときに困ります。そのようなときはstd/os/fileのread-text-file関数を使って一度入力全体を読み込むとよいです。実装例はこちらの提出をご覧ください。

println は flush をしない

インタラクティブ形式の問題では出力の度に flush することが要求されますが、println関数は flush を行ないません。そのため、手動で flush する必要があります。flush する関数は C 言語を埋め込むc inline ...を使って次のように書けます。

// 注意: fun ではなく extern
extern flush() : console ()
    c inline "(fflush(stdout))"

Koka だけでは厳しそうで、C 言語を埋め込まないと無理そうなことは時々あるので、externとc inlineは頭の片隅に置いておきたいです。

`ref<vector<a>>` が指す vector の更新には modify を使う

参照 (ref<a>) の指す vector はmodify関数 (リンク) を使って、次のように更新します。

// r : ref<vector<a>>
r.modify fn(v)
    // v は r が指す vector
    // v の i 番目の要素を x に変更する
    v[i] := x

試していませんが、ref<vector<ref<vector>>>のような多次元の可変 vector の変更もmodifyを入れ子にすればできそうです。

関数とその内部にある関数の両方で var を使っていると面倒なことが起きる

注記: ここの内容を正確に書くにはコンパイルの挙動を詳しくなる必要があるのですが、時間を割く余力がないので怪しいメンタルモデルを提示するのに留めています。

例を出すと、次のコードはコンパイルが通りません。

fun say-kuku()
    // say-kuku のスコープと while の第2引数に指定した関数のスコープで var を使用している
    var i := 1
    // 関数であることを強調するために省略記法を用いていない
    while({ i <= 9 }, fn() {
        var j := 1
        while { j <= 9 }
            if j > 1 then " ".print
            (i * j).show.pad-left(2, ' ').print
            j := j + 1
        i := i + 1
        "".println
    })

このコードのコンパイルが通らない原因を自分は以下のような感じで理解しています (注意: 間違っています)。

ローカル変数を宣言したスコープごとにハンドラが挿入される (注意: プログラムの中間表現³を見ると分かりますが、実際には挿入されてはいなさそうです)。上のコードだと次のようなコードに変換される。

// 注意: このコードは正確ではありません
fun say-kuku()
    // ハンドラを挿入
    with handle-local-variables-in-say-kuku
    var i := 1
    while({ i <= 9 }, fn() {
        // ハンドラを挿入
        with handle-local-variable-in-annonymous-function-2
        var j := 1
        while { j <= 9 }
            if j > 1 then " ".print
            (i * j).show.pad-left(2, ' ').print
            j := j + 1
        i := i + 1
        "".println
    })

内側のスコープでiにアクセスしたとき、外側のハンドラを使わなければならないが、内側のハンドラが使われてしまう。これがコンパイルエラーを生じさせる。

このメンタルモデルを信じることにすると、iへアクセスするときにエフェクトのマスキング (詳しくは公式ドキュメントのMasking Effectsをご覧ください) をすればコンパイルが通りそうです。実際、次のコードはコンパイルが通り、正常に動作します。

fun say-kuku'()
    var i := 1
    while({ i <= 9 }, fn() {
        var j := 1
        val i' = mask<local>{ i }
        while { j <= 9 }
            if j > 1 then " ".print
            (i' * j).show.pad-left(2, ' ').print
            j := j + 1
        mask<local>{ i := i + 1 }
        "".println
    })

他の解決策にjもsay-kuku'のスコープに持ってくるというのがあります (昔の C 言語みたい)。

`ref<a>` を要素に持つ vector を作りたいときは vector(n, ref(init)) した後に for 文で再代入する

まず、参照を要素に持つ vector はvector-init関数では作れません。なぜかというと、vector-initの第2引数として指定する位置ごとの初期値を計算する関数はエフェクトを発生させてはいけませんが、参照を作成するとalloc<h>というエフェクトが生じてしまうからです。

そのため、vector-init関数ではなくvector関数を使う必要があります。しかし、vector(n, ref(init))だけだとすべての参照が同じ reference cell を指してしまいます (Python で[[]] * 10、OCaml でArray.make 10 [| |]と書いたときに起こる問題と同じです)。なので、後で再代入しなければいけません。

val v = vector(10, ref(0))
// この行の時点では v[i] はすべて同じ reference cell を指す
for (0, v.length - 1) fn(i)
    v[i] := ref(0)
// この行の時点で各 v[i] は相異なる reference cell を指す

同じ名前の関数を区別して呼び出す

Koka は関数のオーバーロードが可能です。そのために関数名から型が一意に定まらず、時折型推論がうまくいかないことがあります。

そのようなときは(show: (bool) -> string)(x)のように型注釈を加えたり、std/num/int64/andのように関数名の前にその関数が属するモジュールの名前を書いたりするといいです。

string は `vector<char>` に変換して使う

string型には指定した位置の文字を返す関数がありません。文字列の一部を表す型であるssliceの関数を使うとそのような関数が書けますが、 $i$文字目のアクセスが$\Theta(i)$になってしまいます。そのため、素直にvector<char>に変換して扱うのが良さそうです。stringからvector<char>への変換にはvector関数を使います。

注意としてその逆、vector<char>からstringへの変換にはstring関数が用意されていますが、末尾に余計な文字を付けてしまうバグがあります。

> "ABC".vector.string
"ABC\U0EE0FF"

# このバグは文字列から変換したベクトル以外でも発生する
> ['A', 'B', 'C'].vector.string
"ABC\U0EE0FF"

このバグはすでに報告されており (Vector to string conversion adds an extra character · Issue #486 · koka-lang/koka)、リリースはされていないものの修正されています。 AtCoder で使うのは言語アップデートが行なわれてからが良さそうです。

early return

Koka では関数から値を返すときにreturnを使うと early return ができます。これを使うと、例えば、二分探索が次のように書けます。

fun binsearch(ok: int, ng: int, p: (int) -> e bool): e int
    if abs(ok - ng) <= 1 then return ok
    val m = (ok + ng) / 2
    if p(m) then binsearch(m, ng, p)
    else binsearch(ok, m, p)

なお、Koka ではreturnを書かなくても最後に評価された式の値が戻り値になりますが、その場合は early return は行なわれません。例えば、次のようにcount-downを定義したうえでcount-down(10)を実行すると-1以降も出力されて、停止しません。

fun count-down(n: int): console ()
    if n < 0 then ()
    n.println
    // -1 で止まってくれるはずなので unsafe-decreasing を付けて div を取り除く
    count-down(unsafe-decreasing(n.dec))

fold-int のドキュメントでの記述と実際の挙動が異なる

fold-int関数はドキュメントで次のように説明されています (引用元)。

fold over the integers between [start,end] (inclusive).

しかし、以下の式を評価すると1から9までが表示され、10は表示されないことからも分かるように、実際には[start, end) (= [start, end - 1])内の整数を畳み込んでいます。

fold-int(1, 10, 0, fn(i, acc) { i.println; acc + i })

追記 (2024/5/10): ドキュメント通りにする PR を出してマージされました (Fix off-by-one bug in range/fold* · Pull Request #466 · koka-lang/koka)。v3.1.0 から変更が適用されます。

関数のパラメータにはパターンを指定できる

関数のパラメータとしてパターンを指定すると、そこでパターンマッチングを行なえます。次の例ではパラメータ部分にタプルのパターンを指定しています。

fold-int(1, 10, (0, 1), fn((s, p), i) { (s + i, p * i) })

プログラムの一部の型を調べる

注記: より簡便な方法がありそうです。

(必要ならば) 型を調べたいプログラムを関数として切り出し、適当な名前を付ける。
koka (ファイルパス) --html --htmlcss koka.css --outputdir docsを実行する。実行するとdocs/にドキュメントとなる HTML ファイルが生成される (標準ライブラリのドキュメントと同じ形式)。
Koka のリポジトリからkoka.css(2023年11月2日時点の master ブランチだとdoc/koka.css)をダウンロードして、docs/に配置する。
docs/(ファイル名).xmp.htmlをブラウザで開き、見たい関数の名前をクリックして、そのプログラムを表示する。その後、型を知りたい部分にカーソルを合わせると型が表示される。

余談ですが、AtCoder では C 言語からのコンパイルには gcc を使用しているようです。 ↩︎
実装を読んでみると、fgets(buf, 1023, stdin)を呼び出していることが分かります。fgetsは第2引数から1だけ引いた数の文字を読み込むので、1023 - 1 = 1022 文字まで読み込むことになります。 ↩︎
kokaコマンドに--coreオプションを付けると.kokaディレクトリ内に core file (拡張子は.kkc) が生成されます。また、--showcoreオプションを付けると標準出力にその内容が表示されます。 ↩︎

AtCoderでKokaを使うときのTips

注意 #

シンタックスハイライトを使いたい #

parseは速くない #

readline関数は最大 1022 文字しか読まない #

println は flush をしない #

ref<vector<a>> が指す vector の更新には modify を使う #

関数とその内部にある関数の両方で var を使っていると面倒なことが起きる #

ref<a> を要素に持つ vector を作りたいときは vector(n, ref(init)) した後に for 文で再代入する #

同じ名前の関数を区別して呼び出す #

string は vector<char> に変換して使う #

early return #

fold-int のドキュメントでの記述と実際の挙動が異なる #

関数のパラメータにはパターンを指定できる #

プログラムの一部の型を調べる #

注意