0

考虑以下（非常简化的）示例，该示例通过对其值的附带条件来约束数据类型：

data Transport = Car | Foot | Boat

total wheels : (transport : Transport) -> {auto hasWheels : transport = Car} -> Int
wheels Car {hasWheels = Refl} = 4
wheels Foot {hasWheels = Refl} impossible
wheels Boat {hasWheels = Refl} impossible

有什么办法可以省略或总结这些impossible案例，而 Idris 仍然认为该功能是完整的吗？如果我确实留下了一个案例，我会得到类似的东西

Main.wheels is not total as there are missing cases

我也不能只是一个包罗万象的情况，因为编译器不知道_不能是 Car 所以第二行不进行类型检查：

wheels Car {hasWheels = Refl} = 4
wheels _ {hasWheels = Refl} impossible

这给

wheels _ is a valid case

我已经浏览了这篇文章中关于约束数据类型的想法，但我没有看到任何有用的方法。

在实际代码中这是简化而来的，有很多情况需要单独排出，非常笨拙。

4

1 回答 1

1

我更仔细地研究了我已经链接的问题中讨论的方法，其中一些确实允许完全省略案例。

我想出了以下似乎最适合我实际条件更复杂的实际用例的方法：

isCar : Transport -> Bool
isCar Car = True
isCar _ = False

BoolToType : Bool -> Type
BoolToType True = ()
BoolToType False = Void

total wheels
   : (transport : Transport)
  -> {auto hasWheels : BoolToType (isCar transport)}
  -> Int
wheels Car = 4

但是我真的不明白为什么 Idris 很乐意在这里省略不可能的模式，但不是在我的原始代码中，所以一个真正解释正在发生的事情的答案仍然非常有帮助。

于 2020-03-25T10:48:25.653 回答