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

42 lines
2.0 KiB
Markdown
Raw Blame History

This file contains invisible Unicode characters

This file contains invisible Unicode characters that are indistinguishable to humans but may be processed differently by a computer. If you think that this is intentional, you can safely ignore this warning. Use the Escape button to reveal them.

This file contains Unicode characters that might be confused with other characters. If you think that this is intentional, you can safely ignore this warning. Use the Escape button to reveal them.

#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](https://www.sciencedirect.com/science/article/pii/S0304397500000530) nextとprevに加えてrunを導入
[[MacroML]] MetaMLをバックエンドにマクロとしてのわかりやすいシンタックス(`letmac`)とかを導入?
λ□: box(cross-stage persistence)を導入
λ○□:両方を統合
[SATySFi の多段階計算入門](https://sankantsu.hatenablog.com/entry/2022/08/19/215024)
## [[依存型]]との組み合わせ
[A Dependently Typed Multi-Stage Calculus](https://arxiv.org/abs/1908.02035)
https://link.springer.com/chapter/10.1007/978-3-030-34175-6_4
> Lets 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.
この辺はなんかやりたいことに近そうな予感がする