Some reasoning behind https://cohost.org/Profpatsch/post/369824-dhall-to-javascript and why I think dhall-to-nix is such an awesome tool.
In one word: Free foreign function interface (FFI).
When you want to integrate two languages, you usually have to go via some data exchange format, which in most cases boils down to the C calling convention.
But this is highly restrictive, given that you cannot really pass functions around (unless you find a horrifyingly specific way to encode them).
When you have a language like dhall/purescript, a fundamental insight is that they are subsets of other languages. For dhall this is essentially any untyped lambda calculus (like nix or javascript), for purescript this can be javascript, Erlang or lots of other languages.
Note that in theory, any turing-complete (TC) language can be transpiled to any other TC language (and every non-TC language can be transpiled to any TC language), but in practice such pesky nuances as ›performance‹ play a big role.
Now, in the case of dhall, it is quite literally a typed lambda calculus with some data structures baked in, namely lists, attrsets and sum types. Transpiling them to nix/javascript is as simple as
- erasing all the types and
- figuring out a good representation for sum types
When you look at dhall-to-nix, all you have is a ~500 line function that does all this work in a big recursive pattern-match on the source expression. That’s all there is to it.
This gives you a very powerful FFI
In particular, you can now pass higher-order functions freely between both source and target language, since in the end they are going to be run entirely within the target language.
For example, if I wanted to write a dhall configuration for how files are opened on my system, I could pass it a function which looks up a package from the nixpkgs package collection:
\(getPkg : Text -> Text) ->
{
packages = [
getPkg "hello",
getPkg "coreutils"
] : List Text
}
Or even better, I could “import” an opaque type, so that I cannot confuse packages with other strings on the dhall side:
\(Package : Type) ->
\(getPkg : Text -> Package) ->
{
packages = [
getPkg "hello",
getPkg "coreutils"
] : List Package
}
On the nix side, types are erased, so I would write something like this:
{ nixpkgs }:
let
getPkg = pkgName: nixpkgs.${pkgName};
in
(importDhall ./config.dhall)
{}
getPkg
And it would return me a list like
[
"/nix/store/…-hello"
"/nix/store/…-coreutils"
]
Note that the dhall types are erased, which means I can pass anything I want to the first argument of the function, it will be ignored (here I used {}).
we need to go higher
So we already passed around a function, which is very hard to do with “normal” FFI already, but let’s go crazy here.
We can pass around higher-ranked functions as well, that is functions which take other functions as arguments.
For example, a nix package can have multiple outputs, but you cannot know the outputs when you write the config on the dhall side. So let’s say we want the getPkg function to “report back” to the dhall side which outputs are available, and the dhall side can then decide whether it wants to return the bin, lib, dev or man output.
The dhall file would define an interface like:
let Output = < Bin | Lib | Dev | Man > in
\(Package : Type) ->
\(outputInList : Output -> List Output -> Bool) ->
\(firstOutput : List Output -> Output) ->
\(getPkg : Text -> (List Output -> Output) -> Package) ->
let chooseDevOrFirst = \(existingOutputs : [Output]) ->
if outputInList Output.Dev existingOutputs
then Output.Dev
else firstOutput existingOutputs
in
{
packages = [
getPkg "hello" chooseDevOrFirst,
getPkg "coreutils" chooseDevOrFirst
] : List Package
}
And if coreutils has a dev output and hello only has bin, you get:
[
"/nix/store/…-hello-bin"
"/nix/store/…-coreutils-dev"
]
So what happens here is that the dhall side tells the nix side: “look, I need this package”. Then the nix side calls back and says “I’ve got these outputs, please choose one”. And dhall returns a function that makes the choice.
You can continue this game to any arbitrary depth.
even more fun
I wrote earlier that dhall is not turing complete. That means any dhall evaluation eventually finishes (though maybe you are not there to see it anymore ;) ).
fix : (a -> a) -> a is a typical function that you can only write in a TC language, so it’s impossible to write it in pure dhall.
However, the type of fix can be written down in dhall no problem. You might realize where this is going.
dhall:
\(fix : forall (a : Type) -> (a -> a) -> a) ->
let t = { x : Natural, y: Natural } in
fix t (\(old : t) -> { x = old.y + 19, y = 23 })
nix:
let fix = _: f: let x = f x; in x;
in (importDhall ./fix.dhall) {} fix
output:
{ x = 42; y = 23; }
I think that’s a good point to stop this chost :)
disclaimer: I have not syntax-checked any of the examples except for the fix one, so there might be some typos here or there