dependent-type - 依赖类型的功能不是全部的，但 idris 认为它​​是全部的

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

当我从 REPL 检查 wheels 的整体性时，

:total wheels
Main.wheels is Total

因为我没有处理 wheels 中的 Tram 类型，所以我不明白 wheels 怎么可能是总的。我是不是误解了“总计”的意思？

Answer 1

这是因为在 wheels Motorcycle 中，它将 Motorcycle 视为一个变量，因为它不适合作为构造函数应用程序 - Motorcycle构造函数接受一个参数。

这通过了类型检查器这一事实非常令人惊讶，我认为这实际上是 Idris 设计中的一个(可修复的)错误。为了避免这种错误，我认为它应该只允许以小写字母开头的模式变量自动绑定(bind)，就像绑定(bind)类型变量一样。