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

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