如何指定一個數字範圍作爲Idris中的一個類型？

Question

我一直在試驗伊德里斯，它似乎應該很簡單，指定某種類型來表示兩個不同數字之間的所有數字，例如， NumRange 5 10是5到10之間的所有數字的類型。我想包含雙打/浮點數，但是對於用整數相同的類型也同樣有用。我會如何去做這件事？

Answer 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，然後將檢查該屬性。例如：MkRange 3 0 10 Refl : Range 0 10。像這樣的一個缺點是不得不提取包含的值。當然，如果你想以編程的方式構造一個實例，你需要提供證明界限確實滿足的證明，或者在允許失敗的情況下執行，如Maybe。

我們可以爲Nat s寫一個更優雅的例子，因爲對於他們我們已經有了一個庫數據類型來表示比較證明。特別是LTE，表示小於或等於。

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

現在這個數據類型很好地封裝了n≤x≤m的證明。對於許多臨時應用程序來說這將是過分的，但它肯定會顯示如何使用依賴類型來達到此目的。