Compiler implementation plan

[f-f]

The goal for the project is to provide Dhall bindings to/from Clojure. The original plan was to get an MVP working ASAP, with the following steps:

• grab the ABNF and get a free parser for it
• run the reference implementation on Eta, and use it for resolving imports + typechecking + normalizing (Haskell source -> running on Eta -> make Java bindings -> call from Clojure), so that we have to only do the last mile of transforming the evaluated form to a clojure s-exp.

However, this "shortcut" is not viable yet, so it probably makes more sense to just implement the compiler from the get go, to also have another complete implementation of the standard (at the time of writing only the reference Haskell implementation is complete).

A plan for the Dhall compiler implementation is detailed in dhall-lang/dhall-lang#11, and some more info is in the semantics document and the reference implementation.

Checklist for the compiler implementation:

• Parse Dhall code into a Parse Tree
• Transform Parse Tree into Expression Tree
• Resolve imports:
  • Parse into AST
  • Get envvars (with System/getenv)
  • Get local files (with slurp)
  • Get URLs (also with slurp? How about headers? Maybe we have to bring in clj-http) EDIT: now tracked in Implement http imports #7
  • Be careful that imports need to be cached and retrieved once and only once.
  • Also we'll need to perform the semantic integrity checks (basically sha256 on imports). This is not standardized yet, so it's fine if we ignore them for now. EDIT: now tracked in Perform semantic integrity checks #5
  • After all of this is done, the "security concerns" document should be implemented. EDIT: also tracked in Implement http imports #7
• Typecheck
  • shift
  • subst
  • typecheck
• Normalize
  • alpha-normalize
  • beta-normalize
• Simple tests
  • Parse
  • shift
  • subst
  • alpha-normalize
  • beta-normalize
  • typecheck
  • import EDIT: tracked in Add tests for imports #9
• Tests from the Haskell implementation
  • Parse EDIT: tracked in Port parsing tests from the Haskell implementation #10
  • Typecheck
  • Normalize
  • Imports EDIT: tracked in Add tests for imports #9
• emit Clojure s-exps from the Expression Tree

[f-f]

@Gabriel439 is the above somehow accurate? Am I missing any steps?

[Gabriella439]

The only steps missing are the ones not yet standardized (specifically semantic integrity checks). Other than that it looks complete to me

[f-f]

Cool thanks! I didn't consider the semantic integrity checks, added to the list.

[f-f]

Update: as of 878023f, we now parse all Dhall forms (except imports) from text into an Expr tree.
The Expr type itself is copied straight from the haskell implementation (ours is here).

Basically parsing happens like so:

• we generate a parser from the abnf with Instaparse
• run that on input
• convert the resulting "parse tree" to the Expr AST (code is here)

We have ~50 testcases for basic parsing here - we check that a parsed text form generates a certain AST.

[f-f]

As of what to do next, I was thinking about skipping the imports for now (as some things like "semantic integrity checks" are not standard yet) and work on typechecking/normalizing/emit the "pure" subset of Dhall (so that the pipeline is in place and works).

[f-f]

@Gabriel439 I'm implementing beta-normalize for function application, and I was wondering about your implementation of NaturalFold: do I have to differentiate between a strict unrolling and a lazy one or can I just use a single folding strategy? Is it like that for performance reasons?

[Gabriella439]

@f-f: It's purely an optimization and not required by the standard so if you want to do the single folding strategy that is definitely allowed.

Basically the standard allows you to do anything you want as long as the final result is the same. For example, Natural/even/Natural/odd would be very slow if you pedantically followed the reference implementation in the standard.

See: https://github.com/dhall-lang/dhall-lang/blob/master/standard/semantics.md#%CE%B2-normalization

Also, note that the semantics specifies several built-in types, functions and operators that conforming implementations must support. Implementations are encouraged to implement the following functions and operators in more efficient ways than the following reduction rules so long as the result of normalization is the same.

[f-f]

@Gabriel439 cool, thanks.
As you said naively implementing the specification would be inefficient, so I figured the best path forward was to port your implementation (e.g. the even/odd stuff, or the build/fold fusion) but try to omit the small details (e.g. I don't need this lazy/strict differentiation yet, I'll set up profiling/benchmarks before trying to optimise anything).

I'll also reuse your tests for type check/normalisation/etc (and I guess it would be nice move them to the dhall-lang repo at some point, so they can be in sync with the spec)