Dhall

Dhall is a programmable configuration language designed to add the features missing from JSON and YAML — types, functions, imports, and abstraction — while deliberately stopping short of Turing-completeness. Every Dhall program is guaranteed to terminate, produces a single normalized value, and can be converted to JSON, YAML, TOML, XML, or other formats. Its slogan, coined by creator Gabriel Gonzalez, is that Dhall is “a programmable configuration language that is not a general-purpose programming language.”

History and Origins

Dhall was created by Gabriel Gonzalez (now publishing as Gabriella Gonzalez), a prolific Haskell library author best known for projects like pipes, turtle, and the earlier experimental language Morte. Morte, announced in 2014, was an intermediate calculus-of-constructions compiler explored as a vehicle for super-optimized functional code. Dhall took Morte’s core idea — a typed lambda calculus guaranteed to terminate — and refocused it on a practical problem: configuration.

The language was introduced publicly on December 5, 2016 through Gonzalez’s Haskell for all blog post, “Dhall — A non-Turing-complete configuration language.” The reference implementation in Haskell followed and matured through 2017 as early adopters — particularly within the Haskell and Nix communities — began using Dhall as a typed alternative to YAML.

Dhall’s design reflects Gonzalez’s long-standing interests in total functional programming and software correctness. Rather than treating configuration as a simple serialization format to be templated, Dhall treats it as a first-class programming concern, one worth solving with a typed language with strong safety guarantees.

Design Philosophy

Dhall’s design is organized around a small set of strong commitments:

• Programmable, but not a general-purpose language — Dhall exposes functions, conditionals, and imports, but omits general recursion and unbounded computation. This is a deliberate ceiling, not a limitation waiting to be removed.
• Total functional programming — every well-typed Dhall expression reduces to a normal form in bounded time. There are no infinite loops, no runtime exceptions, no divergent evaluation.
• Safety as a feature — because Dhall is total and its imports are content-addressable via optional SHA-256 hashes, remote configuration can be imported without the usual supply-chain risks that plague templating ecosystems.
• Distribution over inheritance — rather than an OOP-style class hierarchy, Dhall composes configuration through records, unions, and first-class functions.

The non-Turing-completeness property is the most frequently misunderstood part of Dhall. It does not mean the language is weak; rather, it means Dhall intentionally rejects features (arbitrary recursion, general fixed-point operators) whose presence would eliminate the termination guarantee. Everything that can be expressed in Dhall is guaranteed to terminate — which in turn means tools can evaluate untrusted Dhall safely.

Theoretical Foundations

Dhall’s type system is built on System Fω, the higher-order polymorphic lambda calculus. This places Dhall in a well-understood region of type theory, alongside languages like Haskell (whose core is an extension of System Fω). The preceding Morte language was based on the calculus of constructions — a strictly more powerful formalism — and Dhall represents Gonzalez’s refinement of that approach into a practical tool for configuration engineering.

The benefits of this formal grounding are concrete:

• Decidable type checking — every Dhall expression can be type-checked without the checker itself diverging
• Strong normalization — every well-typed expression reduces to a unique normal form
• Principal types — type inference produces a most-general type for every expression

Key Features

Non-Turing-Complete Totality

Dhall has no general recursion and no way to construct a looping program. The absence of these features is an enabling constraint: evaluators, type checkers, and IDE tooling can all operate on Dhall without worrying about runaway computation. A malicious Dhall file cannot hang your build by design.

Strong Static Typing with Inference

Dhall is statically typed with Hindley–Milner-style inference. Types are first-class values in the language (a Type has type Kind, which has type Sort), enabling polymorphic functions and generic records without complex syntax.

let Point = { x : Natural, y : Natural }
let origin : Point = { x = 0, y = 0 }
in  origin

Imports, Including from URLs

Dhall expressions can import other Dhall files, environment variables, or even remote HTTPS URLs. Each import can be pinned to a semantic integrity hash (a SHA-256 of its normal form), which guarantees that the imported value has not changed regardless of the transport:

let types = https://prelude.dhall-lang.org/package.dhall
              sha256:<hash>
in  types.List.map

Because imports are hashed by semantic content (normal form), cosmetic changes to a remote file — whitespace, variable renaming, let-binding reordering — do not invalidate the hash. Only a change in meaning does.

Standard Prelude

Dhall ships a versioned standard library, the Prelude, hosted at prelude.dhall-lang.org and also available as a Git repository. The Prelude provides commonly needed functions for lists, optionals, natural numbers, text manipulation, JSON generation, and more.

Conversion Tooling

A family of companion tools converts Dhall output to downstream formats:

This lets Dhall serve as a typed authoring layer for any system that already consumes these formats — Kubernetes, Terraform via JSON, Ansible via YAML, and so on.

Implementations

Dhall has a clear reference implementation plus a growing set of independent ports:

• dhall-haskell — the reference implementation in Haskell (BSD-3-Clause licensed), hosted at github.com/dhall-lang/dhall-haskell
• dhall-rust / serde_dhall — a Rust implementation usable as both a standalone tool and a serde-compatible library
• dhall-purescript — a PureScript port that has reportedly achieved full compliance with the shared acceptance test suite at various points in its history
• dhall-clj — a Clojure implementation
• dhall-ruby — a Ruby implementation
• dhall-golang — a Go implementation

The existence of multiple independent implementations is possible because Dhall’s language standard is maintained separately from any single codebase at github.com/dhall-lang/dhall-lang, complete with an executable acceptance test suite that implementations run against.

Language Standard and Versioning

Unlike many small languages, Dhall publishes a formal language standard with its own version numbers, distinct from the versions of its implementations. The standard follows a scheme similar to SemVer: major version bumps indicate backwards-incompatible changes to the language, minor bumps indicate new features added compatibly, and patch bumps indicate editorial changes with no semantic effect.

Recent standard versions include:

• v21.0.0 (August 2021) — first-class dates and times
• v22.0.0 (January 2023) — the showConstructor keyword
• v23.0.0 (April 2023) — a native Bytes type
• v23.1.0 (January 2024) — binary integer literals

Current Relevance

As of early 2026, Dhall is actively maintained but past its peak velocity. The reference implementation continues to receive regular releases — dhall-haskell 1.42.3 shipped in September 2025 — and the language standard last advanced to v23.1.0 in January 2024. Development pace is noticeably slower than the 2018–2020 period that produced most of the language’s feature set.

The community has settled into a steady state: the language is stable, the Prelude is mature, and the ecosystem of conversion tools covers the common targets. For users with existing Dhall configurations — especially in Haskell, Nix, and Kubernetes contexts — the language remains a reliable and well-documented choice.

Dhall’s primary competition in the typed-configuration space comes from CUE (constraint-based, from Google’s GCL lineage), Jsonnet (data-templating, also GCL-derived), and KCL (a newer CNCF entrant). Each tool makes different tradeoffs; Dhall’s distinguishing bets are totality, semantic import hashing, and a small principled type system rooted in System Fω.

Why It Matters

Dhall is an unusual artifact in the programming language landscape: a tool built on serious type theory that is self-consciously not trying to be a general-purpose programming language. By accepting limits — no recursion, no I/O, no side effects — Dhall earns properties that general-purpose languages cannot offer: guaranteed termination, safe imports of untrusted code, reproducible evaluation, and a specification small enough that multiple independent implementations can agree on semantics.

Whether or not Dhall achieves broad mainstream adoption, its design is a pointed argument: that configuration deserves the rigor of a real language, and that the right language for configuration is one that deliberately refuses some of the power of a general-purpose one.