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!

1 Like
#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.

4 Likes
Type-checking for uniqueness in Dhall-Lang
#3

Sorry for reviving this old thread, but I’ve been struggling with this and I still can’t figure out how to “package” the validation for re-use by others. Let me show you a basic example. Here I’m trying to enforce that a Natural value is <= 9.

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

-- the config type
let Config = { gzipLevel : Natural }

-- the function that validates a config
let Config/validate = \(c : Config) -> Prelude.Natural.lessThanEqual c.gzipLevel 9

-- the config itself
let config = { gzipLevel = 8 }

-- the assertion that the config is valid
let validate = assert : Config/validate config === True

in  config

Obviously, the assertion above needs access to the config value, but my intention is for this value to be provided by the user. As it stands now, it’s static. It would seem to me that what I’m doing would require the users to “manually” add the assertion on their end, which would obviously be less than ideal.

In the “Reusable validation” by Gabriel, I can’t see the “reusable” part. Are there any other examples of this kind of reusable validation where the configuration is not right next to the assertion?

What am I missing? Many thanks.

1 Like
#4

@denizdogan Any validation requires an explicit assert. The reason is that an assertion can only typecheck when the two sides of the equivalence are actually equivalent. None of the sides may be abstract.

What you can do is to provide a reusable function that creates the equivalence:

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

-- the config type
let Config = { gzipLevel : Natural }

let Config/validate
      : Config -> Type
      = \(c : Config) -> Prelude.Natural.lessThanEqual c.gzipLevel 9 === True

You can then import this function and use it in an assertion:

let myConfig = ...

let _ = assert : Config/validate myConfig

in myConfig
#5

Thanks for responding!

Okay, so that makes sense, I guess I’m just surprised that the validation is ultimately left up to the end user. What made me dive into this in the first place was that I wanted to make a custom datatype which can only represent natural numbers 1 through 9. (This is for my dhall-nginx package which is still work in progress, where I want to make sure that users are not able to set the access log gzip level to anything else than 1-9, as that would be an invalid Nginx configuration value for that particular directive. https://github.com/denizdogan/dhall-nginx/blob/main/directives/ngx_http_log_module/access_log/type.dhall)

1 Like
#6

You could also put the assertion in the place where the user config is consumed.

Another idea would be to add a --validation option to tools like dhall-json through which users can supply a function that creates the equivalence. For dhall text, this doesn’t make much sense though.

#7

This can be made somewhat ergonomic by the fact that you can have the assertions in the type level and you can use placeholder proofs on the right hand side.

A working example:

let Prelude =
      https://prelude.dhall-lang.org/v20.2.0/package.dhall
        sha256:a6036bc38d883450598d1de7c98ead113196fe2db02e9733855668b18096f07b

let Gzip = { level : Natural }

let validate
    : Gzip -> Type
    = \(g : Gzip) -> Prelude.Natural.lessThanEqual g.level 9 === True

let useGzip
    : forall (g : Gzip) -> validate g -> Text
    = \(g : Gzip) ->
      \(_ : validate g) ->
        "foo"

let QED : True === True = assert : True === True

in  useGzip { level = 9 } QED
2 Likes