Dhall.Nix

This library only exports a single dhallToNix function for translating a Dhall syntax tree to a Nix syntax tree for the hnix library

See the dhall package if you would like to transform Dhall source code into a Dhall syntax tree. Similarly, see the hnix package if you would like to translate a Nix syntax tree into Nix source code.

This package also provides a dhall-to-nix executable which you can use to compile Dhall source code directly to Nix source code for your convenience.

Any Dhall expression can be converted into an equivalent Nix expression. For example, Dhall records can be converted into Nix records:

$ dhall-to-nix <<< "{ foo = 1, bar = True }"
{ bar = true; foo = 1; }

... and you can also convert Dhall functions to Nix functions, too:

$ dhall-to-nix <<< "λ(x : Bool) → x == False"
x: x == false

Many Dhall expressions have a straightforward translation to Nix expressions but there are some translations that are not as obvious. The following section documents these trickier conversions:

First, all Dhall types translate to an empty record:

$ dhall-to-nix <<< "Integer"
{}

Polymorphic Dhall functions translate to Nix functions that ignore their type argument:

$ dhall-to-nix <<< "List/head"
t: xs: if xs == []
      then null
      else builtins.head xs

Optional values translate to null if missing or the unwrapped value if present:

$ dhall-to-nix <<< "None Natural"
null

$ dhall-to-nix <<< "Some 1"
1

Unions are Church-encoded:

$ dhall-to-nix <<< "< Left : Bool | Right : Natural >.Left True"
{ Left, Right }: Left true

Also, all Dhall expressions are normalized before translation to Nix:

$ dhall-to-nix <<< "True == False"
false

You can use the dhall-to-nix executable within Nix to assemble Nix expressions from Dhall expressions using the following dhallToNix utility function:

dhallToNix = code :
  let
    file = builtins.toFile "dhall-expr" code;

    drv = pkgs.stdenv.mkDerivation {
      name = "dhall-expr-as-nix";

      buildCommand = ''
        dhall-to-nix <<< "${file}" > $out
      '';

      buildInputs = [ pkgs.haskellPackages.dhall-nix ];
    };
  in
    import "${drv}";

Dhall to Nix

dhallToNix :: Expr s Void -> Either CompileError (Fix NExprF)

Convert a Dhall expression to the equivalent Nix expression

>>> :set -XOverloadedStrings
>>> dhallToNix (Lam "x" Natural (Lam "y" Natural (NaturalPlus "x" "y")))
Right (NAbs (Param "x") (NAbs (Param "y") (NBinary NPlus (NSym "x") (NSym "y"))))
>>> fmap Nix.Pretty.prettyNix it
Right x: y: x + y

Precondition: You must first type-check the Dhall expression before passing the expression to dhallToNix

Exceptions

data CompileError

This is the exception type for all possible errors that might arise when translating the Dhall syntax tree to the Nix syntax tree

Constructors

CannotReferenceShadowedVariable Var

Nix does not provide a way to reference a shadowed variable

CannotProjectByType

We currently do not support threading around type information

Instances

Show CompileError

Defined in Dhall.Nix

Methods

showsPrec :: Int -> CompileError -> ShowS

show :: CompileError -> String

showList :: [CompileError] -> ShowS

Exception CompileError

Defined in Dhall.Nix

Methods

toException :: CompileError -> SomeException

fromException :: SomeException -> Maybe CompileError

displayException :: CompileError -> String