我正在与Manning的Idris进行类型驱动开发.给出了一个示例,教导如何将函数限制为类型族中的给定类型.我们有Vehicle一个使用类型PowerSource要么是Pedal或Petrol,我们需要编写一个函数refill是typechecks仅适用于使用汽油作为其powersource车辆.
下面的代码有效,但不保证重新填充a Car会产生a Car而不是a Bus.如何更改refill函数的签名以仅允许Car在给定a Car和生成Bus时生成Bus？
data PowerSource
= Pedal
| Petrol
data Vehicle : PowerSource -> Type
where
Bicycle : Vehicle Pedal
Car : (fuel : Nat) -> Vehicle Petrol
Bus : (fuel : Nat) -> Vehicle Petrol
refuel : Vehicle Petrol -> Nat -> Vehicle Petrol
refuel (Car fuel) x = Car (fuel + x)
refuel …