Loading article…
型理論において、洗練型[1] [2] [3]は、洗練型の任意の要素に対して成立すると想定される述語を備えた型である。洗練型は、関数の引数として使用される場合の前提条件、または戻り値の型として使用される場合の事後条件を表現できる。たとえば、自然数を受け入れ、5より大きい自然数を返す関数の型は、 と記述される。したがって、洗練型は動作サブタイピングに関連している。
歴史
洗練型の概念は、1991年のフリーマンとフェニングの「MLの洗練型」[1]で初めて導入されました。これは、標準MLのサブセットの型システムを提示しています。この型システムは、「MLの型推論の決定可能性を保持」しながらも、「コンパイル時により多くのエラーを検出できるようにします」。最近では、Haskell、[4] [5] TypeScript、[6] Rust [7]やScalaなどの言語向けに洗練型システムが開発されています。
参照
参考文献
- ^ ab Freeman, T.; Pfenning, F. ( 1991). 「ML の改良型」(PDF) . ACM プログラミング言語の設計と実装に関する会議の議事録。pp. 268–277。doi :10.1145/113445.113468。
- ^ Hayashi, S. (1993). 「リファインメント型の論理」.証明とプログラムのための型に関するワークショップの議事録. pp. 157–172. CiteSeerX 10.1.1.38.6346 . doi :10.1007/3-540-58085-9_74.
- ^ Denney, E. (1998). 「仕様の洗練型」。プログラミングの概念と方法に関する IFIP 国際会議の議事録。第 125 巻。Chapman & Hall。pp. 148–166。CiteSeerX 10.1.1.22.4988。
- ^ Vazou, Niki. Liquid Haskell: Haskell のリファインメント型。第 45 回 ACM SIGPLAN プログラミング言語の原理に関するシンポジウム (POPL 2018)。
- ^ Volkov, Nikita (2015). 「Haskell ライブラリとしてのリファインメント型」
- ^ Panagiotis, Vekris; Cosman, Benjamin; Jhala, Ranjit (2016). 「TypeScript のリファインメント型」。プログラミング言語の設計と実装に関する第 37 回 ACM SIGPLAN カンファレンスの議事録。pp. 310–325。arXiv : 1604.02480。doi : 10.1145 /2908080.2908110 。
- ^ Lehmann, Nico; Geller, Adam T.; Vazou, Niki; Jhala, Ranjit (2023年6月6日). 「Flux: RustのLiquid型」. ACM on Programming Languagesの議事録. 7 (PLDI): 169:1533–169:1557. doi : 10.1145/3591283 .