quartz-research-note/content/多段階計算.md

#programming-language

メタプログラミングの技法の一種。MetaOCamlなどが有名

https://www.pls-lab.org/en/multi-stage-programming

日本語での詳細な解説

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)を導入

λ○□：両方を統合

SATySFi の多段階計算入門

依存型との組み合わせ

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 vadd of 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 type Vector\; n → Vector\; n → Vector\; n as expected.

この辺はなんかやりたいことに近そうな予感がする