Input validation

#1

How can I check user input with dhall ?

For instance the following assertion:

-- ../schemas/Quota.dhall
{ Type = { cpu : Natural }, default.cpu = 1 }

let lessThanEqual = (../../Prelude.dhall).Natural.lessThanEqual

let quota =
      λ(config : (../schemas/Quota.dhall).Type) →
        let check = assert : lessThanEqual 5 config.cpu ≡ True in config::{}

in  quota

will always reply:

→ dhall --explain <<< ‘./openshift/func/makeQuota.dhall {cpu=5}’
Error: Assertion failed

  • … …
  • True

7│ assert : lessThanEqual 5 config.cpu ≡ True

#2

Assertions are checked at type-checking time, so both sides of the equivalence need to be known then. You could achieve that by importing some user-defined expression.

#3

@sjakobi thanks. Seems obvious. I have just realized I need to do the check at the caller side where I receive the input.