What is the dhall idiomatic way to associate different schemas to union values?

Question

I'm trying to represent the pipeline system of the Zuul-CI project using Dhall types: a pipeline can use different connections with different trigger events.

I'd like to provide a default pipeline that setups the correct trigger event for each type of connections in such a way that:

  ⊢ RenderPipeline CheckPipeline::{ connections = [ ConnectionTypes.GitHub ] }

  - pipeline:
    name: check
    trigger:
      github:
        action: open
        event: pull-request

  ⊢ RenderPipeline CheckPipeline::{ connections = [ ConnectionTypes.Gerrit ] }

  - pipeline:
    name: check
    trigger:
      gerrit:
        event: patchset-created

  ⊢ RenderPipeline CheckPipeline::{ connections = [ ConnectionTypes.Gerrit, ConnectionTypes.GitHub ] }

  - pipeline:
      name: check
      trigger:
        gerrit:
          event: patchset-created
        github:
          action: open
          event: pull-request

I had to use an Union for ConnectionTrigger because the merge function expects the value to be a single type.

Is there a way to somehow associate GerritTrigger with ConnectionTypes.Gerrit and avoid typing the event type in the CheckPipeline definition (e.g. remove the ConnectionTrigger.Gerrit annotation)?

let Prelude =
      https://raw.githubusercontent.com/dhall-lang/dhall-lang/v11.1.0/Prelude/package.dhall sha256:99462c205117931c0919f155a6046aec140c70fb8876d208c7c77027ab19c2fa

let ConnectionTypes
    : Type
    = < Gerrit | GitHub >

let GerritTrigger
    : Type
    = { event : Text }

let GitHubTrigger
    : Type
    = { event : Text, action : Text }

let ConnectionTrigger
    : Type
    = < Gerrit : GerritTrigger | GitHub : GitHubTrigger >

let Pipeline
    : Type
    = { name : Text
      , trigger : { Gerrit : ConnectionTrigger, GitHub : ConnectionTrigger }
      , connections : List ConnectionTypes
      }

let CheckPipeline =
      { Type = Pipeline
      , default =
          { name = "check"
          , trigger =
              -- "Here, can this be improved so that Gerrit is not mentioned twice?"
              { Gerrit = ConnectionTrigger.Gerrit { event = "patchset-created" }
              , GitHub =
                  ConnectionTrigger.GitHub
                    { event = "pull-request", action = "open" }
              }
          }
      }

let PipelineRenderTrigger
    : Type
    = { mapKey : Text, mapValue : ConnectionTrigger }

let RenderPipeline =
        λ(pipeline : Pipeline)
      → [ { pipeline =
              { name = pipeline.name
              , trigger =
                  Prelude.List.map
                    ConnectionTypes
                    PipelineRenderTrigger
                    (   λ(connection : ConnectionTypes)
                      → { mapKey =
                            merge
                              { Gerrit = "gerrit", GitHub = "github" }
                              connection
                        , mapValue = merge pipeline.trigger connection
                        }
                    )
                    pipeline.connections
              }
          }
        ]

in  RenderPipeline CheckPipeline::{ connections = [ ConnectionTypes.GitHub ] }

Thanks in advance :)

Answer 1

Yes, you can do this by transforming the triggers field before passing it as a record of handlers to merge. That way the user doesn't have to wrap the triggers themselves; the RenderPipeline function does it for them:

let Prelude =
      https://raw.githubusercontent.com/dhall-lang/dhall-lang/v11.1.0/Prelude/package.dhall sha256:99462c205117931c0919f155a6046aec140c70fb8876d208c7c77027ab19c2fa

let ConnectionTypes
    : Type
    = < Gerrit | GitHub >

let GerritTrigger
    : Type
    = { event : Text }

let GitHubTrigger
    : Type
    = { event : Text, action : Text }

let ConnectionTrigger
    : Type
    = < Gerrit : GerritTrigger | GitHub : GitHubTrigger >

let Pipeline
    : Type
    = { name : Text
      , trigger : { Gerrit : GerritTrigger, GitHub : GitHubTrigger }
      , connections : List ConnectionTypes
      }

let CheckPipeline =
      { Type = Pipeline
      , default =
          { name = "check"
          , trigger =
              { Gerrit = { event = "patchset-created" }
              , GitHub = { event = "pull-request", action = "open" }
              }
          }
      }

let PipelineRenderTrigger
    : Type
    = { mapKey : Text, mapValue : ConnectionTrigger }

let RenderPipeline =
        λ ( pipeline
          : Pipeline
          )
      → [ { pipeline =
              { name =
                  pipeline.name
              , trigger =
                  Prelude.List.map
                    ConnectionTypes
                    PipelineRenderTrigger
                    (   λ ( connection
                          : ConnectionTypes
                          )
                      → { mapKey =
                            merge
                              { Gerrit = "gerrit", GitHub = "github" }
                              connection
                        , mapValue =
                            let {- This is the key bit!

                                   We modify the handlers before passing them to
                                   `merge` so that the user does not have to
                                -}
                                trigger =
                                  { Gerrit =
                                      ConnectionTrigger.Gerrit
                                        pipeline.trigger.Gerrit
                                  , GitHub =
                                      ConnectionTrigger.GitHub
                                        pipeline.trigger.GitHub
                                  }

                            in  merge trigger connection
                        }
                    )
                    pipeline.connections
              }
          }
        ]

in  RenderPipeline CheckPipeline::{ connections = [ ConnectionTypes.GitHub ] }