Gabriel439

This explains the disadvantages of using a general-purpose programming language as a configuration language:

https://github.com/dhall-lang/dhall-lang/wiki/Safety-guarant...

You can do more than just compare the output of two programs in Dhall. You can verify using a semantic integrity check that two programs are the same for all possible inputs. For example:

  $ dhall hash <<< 'λ(x : Natural) → x + 0'
  sha256:986613701cf8cc883c2490af81d5fdcfb0f33f840870acaac21689f57c1baab6

  $ dhall hash <<< 'λ(x : Natural) → x'
  sha256:986613701cf8cc883c2490af81d5fdcfb0f33f840870acaac21689f57c1baab6

  $ dhall hash <<< 'λ(y : Natural) → y'
  sha256:986613701cf8cc883c2490af81d5fdcfb0f33f840870acaac21689f57c1baab6

The cryptographic hash is smart enough that many behavior-preserving changes don't perturb the hash.

There are ASCII equivalents. You can type `\` instead of `λ` and `forall` instead of `∀`. Also `dhall format` will automatically translate ASCII to Unicode for you.

However, if you do want to type them then see:

https://en.wikipedia.org/wiki/Unicode_input

... and the relevant code points are:

* `λ`: `U+03BB`

* `∀`: `U+2200`

Dhall's lists are homogeneous lists, meaning that every element always has the same type of value. This is true whether or not you annotate list elements with a type or you annotate the list with a type.

You only need to annotate the type of an empty list. Lists with at least one element don't require a type annotation because the type can be inferred from the type of that element.

Dhall does not have buit-in support for homogeneous maps. Dhall does have statically typed heterogeneous records (i.e. something like `{ foo = Bool, bar = "ABC" }` which has type `{ foo : Bool, bar : Text }` for example).

If you want to store different type of values in the same list you wrap them in a union. For example, if you want to store both `Text` values and `Natural` numbers in a list you would do:

        let union = constructors < Left : Natural | Right : Text >

    in  [ union.Left 10, union.Right "ABC", union.Right "DEF", union.Left 4 ]

The closest thing to a homogeneous map in Dhall is an association list of type `[ { mapKey : Text, mapValue : a } ]` but even that is still not an exact fit since it doesn't guarantee uniqueness of keys. However, Dhall's JSON/YAML integration does convert that automatically to a JSON/YAML homogeneous map (i.e. a JSON record where every field has the same type).

In general, Dhall's JSON/YAML integration has several tricks and conventions that translate to weakly typed JSON idioms (such as homogeneous maps, omitting null values, and using tags).

> What if the host executing the script had access to some intranet site with sensitive data? Would I be able to do a network import of such a URL, load it as raw text, and provide that as a header to another import?

Yes, a local import would be able to access an intranet site and re-export that information via custom headers supplied to another import. This is allowed because it falls under trusting local imports. Local imports have access to environment variables and your local filesystem, too, which are equally sensitive, which is why they need to be trusted.

This rule is called the "referential transparency" check, which can be summed up as:

* Only environment variables, absolute paths, and home-anchored paths classify as "local" imports

* Only local imports can retrieve other local imports

* URLs can import relative paths, but they are relative to the URL, not relative to your local filesystem

The reason it's called the "referential transparency" check is because this security restriction also leads to the nice property that import system is referentially transparent. That means that every import evaluates to the same result no matter you import it from. For example, if you have a directory of Dhall expressions that refer to each other and you rehost them on a file server the language guarantees that they still behave the same whether you import them locally or you import them via their hosted URLs.

Also, thanks! :)

Author here: You might be interested in this post on safety guarantees:

https://github.com/dhall-lang/dhall-lang/wiki/Safety-guarant...

The main risks in executing potentially malicious Dhall code that is not protected by a semantic integrity check are:

* Using more computer resources than you expected (i.e. network/CPU/RAM)

* Unintentional DDos (as you mentioned)

* The malicious import returning a value which changes the behavior of your program

If you protect the import with a semantic integrity check then the malicious import can no longer return an unexpected value, which eliminates the third issue (changing program behavior). Also, upcoming versions will cache imports based on the semantic integrity check, which would mitigate the second issue (DDos) for all but the first time you interpret the program. There is also a `dhall freeze` subcommand which takes a program and automatically pins imports to their most recent value using semantic integrity check.

Regarding exfiltration, the import system guarantees that only local imports can access sensitive information such as file contents or environment variables. See:

https://github.com/dhall-lang/dhall-lang/wiki/Safety-guarant...

The only way that a remote import can obtain that information is if a local import supplied that information via Dhall's support for custom headers. In fact, this is actually an intended use of that feature (i.e. a local import fetching a Dhall expression from a private GitHub repository using an access token retrieved from an environment variable).

So in other words the threat model is that as long as you can trust local imports then you can transitively trust remote imports because they cannot access your local filesystem or environment variables unless you explicitly opt into that via a local import. I think that's a reasonable threat model because if can't trust the contents of your local filesystem then you can't even trust the Dhall interpreter that you are using :)

Imports are not computed and the set of imports that you retrieve is static (i.e. does not change in response to program state or input), so the set of imports or their paths cannot be used as an exfiltration vector.

Author here: I opened an issue to track this request and remind myself to do this: https://github.com/dhall-lang/dhall-lang/issues/189

The way I would phrase it is that you've concentrated your input and output sanitisation in a trusted kernel (i.e. the compiler/interpreter) and that puts an upper bound on the amount of code that you need to audit (just the compiler/interpreter code base). That's more realistic than auditing all programs written within the compiled/interpreted language

Yes, but it's a restricted set of input and output: the only thing you can do is import other code. You can't, say, launch missiles or delete files unless the compiler/interpreter allows it

However, the compiler/interpreter places an upper bound on the amount of code that we need to audit because it acts like a trusted kernel. We only need to audit the compiler/interpreter itself for safety and once we do so we can automatically trust all programs written in the language that it compiles/interprets

Yes, that's a good analogy

However, I think the more important thing I'm trying to fix is how we compose code. The Rube-Goldberg machine the post refers to is the complicated mechanisms we have to deal with for combining code fragments. Reading in a value shouldn't be any different from reading in code and shouldn't require any more overhead than just copy-and-pasting a URL into your program

There are two separate questions here:

* "Why should we limit I/O to the compiler"?

Think of the compiler or interpreter as a small trusted kernel. It's a mostly fixed code base that you can inspect and audit. The programs that it compiles or interpret on another hand don't have to be trusted because they are perfectly sandboxed. They are effect-free purely functional code

* "Why not use multi-threading for communication?"

This is (in my eyes) the real problem that I'm trying to solve. Using effects as a message bus for composing code seems incredibly awkward and primitive, like explicitly managing stack registers.

To clarify: the idea is that both the view and controller are built into the interpreter. The interpreted program builds the model and is written in a a purely functional and effect-free language

Right, and where I'm going with this is that we should take the JavaScript model to its natural conclusion and use it more pervasively in other domains. In other words, more applications and domains should be configured via sandboxed and interpreted programs that can easily reference other programs

However, the difference is that I don't think we should use an untyped and Turing-complete language for doing this (which is my primary objection to JavaScript). Also, I think the mechanism for referring to other programs should be more lightweight (i.e. just dump the path and URL into your code and you're done)

Yes, this entails moving more logic into compilers/interpreters. For example, Dhall is actually designed this way: not only is it a command line interpreter but it's also a Haskell library that you can use to interpret Dhall expressions and marshal them into Haskell programs. So the Haskell language combined with the Dhall library becomes an "interpreter builder": a way to crank out a large number of specialized applications that are customized via an effect-free programmable configuration language

For the specific example of a server, there would be two layers:

* in Haskell you would implement a server configured by a Dhall expression (i.e. a hybrid server/interpreter)

* end users program in Dhall, not Haskell

* end users provide a record of pure functions (one for each API endpoint) that translate user input to output

However, I think that's still just a superficial answer to the question. The next level is to ask: why do we even need a server? A server is just a way to distribute values, but Dhall already has a way to distribute values (and code): we just import them by reference. So why not just use that directly instead of standing up a server to reimplement what the Dhall interpreter already does internally

You can encode markup in a purely functional languages. That's actually the easy part since you can treat it as an ordinary data structure. Actually, the harder part is coming up with a user-friendly way to transform a stream of events into a stream of outputs within a purely functional language. In my opinion, there is no clear consensus on the "right" way to do this, but the field of functional reactive programming is based on searching for clean solutions to this problem

However, again, you need to step back and ask: what did we need this GUI for? In some cases, the GUI is the requirement (like in a game) so there's not much you can do to simplify things. However, in other cases -the GUI is just a poor man's interface to composing values and code, in which case we might just be able to replace it with importing URLs and paths using Dhall's built-in mechanisms (and perhaps replace all these bespoke GUIs with a general purpose GUI for manipulating Dhall expressions)

To make an analogy to Python: you don't need to recompile Python to interpret new Python programs. Chrome would be like Python: Chrome is itself a compiled program, but it interprets user settings and web pages.

Chrome is allowed to do whatever I/O it wants, but the programs it interprets (like user settings and web pages) are not allowed to do any I/O at all. These interpreted programs are sandboxed.

This isn't really surprising if you think about it. Chrome is already an interpreter for a sandboxed language (JavaScript)

Your program can be a pure function which somebody else can invoke, so it's not necessarily a constant

However, Dhall does have the ability to normalize under lambda when possible so it will actually do this for you if it can! For example, if you try to interpret this program, which is a function:

        let replicate = https://ipfs.io/ipfs/QmQ8w5PLcsNz56dMvRtq54vbuPe9cNnCCUXAQp6xLc6Ccx/Prelude/List/replicate
    
    in  let exclaim = λ(t : Text) → t ++ "!"

    in  λ(x : Text) → replicate +3 Text (exclaim x)

The interpreter will simplify that down to:

    λ(x : Text) → [x ++ "!", x ++ "!", x ++ "!"] : List Text

... although it can't do anything else until somebody else comes along later and calls the function on a specific input

The primary distinction from a dynamic language is that Dhall is typed, total, and does not permit arbitrary effects (only importing other code is allowed), so it's safe to evaluate arbitrary remote code and it's also safe to use Dhall expressions to configure programs since they consist of nothing but pure functional logic. Dhall is first and foremost a programmable configuration language so safety is one of the primary language requirements

A closer analogy to Dhall would be if web pages were assembled entirely from JavaScript instead of HTML, URLs were just pointers to Javascript expressions, and JavaScript code could refer to other JavaScript code anywhere within the syntax tree just by URL (instead of out-of-band via a <script> directive)

In Dhall's case it is a typed interpreter. So every time you interpret an expression there are three phases:

* Resolve all imports (transitively, if necessary)

* Type-check the code

* Normalize the code (a.k.a. evaluation, but it can normalize functions, too)

It's a little more complex than that (for example, imported code is itself type-checked before substitution into the syntax tree), but that's the basic idea

It's closer in spirit to a Bash script sourcing another bash script (i.e. using "source"). However, the difference from Bash is that:

* In Bash the unit of code composition is statements (as opposed to expressions in Dhall) * When you source another script you can only do so at the top-level of the program, as a statement (as opposed to Dhall where you can import other expressions anywhere within the syntax tree)

I'm less familiar with PHP so perhaps somebody who knows it better can explain how Dhall relates to the PHP model

Inputs in a purely functional world are limited to things that you can serialize and deserialize, which does not include functions or types. If you ingest values via imports instead of via traditional I/O then you can transmit any language feature

You're right that I didn't get to output at all. That's my mistake since I wrote the post in a hurry. The idea is that the interpreter of this language is not a general purpose compiler but is a specialized application with a built-in output. For example, one such interpreter might be a browser that just displays the result to the user.

Using Chrome as an example, the Chrome executable would be an interpreter. Chrome itself would be compiled. For simplicity I'll assume that we browse static HTML pages. Your URL bar would be replaced with a code bar that accepts any arbitrary Dhall expression that builds a DOM. However, since Dhall accepts URLs in place of expressions it is still a URL bar (as long as the URL you input refers to an expression that assembles a DOM). The browser would then interpret that expression to build the DOM and render it as a web page

There are several ways you could configure preferences but I'll throw out a simple idea just to convey the point. Chrome itself could be configured via a Dhall expression that assembles a giant record of user settings. Since a Dhall expression can also be a file you can configure user settings via a path to a file (as long as that file you refer to contains an expression for building that record). That file could itself contain references to other files in order to delegate the configuration of certain options.

That's not the only way you could do it, though. Web pages could be pure functions of user settings, too. CSS would just becomes a special case of treating a DOM as a pure function of style settings.

UI or network input is trickier, not because it's hard to model UI or network input in a purely functional setting but rather because you want to do it in a different way on a case-by-case basis. For example, some types of UIs are unchangeable requirements that you have to adapt to (like a game: the UI is the requirement). However, other forms of UIs or network input are just work-arounds for inability to compose code effectively. For example, batch network input can be replaced by just importing URLs as code. Similarly, batch user input can be replaced by just importing files as code.

I don't want to think about I/O. That's the point

I want to focus on connecting pure code together without thinking about the details of how that happens. I want this for the same reason that I don't want to think about manually allocating registers, managing memory, or caring about evaluation order

Also, like I mentioned, traditional I/O can't import functions or types, so this is strictly more powerful

Author here: this is written for a primarily functional audience who already take for granted that it's good to minimize effects, but let me try to rephrase it another way for people who don't have that background

Typically there are two ways that our programs can ingest values:

* statically, via imports

* dynamically, via reading values

Why not ingest all values via imported code? If the import system is sufficiently lightweight this is simpler and easier than reading values the traditional way, plus you can read in things that are not plain values (like functions and types)

In that sense, reading/downloading text and parsing it becomes an implementation detail of the compiler and from the programmer's point of view what you're left with is a network of pure functions that can refer to each other across impure boundaries

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).

For the purposes of evaluation, it's still an improvement to have a total language. As I mentioned in another thread, using a totality checker is like wearing seatbelts: it doesn't protect against everything, but it's still a huge improvement.

The latter example you gave will still not type-check in Dhall, although I'll still answer the spirit of your question

You can write expressions in Dhall that will take a long time to evaluate (see the Ackerman example elsewhere in this thread), but it's harder to do so by accident. Totality checking is worthwhile for the same reason that seatbelts are worthwhile: they don't protect against all accidents, but they do protect against a lot of them

Yes, however standardizing the language is higher priority at the moment

System Fw cannot type-check self application

The type system is what prevents System Fw from being Turing complete. Specifically, the key bit is that you cannot unify the type "a -> b" with "a" (which is what prevents self application)

The key word in "automatic simplification" is "automatic". The feature loses value if a human has to intervene to specify which functions to inline or to continue inlining. Imagine how worthless `go fmt` would be if it prompted the user to confirm every change to the source code

In a Turing complete language you can't safely inline all functions to completion without risking an infinite loop. In such a language there is no decidable way to know when to stop inlining things