伊德里斯 - 基於可判斷財產的類型計算不typecheck

我在伊德里斯面臨一個問題，在那裏我想創建一個基於可判斷財產的類型級別「檢查」，如果屬性持有我得到我想要的類型，但如果屬性失敗，我得到Unit（()），表明程序處於不一致狀態（如果我決定將它用作我的原始類型，則不應編譯）。伊德里斯 - 基於可判斷財產的類型計算不typecheck

下面是一個例子：

TestType : {k : Nat} -> Nat -> Vect k Nat -> Type 
TestType n ls with (isElem n ls) 
    TestType n ls | Yes _ = Nat 
    TestType n ls | No _ =() 

mkTestTypeFromNat : (n : Nat) -> (ls : Vect k Nat) -> Elem n ls -> Nat -> TestType {k=k} n ls 
mkTestTypeFromNat n ls prf res = res 

mkTestTypeFromUnit : (n : Nat) -> (ls : Vect k Nat) -> Not (Elem n ls) -> TestType {k=k} n ls 
mkTestTypeFromUnit n ls prf =()

當我嘗試編譯此，它讓我看到以下錯誤：

When checking right hand side of mkTestTypeFromNat: 
Type mismatch between 
      Nat (Type of n) 
    and 
      with block in Extensible_Records.TestType n 
                k 
                ls 
                (isElem n ls) (Expected type) 

When checking right hand side of mkTestTypeFromUnit: 
Type mismatch between 
      () (Type of()) 
    and 
      with block in Extensible_Records.TestType n 
                k 
                ls 
                (isElem n ls) (Expected type)

在每一種mkTestTypeFrom_功能我提供deciable財產證明，要麼是元素在列表中的證明，要麼是證明它不是。 typechecker不應該認識到它有這些證明，並且能夠毫無問題地計算with (isElem n ls)節，並在每種情況下給我正確的類型？或者我錯過了什麼來說服這樣的類型分析者？

來源

2015-09-28 gonzaw

只有擁有證據才能真正幫助您，直到您使用它。這是我可以爲你的類型提出的最好的;我不知道代碼是否會得到明智的優化，或者如果有辦法讓它們有效，否則。編譯器肯定會認識到每個案例分析只有一個可到達的分支。我不太清楚的是，是否會意識到它不需要評審監票人。

mkTestTypeFromNat : (n : Nat) -> (ls : Vect k Nat) -> Elem n ls -> Nat -> TestType {k=k} n ls 
mkTestTypeFromNat n ls prf res with (isElem n ls) 
    mkTestTypeFromNat n ls prf res | (Yes x) = res 
    mkTestTypeFromNat n ls prf res | (No contra) = absurd (contra prf) 

mkTestTypeFromUnit : (n : Nat) -> (ls : Vect k Nat) -> Not (Elem n ls) -> TestType {k=k} n ls 
mkTestTypeFromUnit n ls prf with (isElem n ls) 
    mkTestTypeFromUnit n ls prf | (Yes x) = absurd (prf x) 
    mkTestTypeFromUnit n ls prf | (No contra) =()

來源

2015-09-28 08:56:32 dfeuer

伊德里斯 - 基於可判斷財產的類型計算不typecheck

回答

相關問題