如何约束输入类型和输出类型是一样的？

Question

我正在与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 (Bus fuel) x        = Bus (fuel + x)

Answer 1

这可以通过引入新VehicleType数据类型并添加一个更多参数来实现Vehicle:

data VehicleType = BicycleT | CarT | BusT

data Vehicle : PowerSource -> VehicleType -> Type 
  where
    Bicycle :                 Vehicle Pedal  BicycleT
    Car     : (fuel : Nat) -> Vehicle Petrol CarT
    Bus     : (fuel : Nat) -> Vehicle Petrol BusT

你应该以某种方式编码构造函数之间的类型差异.如果您想要更多类型安全性,则需要向类型添加更多信息.然后你可以用它来实现refuel功能:

refuel : Vehicle Petrol t -> Nat -> Vehicle Petrol t
refuel (Car fuel) x        = Car (fuel + x)
refuel (Bus fuel) x        = Bus (fuel + x)

更换

refuel (Car fuel) x        = Car (fuel + x)

同

refuel (Car fuel) x        = Bus (fuel + x)

导致下一个类型错误:

Type checking ./Fuel.idr
Fuel.idr:14:8:When checking right hand side of refuel with expected type
        Vehicle Petrol CarT

Type mismatch between
        Vehicle Petrol BusT (Type of Bus fuel)
and
        Vehicle Petrol CarT (Expected type)

Specifically:
        Type mismatch between
                BusT
        and
                CarT