💍

Onyx で定数式を活用した型表現

2023/12/29に公開

Onyx では関数定義でインターフェイスを指定する際に where というトークンを使用します。 where 句には , 区切りで複数のインターフェイスを並べることもできるのですが、インターフェイス以外に定数式を書くことも可能です。これはとても面白い機能だと思いますがこのあたりドキュメントにはびっくりするくらいサラッとしか触れられていません。

Where expressions

Compile-time constant expressions can be used alongside interfaces in where clauses. This gives the programmer even more control over the conditions their function will be called under. For example, ensuring the length of an array fits within a specific range allows us to optimize our code.

「要素数が偶数の配列を受け取って、ニコイチでペアにして足し上げた値を各計算し、元の配列の要素数の半分の要素数の配列が return される」という関数のサンプルコードです。

use core {*}

// 引数の配列の要素数が偶数で返り値の要素数がその半分である、というのを型で表現
add_pairs :: (arr: [$N] $T) -> [N/2] T where N % 2 == 0 {
    ret: [N/2] T;
    for i: 0 .. N {
        if i % 2 == 1 do continue;
        ret[i/2] = arr[i] + arr[i+1];
    }
    return ret;
}

main :: () {
    println(add_pairs(i32.[ 1, 2, 3, 4 ])); //=> [ 3, 7 ]
 // println(add_pairs(i32.[ 1, 2, 3 ]));    //=> Compile Error
}

要素数が奇数の配列を渡すとちゃんとコンパイルエラーになります。

$ onyx run src/where.onyx
(/xxxxx/src/where.onyx:4,52) Where clause did not evaluate to true.
 4 | add_pairs :: (arr: [$N] $T) -> [N/2] T where N % 2 == 0 {
                                                        ^~ 
(/xxxxx/src/where.onyx:15,22) Here is the code that caused this constraint to be checked.
 15 |     println(add_pairs(i32.[ 1, 2, 3 ]));    //=> Compile Error
                           ^

分類としては Idris とかの依存型に近い機能なんでしょうか（よく知らないし調べてない）？
あるいは C++ や Java や TypeScript などの他の言語でもこういった型表現は普通にできるもんなんですかね。

補足

この記事のサンプルコードは nightly をビルドしないと動きません（2023-12-29, v0.1.8 時点）。

nightly ビルドの方法は、インストールコマンドの末尾に nightly を足すだけです。

sh <(curl https://get.onyxlang.io -sSfL) nightly

Where expressions

Discussion