Type safety/polymorphism

#1

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!

#2

Dhall is structurally typed, meaning that equality of types is determined by their shape. For example, your CarDoor and LorryDoor type are the same type as far as Dhall is concerned; the fact that they have different names when you let-bind them does not affect how the interpreter thinks about them. It’s the same as if you had written:

let Door = { size : Natural }

let CarDoor = Door

let LorryDoor = Door

let Vehicle = { door : Optional Door }

let Car = Vehicle

let Lorry = Vehicle

…

… which means that your add_door_to_car and add_door_to_lorry function are the same function and are already interchangeable.

Dhall does not have anything like Haskell’s newtype to create distinct types that have the same shape, and generally it’s not idiomatic to try to implement newtypes in Dhall. But if you really want to try try then you can simulate something like it by wrapping the type in a record with a distinct field, like this:

let Door = { size : Natural }

let CarDoor = { car : Door }

let LorryDoor = { lorry : Door }

…

… or more generally you could do:

let Newtype = Type → Type

let Door = λ(newtype : Newtype) → newtype { size : Natural }

let Vehicle = λ(newtype : Newtype) → newtype { door : Optional (Door newtype) }

let Car : Newtype = λ(type : Type) → { car : type }

let Lorry : Newtype = λ(type : Type) → { lorry : type }

let CarDoor = Door Car

let LorryDoor = Lorry Door

let CarVehicle = Vehicle Car

let LorryVehicle = Vehicle Lorry

in  { CarDoor, LorryDoor, CarVehicle, LorryVehicle }

… which evaluates to:

{ CarDoor = { car : { size : Natural } }
, CarVehicle = { car : { door : Optional { car : { size : Natural } } } }
, LorryDoor = { lorry : { size : Natural } }
, LorryVehicle = { lorry : { door : Optional { lorry : { size : Natural } } } }
}

The downside of that is you can’t easily write an add_door_to_vehicle function that can be used on both types of vehicles because now they are distinct types.

1 Like
#3

Thank you. My example above was not a very good one, I hadn’t thought that it would have worked anyway because of structural typing. In the real-life situation, the two types of door (CarDoor and LorryDoor) are different record types with different attributes, so structural typing would not apply. I have, say, m different functions that operate on vehicles (eg, copy_driver_side_door_to_passenger_side), and n different vehicle types. As far as I can see, this requires me to have m * n different functions in total, and the code for eg copy_driver_side_door_to_passenger_side_for_car is exactly the same as copy_driver_side_door_to_passenger_side_for_lorry, except with the types changed.

I don’t feel completely confident in assessing which FP idiom would reduce duplication, but I guess something like the thing that goes by the name of abstract types in Scala (apologies, I don’t trust my Haskell knowledge enough to be confident about what it’s called in that language), ie:

let Vehicle = {
     DoorType : Type
     , Doors : List DoorType
}

Which would allow functions like copy_driver_door_to_passenger_side that could be polymorphic across all vehicle types.