Modeling vehicle maintenance with GADTs in F#

VehicleMaintenance.fs

module VehicleMaintenance

open TypeEquality // See my other gists for this module

(*
A vehicle shop can perform certain maintenance procedures on cars and bicycles. Every maintenance procedure has a price.
For bicycles prices are fixed. For cars the price may depend on engine capacity.
*)

// Vehicles and prices

type Car = {
    EngineCapacity : decimal
}

type Bicycle = Bicycle

type Price = Price of decimal

// All maintenance procedures are represented by a single type. It is a GADT where the type parameter determines which
// vehicle(s) the procedure is applicable to.

type Maintenance<'v> =
    /// Oil change is applicable only to automobiles.
    | ChangeOil of TEq<'v,Car>
    /// Only bicycles have a chain.
    | ChainTension of TEq<'v,Bicycle>
    /// Both bicycles and automobiles need correct tyre pressure. Correspondingly the type parameter is not constrained.
    | TyrePressure

// Helpers for creating `Maintenance` values

let changeOil = ChangeOil TypeEquality.refl
let chainTension = ChainTension TypeEquality.refl
let tyrePressure = TyrePressure // For symmetry only, this helper does not do much

// Finally, a function which computes the price of a maintenance procedure for a vehicle.

let price (vehicle : 'v) (procedure : Maintenance<'v>) : Price =
    match procedure with
    // Tyre pressure procedure for both cars and bicycles costs the same.
    | TyrePressure -> Price 10M
    // Chain tension for bicycles is fixed price.
    | ChainTension _ -> Price 12M
    // The price for changing oil depends on the engine capacity of the car.
    | ChangeOil isCar ->
        // The vehicle is actually a car in this cases; guaranteed by the type system. The type annotation illustrates
        // this but, as expected, is not required.
        let car : Car = TypeEquality.coerce isCar vehicle // We went from `v` to `Car`!
        // Compute with the `Car` value normally
        if car.EngineCapacity <= 2000M then Price 30M else Price 40M

// Examples

// Does not type check: good
// let example1 = price { EngineCapacity = 1500M } chainTension

// Similarly does not type check: good
// let example2 = price Bicycle changeOil

// Both are OK
let example3A = price { EngineCapacity = 1500M } tyrePressure
let example3B = price Bicycle tyrePressure

// Examples of vehicle-specific maintenance procedures
let example4 = price { EngineCapacity = 1500M } changeOil
let example5 = price Bicycle chainTension

(*
DISCUSSION

What are the interesting and special properties here? There are several.

First, _all_ maintenance procedures are captured by a single DU and not two DUs for cars and bicycles separately. At the
same time, it is possible to differentiate procedures when needed, due to the type parameter. This being (an
approximation of) a generalized algebraic data type (GADT), the differentiation is explicit and type safe.

Second, function `price` has an interesting signature. It is polymorphic in vehicle type without any constraints on the
vehicle type parameter `v`! In particular, the function does not require vehicle types to implement a common interface.
It seems impossible for the function to differentiate vehicles by types without any constraints without reflection or
similar. Yet, no reflection or type pattern matching happens in the function. The technique is that the type variable of
`procedure` GADT explicitly matches the vehicle type. This not only ensures on the type level that only _compatible_
vehicles and procedures are passed to the function, but is enough to "replace" constraints using the machinery of module
`TypeEquality`.

It is worth repeating again that the model makes it impossible, using types, to compute the price of a maintenance
procedure for a vehicle which does not require the said maintenance! This can be seen in the examples above.

Continuing the second point above, the vehicle is "refined" to value `car : Car` by function `coerce` which applies the
"proof" `isCar` that `vehicle` is actually a `Car`. This is ensured by the "shared" type parameter `v` in the signature
of the function. Of course, it is possible to add more cases to the `Maintenance` DU for both cars or bicycles. Then
there would be more cases to match on as always with DUs; in each of those cases the "proof" can be used to recover the
concrete type of the vehicle, based on the type information carried by the `Maintenance` value.

*)