Hello all,
I’m encountering situations like the example below a lot in my dhall code, and I’d like to make sure I’m using the right pattern. Let’s say I have a Car
and Lorry
type, both of which have a door
attribute, and I’d like to make sure a lorry door can never be added to a car, or vice versa:
let CarDoor = {
size : Natural
}
let LorryDoor = {
size : Natural
}
let Car = {
door : Optional CarDoor
}
let Lorry = {
door : Optional LorryDoor
}
let add_door_to_car =
λ(door : CarDoor) ->
λ(car : Car) ->
car // { door = Some door }
let add_door_to_lorry =
λ(door : LorryDoor) ->
λ(lorry : Lorry) ->
lorry // { door = Some door }
let car_1 = { door = None CarDoor }
let car_1 = add_door_to_car ({ size = 5 }) car_1
in car_1
Which all works great. What would save some code, though, is to be able to use a single function to add doors to both lorries and cars, something like the example below, except one which actually works:
let Door = < car : CarDoor | lorry : LorryDoor >
let Vehicle = < car : Car | lorry : Lorry >
let add_door_to_vehicle =
λ(vehicle : Vehicle) ->
λ(door : Door) ->
merge {
car = add_door_to_car (Door.car door)
, lorry = add_door_to_lorry (Door.lorry door)
} vehicle
I’d like to avoid having one add_door_to_....
function per vehicle, whilst preserving the type safety that car doors can’t be added to lorries, or the other way round. Am I correct in thinking that that’s not possible, or am I missing something?
Thanks!