Ressources on building language bindings

wolf · September 29, 2020, 9:43am

This might be a naive question but I was wondering if there were any resources on how to get started building language bindings for dhall for another language. I’m asking this as somebody who has great interest in how languages get built and how type systems work (aka the will to learn) but without any practical experience in either space beyond reading the superficial blog post here and there.

I’m aware that various bindings already exist:

go
rust
etc

I’m also aware of the “Dhall Acceptance Tests” in the main repository.

Now I could read through the source of the various existing bindings and dig into the acceptance tests - and this is certainly something I will do, if I go forward with this - but I wonder if there is a list of resources which go over the basics, before I have to piece together everything from existing source code. A “Getting Started” if you may.

I’m looking forward to your answers!

Gabriel439 · September 29, 2020, 3:47pm

@wolf: The closest thing we have is the standard:

github.com

dhall-lang/dhall-lang/blob/master/standard/README.md

# Semantics

This document formalizes the semantics for resolving, type-checking and
normalizing Dhall expressions.

Note that this document *does not* specify how a language binding marshals an
normalized Dhall expression into a matching expression in the host language.
The details of how to do so are left open to each implementation, including
supported integer ranges or how to idiomatically encode unions.

Some of these standard documents are literate Haskell code showing how to
translate the natural deduction notation to executable code.  You can build the
Haskell code by running (in this directory):

```bash
$ nix-shell  # Optional, if you want to use the exact same environment as CI
$ cabal build
```

Note that the literate Haskell code is written in such a way as to match the

This file has been truncated. show original

… but the main thing missing from that is an explanation of how to translate natural deduction notation to code. So one of the things I’ve been working on is turn the standard into literate Haskell code to help people along (and also rework the standard to use a more efficient evaluator).

This is the relevant issue:

github.com/dhall-lang/dhall-lang

[RFC] Literate Haskell semantics

opened 11:51AM - 12 Apr 20 UTC

Nadrieril

### TL;DR I propose we write the inference rules of the standard in literate …Haskell, so that they become executable. That would make experimentation easier and the standard more robust. ### Proposal The way we currently write the standard is not the most convenient or robust. Among several issues, inference rules aren't very natural to read or write and are difficult to abstract over. Some bits of the standard (notably the imports spec and the typing rule for merge) are notoriously hard to understand. We rely on implementations to validate tests and ensure the standard is consistent. I propose we instead write the standard in literate Haskell. I believe most contributors here are at least somewhat familiar with Haskell, and in any case we shall not make use of advanced features, to ensure that the standard stays readable to non-Haskellers. The text of the standard need not change, but the infernce rules would be replaced. For example, the typing rule Γ₀ ⊢ A : i ↑(1, x, 0, (Γ₀, x : A)) = Γ₁ Γ₁ ⊢ B : o i ↝ o : c ────────────────────────────────────────────────────────────────── Γ₀ ⊢ ∀(x : A) → B : c could become ```haskell typeOf ctx (Pi x a b) = do i <- typeOf ctx a let ctx1 = push x a ctx o <- typeOf ctx1 b c <- function_check i o return c ``` Benefits: - easier to experiment with new features - more readable semantics - force us to be more precise, eg. around parsing and desugaring - easier to translate the standard into code (since it is already code) - tests are guaranteed to be consistent with the spec Drawbacks: - larger maintenance burden for contributors This is a large undertaking and will take some time and effort. I hope we can reuse a lot of code from `dhall-haskell`, to avoid reinventing everything. We can get there gradually and the benefits will hopefully be worth it.

… and if you look at the sample branch linked from that issue you can see some example code showing how to translate natural deduction to Haskell code: