如何限制輸入類型和輸出類型相同？

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