f-f / dhall-clj Goto Github PK

As implemented in dhall-lang/dhall-haskell#863

This is not theoretically blocked by #7, but in practice it's not needed until then.

To preserve source information, the Haskell implementation uses a Note constructor as a wrapper.

We get this data already from Instaparse as metadata, so we should just pass this metadata around.
This would probably mean be careful about creating new objects (because they should carry the meta from the old ones) or even just applying non-meta-aware functions to them.

We should test that given a Dhall expression, both the Haskell implementation and this one serialize to the same bytes

Fix: https://help.appveyor.com/discussions/problems/6908-is-there-a-way-to-increase-java-heap-size-javalangoutofmemory

As standardized in dhall-lang/dhall-lang#263 and implemented in dhall-lang/dhall-haskell#667

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 #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 #5
  • After all of this is done, the "security concerns" document should be implemented. EDIT: also tracked in #7
• Typecheck
  • shift
  • subst
  • typecheck
• Normalize
  • alpha-normalize
  • beta-normalize
• Simple tests
  • Parse
  • shift
  • subst
  • alpha-normalize
  • beta-normalize
  • typecheck
  • import EDIT: tracked in #9
• Tests from the Haskell implementation
  • Parse EDIT: tracked in #10
  • Typecheck
  • Normalize
  • Imports EDIT: tracked in #9
• emit Clojure s-exps from the Expression Tree

As standardized in dhall-lang/dhall-lang#308 and (partially) implemented in dhall-lang/dhall-haskell#728

As mentioned in dhall-lang/dhall-haskell#568, the current tests for the Haskell implementation do not check for the "correct parse", so it'd be nice to generate the correct AST and check against that.

As standardized in dhall-lang/dhall-lang#293 and implemented in dhall-lang/dhall-haskell#690

It should be possible to import Dhall expressions over http/https, as defined in the standard.

This would mean implementing proper "import chaining", and check that we're respecting the Security Concerns document.

Some tests for beta-normalization are failing

As described in the standard

As standardized in dhall-lang/dhall-lang#238

We should perform the semantic integrity checks on imports (right now they are skipped)

Blocked by #4 (as we should hash the binary-encoded blob)

As standardized in dhall-lang/dhall-lang#307 and implemented in dhall-lang/dhall-haskell#726

The following expression is broken in our interpreter:

λ(x : Bool) → λ(x : Bool) → x@1

since it emits the following form:

(clojure.core/fn [x] (clojure.core/fn [x] x-1))

which doesn't make any sense.

The problem here is that Clojure does not support accessing shadowed bindings, so to fix this we should rename all variables to something unique; the sanest option is to use the De Bruijn indices for it e.g. x@0 -> x_0.
In this way we can solve this by just applying α-normalization parametrized by the rename variable (instead of _)

See dhall-lang/dhall-haskell#596

E.g. see ClojureScript's AppVeyor config

Since we get the type of an expression from the typecheck, we could validate it against a user-provided spec.

As standardized in dhall-lang/dhall-lang#194

Most likely with GitlabCI. It should run tests only on master for now.

As standardized in dhall-lang/dhall-lang#334

As standardized in dhall-lang/dhall-lang#266, dhall-lang/dhall-lang#271 and implemented in dhall-lang/dhall-haskell#675

The ? operator to alternatively resolve imports should be supported

As standardized in dhall-lang/dhall-lang@af53b07

..and implemented in dhall-lang/dhall-haskell#657