依赖类型的函数不是完全的,但是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

当我检查wheelsREPL 的总数时,

:total wheels
Main.wheels is Total

因为我没有处理Tram类型wheels,我不明白怎么wheels可以总计.我误解了"总"是什么意思吗？

Answer 1

这是因为wheels Motorcycle它Motorcycle作为一个变量处理,因为它没有很好地作为构造函数应用程序输入 - Motorcycle构造函数接受一个参数.

事实上,它超越了类型检查器是非常令人惊讶的,我认为这实际上是伊德里斯设计中的一个(可修复的)错误.为了避免这种错误,我认为它应该只允许模式变量自动绑定,如果它们以小写字母开头,与绑定类型变量的方式非常相似.