功能上依賴型是不是總，而是伊德里斯認爲這是總

Question

我有一個Vehicle類型取決於PowerSource類型：

data PowerSource = Petrol | Pedal | Electric 

data Vehicle : PowerSource -> Type where 
    Unicycle : Vehicle Pedal 
    Motorcycle : (fuel: Nat) -> Vehicle Petrol 
    Tram: (battery : Nat) -> Vehicle Electric 

和功能wheels。 Tram是未處理的情況。

wheels : Vehicle power -> Nat 
wheels Unicycle = 1 
wheels Motorcycle = 2 

當我檢查的wheels從REPL總的煩躁，

:total wheels 
Main.wheels is Total 

，因爲我沒有在wheels處理Tram型，我不明白怎麼wheels可總。我誤解了「總數」是什麼意思？

Answer 1

這是因爲在wheels Motorcycle中，它將Motorcycle作爲變量處理，因爲它沒有很好地作爲構造函數應用程序類型化 - Motorcycle構造函數接受一個參數。

事實上，這通過類型檢查是非常令人驚訝的，我認爲這實際上是在伊德里斯設計（可修復）的錯誤。爲了避免這種錯誤，我認爲它應該只允許模式變量自動綁定，如果它們以小寫字母開頭，就像綁定類型變量一樣。