如何限制输入类型和输出类型相同？

Question

我正在通过Manning的Idris类型驱动开发。给出了一个例子，教导如何将函数限制在一个类型族中的给定类型。我们有Vehicle类型，它使用PowerSource，即Pedal或Petrol，我们需要编写一个函数refill，该类型只适用于使用汽油作为能源的车辆。

以下代码有效，但不能保证填充Car将生成Car而不是Bus。我如何需要将refill函数的签名更改为只允许在给出Car时生成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 

Answer 2

另一种可能性是做什么你需要外部。当您无法更改原始类型时，它可能是一个选项，例如如果它来自图书馆。或者，如果你不想让你的类型混乱很多额外的索引，你可能想添加更多的属性。

让我们重用VehicleType型由@Shersh介绍：

​​3210

现在，让我们定义一个函数，它告诉我们它的构造函数用于构造车辆。它使我们能够说明我们的财产退出consice：

total 
vehicleType : Vehicle t -> VehicleType 
vehicleType Bicycle = BicycleT 
vehicleType (Car _) = CarT 
vehicleType (Bus _) = BusT 

现在我们可以说，refuel保持车辆的类型：

total 
refuelPreservesVehicleType : vehicleType (refuel v x) = vehicleType v 
refuelPreservesVehicleType {v = (Car _)} = Refl 
refuelPreservesVehicleType {v = (Bus _)} = Refl