Config Validations


#1

I’m completely new to dhall but I really like what I’m seeing so far playing with it. One thing that I don’t have a good idea about after reading docs/tutorials is the validation story and what is the suggested path to take here.

By validation I mean things like:

  • Make sure that opacity field in the final config is 0 <= opacity <= 100
  • Make sure that minReplicas <= maxReplicas

For this simple case I saw Assertions, but I also saw it mentioned that these only execute at type-checking time - which I don’t fully understand consequences of.

I can see how the validation could require things that are outside of the scope of the language:

  • regexes
  • remote calls to validate that referenced entities exist

To me the configuration as code is great but it requires a validation layer that allows to express more than what the type system provides. The problem with this is that if we require another language to run the validations on the final object outputted by dhall (say Python or Kotlin) then there is always a question: why not use the same language to describe the configuration in the first place - it’s much simpler for the end user, they have to learn one (say Python) instead of two (dhall + Python) languages and config creation and config validation share exactly the same representations in code. Of course I understand the advantages that dhall provides (like no being Turing complete) that brought me to it in the first place but I just feel it’s not a complete ecosystem without validations. Would really love to know your thoughts on this!


#2

I believe what you want is possible. There are two similar solutions, depending on whether or not you wish to package and reuse the validation logic.

Non-reusable validation

If you don’t intend to package the validation into a reusable function, you can inline the validations after the config is defined, like this:

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

let config = { opacity = 101, minReplicas = 4, maxReplicas = 4 }

let validOpacity =
      assert : Prelude.Natural.lessThanEqual config.opacity 100 ≡ True

let validReplicas =
        assert
      :   Prelude.Natural.lessThanEqual config.minReplicas config.maxReplicas
        ≡ True

in  config

… which correctly rejects the configuration with the following error message:

% dhall --file example.dhall            

Use "dhall --explain" for detailed errors

Error: Assertion failed

- False
+ True

6│       assert : Prelude.Natural.lessThanEqual config.opacity 100 ≡ True
7│

Reusable validation

You can also package a reusable validation function to share with others, like this:

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

let Config = { opacity : Natural, minReplicas : Natural, maxReplicas : Natural }

let validateConfig =
        λ(config : Config)
      → let validOpacity = Prelude.Natural.lessThanEqual config.opacity 100

        let validReplicas =
              Prelude.Natural.lessThanEqual
                config.minReplicas
                config.maxReplicas

        in  { validOpacity, validReplicas }

let config
    : Config
    = { opacity = 101, minReplicas = 4, maxReplicas = 4 }

let validate =
        assert
      : validateConfig config ≡ { validOpacity = True, validReplicas = True }

in  config

… and the error message it produces helpfully highlights the invalid field:

% dhall --file example.dhall            

Use "dhall --explain" for detailed errors

Error: Assertion failed

{ validOpacity = - False
                 + True
, …
}

21│         assert
22│       : validateConfig config ≡ { validOpacity = True, validReplicas = True }
23│

example.dhall:21:9

Appendix: Invalid solution

Just for completeness, here is an incorrect solution that many people might attempt on their first try:

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

let Config = { opacity : Natural, minReplicas : Natural, maxReplicas : Natural }

let validateConfig =
        λ(config : Config)
      → let validateOpacity =
              assert : Prelude.Natural.lessThanEqual config.opacity 100 ≡ True

        let validateReplicas =
                assert
              :   Prelude.Natural.lessThanEqual
                    config.minReplicas
                    config.maxReplicas
                ≡ True

        in  config

let theConfig
    : Config
    = { opacity = 101, minReplicas = 4, maxReplicas = 4 }

in  validateConfig theConfig

That never succeeds because the type-checker is checking that the assertions are true for all possible inputs to the validateConfig function, and the type-checker correctly infers that there can potentially be some inputs that might fail the assertions.