Host datatype specifications in Dhall

Hi there,

We’re scoping out the idea of leveraging Dhall to host ‘data type specifications’. If you’re familiar with schema systems such as Google Protobufs, JSON Schemas, CDDL or anything of this sort, that’s what we’re trying to build.

More precisely, imagine taking out Haskell ADTs and putting them in a configuration file, such that a dedicated complier+codegen pipeline can create type libraries for a variety of target languages.

We want to leverage an existing configuration language environment, and Dhall seems like a great fit. Not only does one get functions to manage reuse, automation and tooling that comes with Dhall (lsp, formatters) but also a fabulous way to distribute and share Dhall based configurations and specs.

Which brings me to my question…

We’re not entirely sure if having an eDSL hosted in Dhall (like dhall-kubernetes and friends) to represent our ADTs (with additional features like annotations, constraints, opaque types etc.) is appropriate. For example, in such and eDSL one would write something like the following in Dhall for the Set and Maybe types:

let defs = [
  opaque "Set" ["a"],
  data "Maybe" [ "a" ] (toMap { Nothing = nullary, Just = var "a" })
]

let instances = [
  isJson [isJson "a"] "Maybe" ["a"]
]

Alternatively, we’re considering using Dhall natively and thinkering with the idea of using the builtin Dhall type semantics and working directly with that. Concretely, a Dhall record maps to whatever a native ‘record’ is in the target language, the same for Dhall sum types and other relevant builtins. Seems like this approach gives us existing mappings and codegen that Dhall supports for popular languages. Not to mention you don’t have the annoying verbosity that comes with eDSLs. However, my concern is that ‘data type language’ features are then very much bounded to Dhall type features.

I hope this makes sense and thank you for your time.

Cheers,
Drazen

1 Like

Yeah, so my intuition here is that you want something like Dhall, but not exactly Dhall.

Specifically, I think the latter approach you mentioned of using the native Dhall types directly is much closer to the right way of doing this. However, as you noted, the Dhall types might not support all of the IDL features that you want to model, which is why I say that you want something that is most likely some variation on Dhall.

1 Like

Thanks a lot this is very helpful and sorry for such a delayed response.

We experimented with Dhall a bit and ran into some inconvenience with defining recursive data types. Eventually our TypeTerm became recursive, and to encode that in Dhall we resorted to something like a Scott encoding.
We essentially wanted to output a well structured JSON/YAML from a Dhall config and input that into our compiler, but this encoding now yields Dhall functions which can’t be represented in JSON/YAML and alike. I wonder if we’re missing something…

Note that there is one special recursive type that dhall-to-json does support, which is Prelude.JSON.Type. If you convert your internal recursive type to that type then dhall-to-json can render it as JSON