How to limit input type and output type to the same?

Question

I am going through Model Development with Idris from Manning. An example is given that describes how to restrict a function to a given type in a type family. We have a Vehicle type that uses PowerSource , which is either Pedal or Petrol , and we need to write a refill function, which typechecks only for vehicles that use gasoline as a power source.

The code below works, but does not guarantee that refueling Car will create a Car , not a Bus . How do I change the signature of the refill function to allow the creation of a Car when specifying a Car and the creation of a Bus when specifying a 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

This can be achieved by introducing a new VehicleType data VehicleType and adding another parameter to Vehicle as follows:

 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 

You must somehow encode the type difference between the constructors. If you need extra type safety, you need to add extra type information. Then you can use it to implement the refuel function:

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

Replacement

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

with

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

results in an error of the following type:

 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

Another possibility is to do what you want from the outside. This may be an option when you cannot change the original type, for example. if it comes from the library. Or if you do not want to clutter your type with too many additional indexes that you can add to add more properties.

VehicleType use of the VehicleType type introduced by @Shersh:

 data VehicleType = BicycleT | CarT | BusT 

Now we define a function that tells us which constructor was used to build the vehicle. This allows us to declare that our property is completed:

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

And now we can say that refuel saves the type of vehicle:

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