How to validate internal consistency of a config with dhall?

Question

I will start with a motivating example of a config that almost represents an envoy proxy config :)

virtual_hosts:
- name: webxp-api_http
  domains: ["*"]
  routes:
  - match: { prefix: "/static/v5.0" }
    route: { cluster: bodhi_static }
  - match: { prefix: "/"}
    route: { cluster: bodhi-web }

  clusters:
  - name: bodhi_web
  - name: bodhi_static

The rule is, that name has to be defined clusters list have to be defined to be used in the route part of the config. If you look closely, this config will fail to load, because bodhi_web is not bodhi-web. How would I encode that in Dhall?

On one hand I could have clusters as a list in a let binding, and that would help, but nothig forces me to use the binding and in reality I would like tho think of clusters as a sum-type for the cluster: field? Could dependent types help me here (i.e. I remember doing something like this in purescript, that has some limited capacity for dependent type-programming)

Or should I just create a constructor/validator function and abuse assert to get this validated?

Or I just shouldn't? :)

Answer 1

I would approach this by authoring a utility function that generates a correct-by-construction configuration.

Using your example, if we want to ensure that the list underneath the clusters field always matches the list of routes, then we derive the clusters field from the routes field:

let Prelude = https://prelude.dhall-lang.org/package.dhall

let Route = { match : { prefix : Text }, route : { cluster : Text } }

let toVirtualHosts =
          \(args : { name : Text, domains : List Text, routes : List Route })
      ->  { virtual_hosts =
                  args
              //  { clusters =
                      Prelude.List.map
                        Route
                        Text
                        (\(r : Route) -> r.route.cluster)
                        args.routes
                  }
          }

in  toVirtualHosts
      { name = "webxp-api_http"
      , domains = [ "*" ]
      , routes =
          [ { match = { prefix = "/static/v5.0" }
            , route = { cluster = "bodhi_static" }
            }
          , { match = { prefix = "/" }
            , route = { cluster = "bodhi_web" }
            }
          ]
      }

$ dhall-to-yaml --file ./example.dhall
virtual_hosts:
  clusters:
  - bodhi_static
  - bodhi_web
  domains:
  - *
  name: webxp-api_http
  routes:
  - match:
      prefix: /static/v5.0
    route:
      cluster: bodhi_static
  - match:
      prefix: /
    route:
      cluster: bodhi_web

Answer 2

My alternative attempt, heavily relying on the fact, that empty alternatives will end-up being text when converted to yaml, i.e: {cluster = <static | web>.static} is interpreted as cluster: static

This means, I can i.e:

let Clusters = < bodhi_static | bodhi_web >

let Route =
      { Type = { match : { prefix : Text }, cluster : Clusters }
      , default = {=}
      }

let Cluster = { Type = { name : Clusters }, default = {=} }

in  { matches =
        [ Route::{ match = { prefix = "/" }, cluster = Clusters.bodhi_web }
        , Route::{
          , match = { prefix = "/static" }
          , cluster = Clusters.bodhi_static
          }
        ]
    , clusters =
        [ Cluster::{ name = Clusters.bodhi_static }
        , Cluster::{ name = Clusters.bodhi_web }
        ]
    }

Bit more repetitive, but simpler i.m.o?