14

私は Idris で実験してきましたが、2 つの異なる数値の間のすべての数値を表すために、ある種の型を指定するのは簡単なはずです。たとえばNumRange 5 10、5 から 10 までのすべての数値の型です。浮動小数点数ですが、整数で同じことを行うための型も同様に役立ちます。どうすればこれを行うことができますか？

4

1 に答える 1

10

実際には、必要に応じて境界を単純にチェックする方がよい場合もありますが、データ型を記述してそのようなプロパティを強制することは確かにできます。

それを行う簡単な方法の1つは次のとおりです。

data Range : Ord a => a -> a -> Type where
  MkRange : Ord a => (x,y,z : a) -> (x >= y && (x <= z) = True) -> Range y z

Ord特殊化する必要があるかもしれませんが、型クラスの上に一般的に書きました。範囲要件は式として表されるため、Refl作成時に a を指定するだけで、プロパティがチェックされます。例: MkRange 3 0 10 Refl : Range 0 10. このようなものの欠点の 1 つは、含まれている値を抽出しなければならないという不便さです。もちろん、プログラムでインスタンスを構築したい場合は、境界が実際に満たされていることを証明する必要がありますMaybe。

Nats については、比較証明を表すライブラリ データ型が既にあるので、より洗練された例を問題なく書くことができます。特にLTE、以下を表します。

data InRange : Nat -> Nat -> Type where
  IsInRange : (x : Nat) -> LTE n x -> LTE x m -> InRange n m

このデータ型は、n ≤ x ≤ m の証明をうまくカプセル化しています。多くのカジュアルなアプリケーションではやり過ぎですが、依存型をこの目的で使用する方法を示しています。

于 2015-02-10T16:16:01.843 に答える