2.3 KiB
| date |
|---|
| 2023-12-07T17:36:32+0900 |
#programming-language
メタプログラミングの技法の一種。MetaOCamlなどが有名
https://www.pls-lab.org/en/multi-stage-programming
Scalaのバージョン3にも導入されてるらしい
https://logmi.jp/tech/articles/324146
日本語での詳細な解説
MetaOCaml を使った自己反映言語のコンパイル 浅井 健一 (Black ) http://www.is.ocha.ac.jp/~asai/jpapers/ppl/asai14.pdf
メタプログラミングのための時相論理に基づく型付 λ 計算 湯瀬 芳洋 五十嵐 淳 http://www.fos.kuis.kyoto-u.ac.jp/~igarashi/papers/pdf/lambdaCB-PPL05.pdf
筑波大学 論理と計算（2） http://www.cs.tsukuba.ac.jp/~kam/lecture/gairon2-2012/gairon2.pdf
λ○: nextとprevを導入
MetaML nextとprevに加えてrunを導入
MacroML MetaMLをバックエンドにマクロとしてのわかりやすいシンタックス(letmac)とかを導入？
λ□: box(cross-stage persistence)を導入
λ○□：両方を統合
依存型との組み合わせ
A Dependently Typed Multi-Stage Calculus
https://link.springer.com/chapter/10.1007/978-3-030-34175-6_4
Let’s consider an application, for example, in computer graphics, in which we have potentially many pairs of vectors of the fixed (but statically unknown) length and a function—such as vector addition—to be applied to them. This function should be fast because it is applied many times and be safe because just one runtime error may ruin the whole long-running calculation. Our goal is to define the function
vaddof type $$Πn : Int.∀β.⊲β(Vector (%_αn) → Vector (%_αn) → Vector (%_αn))$$ .It takes the length n and returns (β-closed) code of a function to add two vectors of length n. The generated code is run by applying it to ε to obtain a function of typeVector\; n → Vector\; n → Vector\; nas expected.
この辺はなんかやりたいことに近そうな予感がする
Rustでのプログラム合成
https://fitzgeraldnick.com/2018/11/15/program-synthesis-is-possible-in-rust.html
impl Return typeと組み合わせたらもっと派手なことできそう