Type scaffolding / commutative composition

Viewed 67

I have 3 types : Task (a unit of work), Estimate (a time period) and User.

In my app, I'd like to "decorate" my Tasks to make EstimedTask (that could be sum-ed), AssignedTask (to be sorted) and AssignedEstimatedTask (that are both and on which I can apply a Gantt algorithm)

My first try is to implement them with tuples :

EstimatedTask :: (Task, Estimate)
AssignedTask :: (Task, User)
AssignedEstimatedTask :: (Task, Estimate, User)

but then if I want to construct an AET I have to define 3 constructors

T -> E -> U -> AET
(T, E) -> U -> AET
(T, U) -> E -> AET

As I intend to decorate even more, I'm afraid the number of constructor will explode.

Is there a smart way to do that ? In particular, is there a prefered method to make sub-constructor commutative (such that assign . estimate $ task == estimate . assign $ task ?

1 Answers

Define data Controlled :: Type -> Bool -> Type such that Controlled t False is a singleton type (like (), no information) and Controlled t True is a copy of t:

data Controlled :: Type -> Bool -> Type where
    Exists :: a -> Controlled a True
    NonExist :: Controlled a False

Then define a "full" type representing everything you can have, with Controlled slots:

data AssignedEstimatedTask' :: Bool -> Bool -> Type where
    AssignedEstimatedTask ::
        { getTask :: Task
        , taskUser :: Controlled User a
        , taskEstimate :: Controlled Estimate b } ->
        AssignedEstimatedTask' a b

Fill in a bunch of synonyms:

-- naming the types is exponential!
type JustTask = AssignedEstimatedTask' False False
type AssignedTask = AssignedEstimatedTask' True False
type EstimatedTask = AssignedEstimatedTask' False True
type AssignedEstimatedTask = AssignedEstimatedTask' True True

justTask :: Task -> JustTask
justTask t = AssignedEstimatedTask t NonExist NonExist

And now you can add things to a task by using record updates, which are tracked at compile-time:

jTask :: JustTask
aTask :: AssignedTask
eTask :: EstimatedTask
aeTask, eaTask :: AssignedEstimatedTask
-- ofc, all of ^ could have been inferred
jTask = justTask someTask
aTask = jTask { taskUser = Exists someUser }
eTask = jTask { taskEstimate = Exists someEstimate }
aeTask = aTask { taskEstimate = Exists someEstimate }
eaTask = eTask { taskUser = Exists someUser }
-- aeTask == eaTask

Working example

If you really want to extract the record updates as functions, they look like this

assignTask :: User -> AssignedEstimatedTask' a e -> AssignedEstimatedTask' True e
assignTask u t = t { taskUser = Exists u }
estimateTask :: Estimate -> AssignedEstimatedTask' a e -> AssignedEstimatedTask' a True
estimateTask e t = t { taskEstimate = Exists e }
Related