コンパイル時依存型はシステムプログラミング言語に必ずやってくる
Compile-Time Dependent Types
C++のテンプレートやconstexpr、Rustのconst generics、Zigのcomptimeなど、コンパイル時計算の機能は制約が多く型システムも欠けがちだ。著者はSylという言語で、static/erasedというモードを持つ型システムにコンパイル時計算を組み込もうとしている。two-level type theoryに着想を得て、コンパイル時は依存型、実行時は単純型という設計を目指す。
つまりSylは、コンパイル時には依存型付けされ、実行時には単純型付けされる。
HNでの議論
18- nextaccountic
「コンパイル時依存型」
「コンパイル時依存型がシステムプログラミング言語に必ずやってくるのは避けられないように思える」
C++にはテンプレートとconstexprがある。Rustにはconst genericsがある。Zigにはcomptimeがある。Cにだって_Genericがある。しかし、これらの機能は高度に制限されていたり、まともな型システムを欠いていたり、あるいはその両方であることが多い。
とはいえ、これらの言語機能は依存型の例ではないのでは……
「つまり、Sylはコンパイル時には依存型付けされ、実行時には単純型付けされる」
「これがStaged Compilation with Two-Level Type Theory https://andraskovacs.github.io/pdfs/2ltt.pdf の核となるアイデアだ。ただし、これはモーダル型システムとしては提示されていない」
でも依存型（そして一般に静的型）は実行時には存在しないはずだ！
でもたぶん言いたいのは、Sylが依存型をオーバーヘッドなしで実装している、たとえば辞書渡し（dictionary passing）のようなことをしない、ということだろう。だから完全な型消去が可能なのだ。この理解で合っている？（論文を読むつもり）
- carterschonwald
すごくクール！同じ設計・影響圏に重なる長年の裏プロジェクトがあるんだけど、かなり違う方向に進めているんだ
- superxpro12
LTOはこういう類のことをどのくらいうまく最適化するんだろうね、多相関数やオブジェクトをコンパイル時に解決するために全部の手間をかけるのと比べて。