Skip to content
master
Go to file
Code

Latest commit

* Implement `with` directly rather than via desugaring

I found it confusing to implement the recent `with`
optimizations (#1052) because `with` expressions are currently neither
pure sugar nor first-class expressions.

Also, there is arguably still scope for pathological behaviour, since
an abstract function like

    \(r : {a : {b : {c : Natural}} }) -> r with a.b.x = 1 with a.b.y = 2

will be evaluated to a function which potentially evaluates `r` 6
times (in an implementation which does not evaluate arguments before
passing them to a function).

This commit defines type inference and beta-normalization for `with`
expressions directly, rather than via a desugaring step.  As a
side-effect, desugaring of abstract `with` expressions no longer
happens; they are left as plain `with` expressions.  This is a
breaking change.

There is another consideration, which is there are currently a number
of simplifications for right-biased record merge expressions which the
current `with`-desugaring can piggyback on.  For example, currently:

    (e with k = v).k

evaluates to `v`, because of the simplification of expressions of the
form `(l // { k = v, rs... }).k`.  This commit does not attempt to
preserve those simplifications, but we could introduce some
`with`-simplifications in later commits if desired.

* small tweaks

* oops, remove duplicate alpha-normalization rule

* Update standard/beta-normalization.md

Co-authored-by: Gabriel Gonzalez <Gabriel439@gmail.com>

* Update standard/type-inference.md

Co-authored-by: Gabriel Gonzalez <Gabriel439@gmail.com>

* fix type inference rule

as caught by @Nadrieril

* better mnemonic variable names

as caught by @Gabriel439

* Allow creation of intermediate records

also tidy up the judgments a bit, add tests for the new judgments,
remove tests for the old desugaring behaviour.

* Update standard/type-inference.md

Co-authored-by: Gabriel Gonzalez <Gabriel439@gmail.com>

* Update standard/type-inference.md

Co-authored-by: Gabriel Gonzalez <Gabriel439@gmail.com>

* Add a test for partially-abstract `with` expressions

This caught a bug in dhall-golang.

Co-authored-by: Gabriel Gonzalez <Gabriel439@gmail.com>
e663cb3

Git stats

Files

Permalink
Failed to load latest commit information.
Type
Name
Latest commit message
Commit time
 
 
 
 
 
 
img
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 

README.md

Dhall Logo

Dhall is a programmable configuration language optimized for maintainability.

You can think of Dhall as: JSON + functions + types + imports

Note that while Dhall is programmable, Dhall is not Turing-complete. Many of Dhall's features take advantage of this restriction to provide stronger safety guarantees and more powerful tooling.

You can try the language live in your browser by visiting the official website:

Getting started

The easiest way to get started experimenting with Dhall is to install the dhall-to-json and/or dhall-to-yaml executables, which enable you to generate JSON and YAML, respectively, on the command line. Platform- and runtime-specific installation instructions can be found in the Dhall wiki.

For other ways to integrate Dhall in your project, read:

Tutorials

For a short introduction, read:

To learn more about core language features, read:

For an even longer hands-on tutorial, read:

... and for an even longer tutorial, read:

Finally, we have a cheatsheet for a very condensed overview and quick lookup:

What is this repository?

The Dhall configuration language has multiple implementations so that Dhall configuration files can be understood natively by several programming languages. You can find the latest list of the language bindings and their respective repositories here:

This repository contains language-independent functionality, such as:

  • The grammar and formal semantics

    Dhall is a formally-specified language standard, and language bindings follow the specification in order to ensure portability of Dhall configuration files across language bindings.

  • The standard test suite

    This repository contains a test suite that language bindings can use to check compliance against the standard.

  • The Prelude

    One Dhall package named the Prelude is versioned with and distributed alongside the language standard. This package contains general-purpose utilities.

  • Shared infrastructure for the Dhall ecosystem

    Several services support Dhall developers and this repository contains a NixOps specification of that infrastructure that automatically deploys changes merged to that configuration.

Development status

The current version and versioning policy is detailed in the Versioning document, and you can see the latest changes in the Changelog.

The Dhall configuration language slowly evolves in response to user feedback and if you would like to participate in the language evolution process then you should read:

Design philosophy

Programming languages are all about design tradeoffs and the Dhall language uses the following guiding principles (in order of descending priority) that help navigate those tradeoffs:

  • Polish

    The language should delight users. Error messages should be fantastic, execution should be snappy, documentation should be excellent, and everything should "just work".

  • Simplicity

    When in doubt, cut it out. Every configuration language needs bindings to multiple programming languages, and the more complex the configuration language the more difficult to create new bindings. Let the host language that you bind to compensate for any missing features from Dhall.

  • Beginner-friendliness

    Dhall needs to be a language that anybody can learn in a day and debug with little to no assistance from others. Otherwise people can't recommend Dhall to their team with confidence.

  • Robustness

    A configuration language needs to be rock solid. The last thing a person wants to debug is their configuration file. The language should never hang or crash. Ever.

  • Consistency

    There should only be one way to do something. Users should be able to instantly discern whether or not something is possible within the Dhall language or not.

The Dhall configuration language is also designed to negate many of the common objections to programmable configuration files, such as:

"Config files shouldn't be Turing complete"

Dhall is not Turing-complete. Evaluation always terminates, no exceptions

"Configuration languages become unreadable due to abstraction and indirection"

Every Dhall configuration file can be reduced to a normal form which eliminates all abstraction and indirection

"Users will go crazy with syntax and user-defined constructs"

Dhall is a very minimal programming language. For example: you cannot even compare strings for equality. The language also forbids many other common operations in order to force users to keep things simple

Name

The language is named after a Dustman from the game Planescape: Torment who belongs to a faction obsessed with death (termination). The fountain pen in the logo is the modern analog of Dhall's quill.

The name rhymes with "tall"/"call"/"hall" (i.e. "dɔl" for a US speaker or "dɔːl" for a UK speaker using the International Phonetic Alphabet).

Contributors

Code Contributors

This project exists thanks to all the people who contribute. [Contribute].

Financial Contributors

Become a financial contributor and help us sustain our community. [Contribute]

Individuals

Organizations

Support this project with your organization. Your logo will show up here with a link to your website. [Contribute]

You can’t perform that action at this time.