Programatic configuration with Dhall

Emery Hemingway ehmry at posteo.net
Wed Sep 4 10:59:12 CEST 2019


Hello Genodians,

As a side project I've been experimenting with using the Dhall
configuration language (https://dhall-lang.org/) for generating and
composing Genode XML. Dhall is a purely functional, non-Turing complete
language designed for expressing and transforming configuration. The
standard prelude, something like a pure standard library, supports
transformation of Dhall expressions to XML (as of v9.0.0) which allow
Genode configuration to be expressed and rendered using the pure Dhall.
I would not advocate parsing Dhall directly within Genode components,
rendering to XML files is certainly fine for now.

A non-trivial analogy would the "noux-system" package expressed as Dhall:
https://git.sr.ht/~ehmry/genode-ehmry/tree/master/runtimes/noux-system/pkg.dhall

Using this language has its advantages and its drawbacks. The advantages
being checks against malformed configuration using a strict type system,
the ability to deduplicate and normalize similiar configurations, and
the ability to automatically generate configuration parameters such as
resource quotas and routing rules using induction rather than hand-
tweaking.

The disadvantages being a new language to learn (though faster than the
training to write flawless XML), an esoteric appearance, and a lack of
recursive types (nested XML is possible, but expressed as partially
applied nested functions, which are basically opaque).

If its something you interested in, I would recommend playing with the
language a bit, and then working from the largest to narrowest scope
when writing configurations, because nested configuration may always
be expressed as a string of XML.

The Genode Dhall Prelude can be found here:
https://git.sr.ht/~ehmry/dhall-genode

Cheers,
Emery



More information about the users mailing list