如何约束输入类型和输出类型相同？

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

另一种可能是在外部做你想做的。当您无法更改原始类型时，这可能是一个选项，例如如果它来自图书馆。或者，如果您不想使用太多额外的索引来扰乱您的类型，您可能希望添加这些索引来声明更多属性。

让我们重用@Shersh 引入的 VehicleType 类型：

data VehicleType = BicycleT | CarT | BusT

现在，让我们定义一个函数，告诉我们使用哪个构造函数来构造车辆。它允许我们声明我们的属性戒烟意识：

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

如何约束输入类型和输出类型相同？

How to constraint input type and output type to be the same?

type-safety

dependent-type

idris