Add dhalli, an interactive REPL for Dhall #266
Conversation
This commit splits out the pretty printing logic from Dhall.Core into its own module. Dhall.Core actually relies on some "internal" pretty printing functions, so pretty printing has been moved to Dhall.Pretty.Internal - Dhall.Pretty exposes the public facing interface.
This commit introduces dhalli, a fairly minimal Dhall REPL that supports: * Evalution of Dhall expressions along with import resolution * Type inspection of abritrary expressions * Syntax highlighting and pretty printing for output * Persistent bindings with :let * One-expression lookup with an implicit "it" binding
|
I've based this on the semantic pretty printing branch, as I want syntax highlighting for output. |
|
@ocharles: Note that this still needs to resolve the merge conflicts from the original pretty-printing branch |
|
Now that the other branches are merged, could you merge |
dhalli/Main.hs
Outdated
|
|
||
|
|
||
| data Env = Env | ||
| { envBindings :: StrictMap.Map Dhall.Text Binding |
There was a problem hiding this comment.
Dhall bindings should probably be an ordered association list (i.e. [(Text, Binding)]) like the Context. The reason order matters is so that x@n references to shadowed variables work correctly
In other words, something like this should work:
> :let x = True
> :let x = False
> x@1
Bool
TrueThe other reason you want to do this is to avoid bugs such as the following:
> :let x = 1
> :let y = x : Integer
> :let x = TrueIf you used a Map for that then the second x would override the first x and you would turn y from a well-typed to an ill-typed term.
There was a problem hiding this comment.
If you used a Map for that then the second x would override the first x and you would turn y from a well-typed to an ill-typed term.
That's not quite true, as expressions are normalized before putting them into the environment. So in this case, you'd add (x, 1), then (y, 1), then replace (x, True).
You're otherwise right though, so I'll make that change.
dhalli/Main.hs
Outdated
|
|
||
| return | ||
| ( Dhall.normalize | ||
| ( StrictMap.foldlWithKey' |
There was a problem hiding this comment.
A more accurate way to do this and to correctly take into account variable shadowing and variable capture is to create a nested let expression from the previous bindings and normalize that.
dhalli/Main.hs
Outdated
| normalize loaded | ||
|
|
||
| t <- | ||
| typeCheck expr |
There was a problem hiding this comment.
You need to type-check the expression before normalization, otherwise the expression can diverge
dhalli/Main.hs
Outdated
| ( Expr.Annot ( Expr.Var ( Dhall.V varName 0 ) ) t ) | ||
|
|
||
| addBinding _ = | ||
| error ":let should be of the form `:let x = y`" |
There was a problem hiding this comment.
You probably want to use liftIO . fail instead of error. The issue with error is that it is not evaluation-safe:
error message `seq` () = error message
fail message `seq` () = ()
dhall.cabal
Outdated
| @@ -147,6 +147,22 @@ Executable dhall | |||
| Other-Modules: | |||
| Paths_dhall | |||
|
|
|||
| Executable dhalli | |||
There was a problem hiding this comment.
Perhaps call this dhall-repl instead
dhalli/Main.hs
Outdated
|
|
||
|
|
||
| greeter :: MonadIO m => m () | ||
| greeter = |
There was a problem hiding this comment.
I would skip the greeter. I try to keep the tooling minimal and unintrusive
dhalli/Main.hs
Outdated
| => Repline.Options m | ||
| options = | ||
| [ ( "type", dontCrash . typeOf ) | ||
| , ( "let", dontCrash . addBinding ) |
There was a problem hiding this comment.
Another useful option would be save:
> :save ./x = 1
> ./x
Integer
1
|
I've addressed all your suggestions except for |
|
Thanks! This looks amazing :) |
This commit introduces dhalli, a fairly minimal Dhall REPL that supports: