Idrall

Dhall bindings for Idris.

Parse, evaluate, check/infer types of Dhall expressions.

Status

Still a work in progress, but for a given dhall expression with not much imports, idrall should be able to parse/type check and attempt evaluation. Type checker is pretty complete (one test is failing but that is due to this Idris2 issue. Need to start running the other tests like parsing/normalisation etc. Everything around imports needs some work. There's now an elaborator reflection, but it's pretty new so will see how it handles.

Derive Usage (WIP)

For an example of how to do a whole parse -> resolve -> typecheck -> eval pass of a dhall file, and marshall it into an idris type, check out the file ./examples/Package.idr

There are FromDhall and ToDhall interfaces that you can use elaborator reflection to derive. You can use it for both ADTs and Records like so:

-- ADT example
data ExADT1
  = Foo
  | Bar Bool
  | Baz (Maybe Bool)

%runElab (deriveFromDhall ADT `{ ExADT1 })
%runElab (deriveToDhall ADT `{ ExADT1 })

-- Record example
record ExRec1 where
  constructor MkExRec1
  mn : Maybe Nat

%runElab (deriveFromDhall Record `{ ExRec1 })
%runElab (deriveToDhall Record `{ ExRec1 })

There's implementations of FromDhall and ToDhall for String, Nat, Integer, Bool, Double, and List/Maybe of those. That FromDhall interface gives you the fromDhall function you can use on dhall expression to get a Maybe of your Idris ADT or Record. The ToDhall interface gives you a toDhall and toDhallType function, for returning dhall literals and dhall types respectively. For more examples see the ./examples or the ./tests/derive dir.

The behaviour of this isn't thought out yet. For example, the deriveFromDhall ADT function ignores the dhall union and just looks for matching constructors. Also deriveFromDhall Record ignores extra fields on the dhall record. This behaviour may change.

For error messages, when the compiler knows what dhall file the input text comes from, it can render a good error message with the fancyError function. The error messages are less good when it's just reading dhall from a random idris String.

Indepth Usage (very alpha, YMMV)

Functions for parsing/evaluating/typechecking/resolving dhall expressions, should you need to ve a lot of control over how those things happen. These are all janky names and subject to change.

There's some functions in Idrall/APIv1.idr that expose the parsing/type checking/evaluation. The valueFromString function takes a dhall string, infers it's type, then evaluates it. If you have idris2 installed you can run the following shell commands (prefixed with a $) from the root dir of this repo:

$ idris2 Idrall/APIv1.idr -p contrib --client ':exec doStuff valueFromString "{hello = 1, world = 2}.world + 3"'
Success: (VNaturalLit 5)

You can also create local dhall files, like the one provided at examples/if-function.dhall:

$ cat examples/if-function.dhall
let f = λ(x : Bool) →
  if x
  then "it's true!"
  else "nah"
in f True

and use valueFromString to evaluate them as follows. Note the path in the string:

$ idris2 Idrall/APIv1.idr -p contrib --client ':exec doStuff valueFromString "./examples/if-function.dhall"'
Success: (VTextLit (MkVChunks [] "it's true!"))

To see the types it is returning you'll want to check out IOEither.idr and Value.idr.

There's still not much of an API, and this will hopefully change, but this should be enough to help you kick the tires if you're curious. If you find any problems or have any suggests, issues and pull requests are welcome.

Features

Most language features are in and should be working relatively correctly. The import system is incomplete, and other behaviour is also missing.

Imports

• Keyword: missing
• Operator: ?
• Keyword: as Text
• Keyword: using
• Local imports (/path/to/file.dhall)
• Environment variables
• HTTP imports
• Semantic integrity checks

Other

• Normalisation under binders
• Anything to do with caching
• CBOR representation

Dependencies

idris2

Not required, but some of the Makefile commands use rlwrap to make the Idris2 repl behave better.

Installation

make install

Tests

Note: You'll need to clone the submodules (git submodule update --init) for the tests to run, as they depend on the dhall-lang project test files. After that, you can run:

make test

Implementation details

Type checking

Type checking and inference (aka synthesis) in Dhall is covered by these rules. The rules are implemented here using a technique called Normalisation by Evaluation (NbE). It is described in this paper by David Christiansen, and was also used by @AndrasKovaks in their branch on dhall-Haskell (I found this commit particularly useful).

The general idea of NbE is that you have a data structure that represents the raw syntax Language, which is called Expr here. Expressions can be literals (3, True), types (Natural, Bool, Type), functions, builtins, operators, etc. You evaluate the Expr to a data structure that only represents expressions that cannot be reduced further, called Value here. Eg, the expression True && False can be represented in an Expr, but as a Value would be reduced to False.

To convert a Value back to an Expr is called "reading back" or "quoting".

To normalise an Expr you evaluate it to a Value, then read it back to a Expr, this which ensures it's fully normalised.

Type synthesis (or type inference) takes an Expr and returns its type as a Value.

Type checking checks an Expr against a type given as a Value. A Value is synthesised for the type of the Expr, and both this Value and the provided type Value are read back to Exprs. This ensures there are no reducible expressions in either. Now you can compare the types using an alpha equivalence check to see if they match.

That was a very brief, potentially wrong introduction to the NbE technique used. I'm glossing over a bunch of details about closures, neutral values, the environment/context, etc. but this should be enough to get started with. See the above paper for a full description, and check out the code to see it in action.

Contributions

Any contributions would be appreciated, also just try using this and opening any issues if you find any would be great. greping the code for TODO will show a lot of rough edges that could use some attention. If anything in the "Future work" section below catches your eye you can try that too!

Examples of adding language features

Adding features generally means editing the Expr and Value types, the parser, the eval/check/synth functions, the tests etc.

As an example, the List type was added via #1, and literal values of type list ([1, 2, 3]) were added via #2. For an example of an operator, #3 adds the # operator for appending lists.

Idris1 compatibility

There is an idris1 tag which is the last confirmed commit that works with idris1. It's got all the dhall types and not much else, so if you're desperate for a Dhall implementation for idris1 it may help, but realistically you're gonna need the Idris2 version.

Updating the dhall-lang git submodule

Run git submodule update --recursive --remote

Future work

• Add the missing things from the features list above.
• Use dependent types to prove field names in values are elements of their Unions/Records.
• Improve postfix operator parsing (x.y, x.(y), x.{y}...)
• Think about what api/types to expose so as to make this as nice as possible to use.
• Scope checking as found in Tiny Idris, you can find some failed attempts here.