Dhall does the dumbest thing possible to enforce totality: Dhall doesn't support recursion! Note that Dhall does support lists and folds on lists (which are to

Dhall does the dumbest thing possible to enforce totality: Dhall doesn't support recursion! Note that Dhall does support lists and folds on lists (which are total), but not user-defined recursion For example, if you write: let x = x in x ... then the second `x` will be flagged as an unbound variable because `let`-bound variables are not in scope for their own definitions. Similarly, there is no `let rec` in Dhall That implies that if you want a user-defined recursive type that was not a list then you have to explicitly Boehm-Berarducci-encode the recursive type and its inhabitants. For example, if you wanted to encode the following Haskell data type in your configuration: data Tree = Node Integer | Branch Tree Tree example :: Tree example = Branch (Node 1) (Branch (Node 2) (Node 3)) ... you would encode it like this: λ(Tree : Type) → λ(Branch : Tree → Tree → Tree) → λ(Node : Integer → Tree) → Branch (Node 1) (Branch (Node 2) (Node 3)) You can think of Boehm-Berarducci encoding as "anonymous recursion" when you write it this way because every inhabitant of such a "recursive" type includes the datatype definition in the value (if you view the lambda-bound type and constructors as the datatype definition) Or to put it another way, if you ignore Dhall's support for builtin types, builtin functions, and imports then Dhall is literally the exact same thing as System Fw . You're used to thinking of System Fw or the calculus of constructions as underlying core languages for a higher-level language semantically defined in terms of the core language like Coq, Agda or Haskell. However, in Dhall there is no underlying core language: you are assembling raw System Fw expressions. Since the most pedantic definition of System Fw requires explicit polymorphism and doesn't support recursion then Dhall behaves the same way, too. I agree, though, that the lack of (unsafe) IO is an even bigger deal. Like you mentioned, if you use immutable URLS (such as IPFS) then they are basically pure. Even if you do use mutable URLs, you can always use the ability to normalize programs to purify them of imports (and you can also use Dhall's API to safely and statically verify that an expression is devoid of imports).