Using dhall with eta

[jneira]

Dhall is a programmable configuration language that is not Turing-complete
You can think of Dhall as: JSON + functions + types + imports

(from https://github.com/dhall-lang/dhall-lang)

Dhall is a relatively new configuration language written in haskell and its goals and features marry very well with langs like haskell/eta. Its main advantage over yaml f.e. is that dhall is typed and is guaranteed to terminate so you can make your config more discoverable and safe.

• you can use it to configure programs written in other language: haskell, scala or rust
  • maybe the next can be java or groovy!
• It can be compiled to other config formats like json, yaml, bash, nix or cabal
  • maybe the next could be gradle

Its main drawbacks are:

• it has a lot of dependencies
• maybe it is too much powerful (functions and imports) for simple configurations

The goal of this issue is track the progress and possible problems of the use of dhall ant its tools:

• compilation of dhall-haskell with eta
• execution with eta of all core program subcommands (dhall, dhall repl, dhal format, dhall hash, ...)
  • Tested repl, format, hash and lint
• execution with etlas of its tools:
  • dhall-json: it needed a patch
  • dhall-text,
  • dhall-to-cabal
  • [dhall-nix] (https://github.com/dhall-lang/dhall-nix)
• test performance: we will open a new one if needed
• use dhall-to-etlas to make etlas use dhall as its default configuration input.
  • In progress, tracked in this one: typelead/etlas#66
• create a library to expose the dhall api and make easy the interop with java client code

[puffnfresh]

Sounds good!!

[rahulmutt]

Good stuff! Finally looked into Dhall this morning and it looks great. One cool thing to try out is to make a Dhall-to-Gradle compiler to make Gradle configuration type-safe, similar to the Gradle Kotlin DSL. It would be nice to have proper syntax highlighting for it.

Functions and imports are actually nice for configurations. It means you can provide a standard template configuration and have users modify it to their needs without having to copy/paste which can be error prone. YAML's syntax for key/value abstractions actually uses ad-hoc symbols and I'd take a let expression over that any day!

If we do shift to Dhall though, we should make sure we have lots of templates + examples because StackOverflow won't help people like it would with existing formats.

[NickSeagull]

I love Dhall, but for sure, we should have lots of templates as Rahul mentioned 😄

[jneira]

dhall-to-cabal has been released!
the dhall expression for the cabal of the project itself:

let GitHub-project =
          https://raw.githubusercontent.com/ocharles/dhall-to-cabal/1.0.0/dhall/GitHub-project.dhall

in  let prelude =
          https://raw.githubusercontent.com/ocharles/dhall-to-cabal/1.0.0/dhall/prelude.dhall

in    GitHub-project
      { owner = "ocharles", repo = "example" }
    ⫽ { version = prelude.v "1.0.0"
      , library = prelude.unconditional.library
          (   prelude.defaults.Library
            ⫽ { build-depends =
                  [ { package ="base"
                    , bounds =  prelude.majorBoundVersion (prelude.v "4")
                    }
                  ]
              , exposed-modules =  [ "Hello.World" ]
              }
          )
      }

[rahulmutt]

Really cool :) Does Dhall have a feature to show a simplified version of the config with all the let's inlined and the URLs downloaded? That will be useful for debugging configs.

[jneira]

@rahulmutt yeah, it names it reduce to the normal form:

The normal form is equivalent to the original program except stripped of all imports and indirection

Moreover

dhall-to-cabal is currently running a two-for-one deal! By installing dhall-to-cabal we'll throw in the cabal-to-dhall executable absolutely free! cabal-to-dhall does the reverse of dhall-to-cabal - taking .cabal files and trasforming them into appropriate Dhall expressions. This can be a great way to get started with dhall-to-cabal.

(from https://github.com/dhall-lang/dhall-to-cabal/blob/master/README.md)

[rahulmutt]

That's great to hear - looks like it is going to be good for practical use.

[jneira]

> echo True | etlas run exe:dhall
Up to date
Bool

True

it lives!

[jneira]

• The build has used a bunch of patches that are in this branch of eta-hackage and a fork of dhall-haskell with some minor changes to make it compatible with eta. It used the branch of eta with the switch from cpphs to hpp
• Patches are incomplete: we have to implement the java ffi to double-conversion: https://github.com/jneira/eta-hackage/blob/dhall-patches/patches/double-conversion-2.0.2.0.patch
• We have to test more complex expression involving functions and http calls
• The upstream of dhall-haskell has one type application that we have to revise: dhall-lang/dhall-haskell@master...jneira:master
• We have to try compile and execute dhall-repl component (it is commented for now)

[jneira]

• I've updated the fork of dhall to adapt last commits upstream (it replaces text-format package with formatting)
  • Also replaced the type application with a type annotation: Data.Scientific.fromFloatDigits @Double to Data.Scientific.fromFloatDigits :: Double -> Scientific
• formatting patch added

[jneira]

• As eta is built ghc-7.10.3/lts-6,27 and maybe we would need to build dhall with them, i've created a branch of dhall-haskell with those constraints: https://github.com/dhall-lang/dhall-haskell/compare/master...jneira:ghc-7.10.3?expand=1
• The branch to be used within eta only has (at least for now) the dhall-repl commented: https://github.com/jneira/dhall-haskell/compare/ghc-7.10.3...jneira:eta?expand=1

[rahulmutt]

@jneira Awesome thanks! I think this means we can add support for something like [package-name].dhall and project.dhall for new-build directly inside of etlas by using dhall as a dependency with the lts-6.27-compatible configuration. I have no issues if you use a git dependency to your fork, but I would probably be better if the fork is under the eta-lang org.

Would you be interested in implementing the parser bit that will parse the .dhall into a proper GenericPackageDescription?

[jneira]

@rahulmutt Totally agree with moving the project to eta-lang. The version to use withint eta could be a patch in eta-hackage but obviously the fork to be included in eta it is not. If dhall maintainers think it is a good idea include the branch with ghc-7.10.3 compatibility in the upstream project we could use a git reference in stack.yaml. In any case i am going to move the project.

Would you be interested in implementing the parser bit that will parse the .dhall into a proper GenericPackageDescription?

Sure!

[jneira]

It turns out that dhall-to-cabal already does the conversion of a dhall file to a GenericPackageDescription: https://github.com/dhall-lang/dhall-to-cabal/blob/master/lib/DhallToCabal.hs#L550

[rahulmutt]

In that case, this line:
https://github.com/dhall-lang/dhall-to-cabal/blob/master/dhall-to-cabal.cabal#L85
Needs to be patched to etlas-cabal. And then you can use it as a dependency for etlas.

[jneira]

mmm, it seems it would need some more changes. Maybe we would need a dhall-to-etlas...

[rahulmutt]

@jneira Yes most likely that will be the case. You can create a fork and name is as dhall-to-etlas and add it to the eta-lang org. Then, you can add it as a submodule for the etlas repo.

[rahulmutt]

So there's two things that need to be changed in the internal logic for etlas:

1. When etlas looks for [package-name].cabal, it should also look for [package-name].dhall.
2. When etlas looks for cabal.project, cabal.project.freeze, etc. it should also look for etlas.dhall, etlas.dhall.freeze, etc.

How does that sound?

[jneira]

Otoh, the actual version of dhall is throwing StackOverflowExceptions for some simple inputs (like True or False, but no for 1, +1 or 1.1). It seems the cause is the switch of dhall-haskell to megaparsec instead trifecta as parser library.
As @rahulmutt has noted, that package seems to be continuation based and it would need a patch adding a trampoline function (like aeson or binary)

[jneira]

@rahulmutt sounds good to me, i'll give a try asap

[rahulmutt]

@jneira Can you file the issue with megaparsec on eta-hackage?

[jneira]

Hi, patching megaparsec with typelead/eta-hackage#86, dhall works again with eta
The next step is handle the error when you try to import via http dhall definitions:

C:\ws\eta\dhall\dhall-haskell>etlas run exe:dhall -- --explain
Up to date
let GitHub-project =
          https://raw.githubusercontent.com/ocharles/dhall-to-cabal/1.0.0/dhall/
GitHub-project.dhall
in Github-project
^Z

↳�� https://raw.githubusercontent.com/ocharles/dhall-to-cabal/1.0.0/dhall/GitHub
-project.dhall
JException java.nio.channels.IllegalBlockingModeException

[rahulmutt]

@jneira I have a hunch that's caused by some inconsistent sequence of operations in the network package. I think what's happening is that we're putting it in blocking mode and trying to use some non-blocking operation or vice-versa.

[jneira]

Hi, i have a version of dhall-to-etlas that compiles!
The version has a git reference in stack.yaml to a commit of etlas, so it can be built outside of it. I suppose it will have to be changed to be included as a git submodule in etlas itself.
I dont fully analize the code but i dont sure if it can generate a full GenericPackageDescription usable in etlas.

[rahulmutt]

I agree that it should be a submodule of etlas, just as hackage-security is.

It can generate a GenericPackageDescription here:
https://github.com/eta-lang/dhall-to-etlas/blob/master/lib/DhallToCabal.hs#L346-L348

You'll have to override the readSourcePackage function which is responsible for Cabal file parsing in the new-build system:
https://github.com/typelead/etlas/blob/master/etlas/Distribution/Client/ProjectConfig.hs#L912

In general, grep for readGenericPackageDescription and read the surrounding context and make sure it locates (and gives preference to) .dhall files over .cabal files.

[jneira]

Hi, before including dhall-to-etlas in etlas i've wanted to write a valid dhall-to-etlas.dhall.
The result is longer than cabal version and i have to say that syntax is more noisy than cabal or yaml format. However lets, lambdas and imports are a game changer and the possibilities are very promising.
And the type checking is invaluable.

[jneira]

• The yaml conversion also works after applying this patch

C:\Users\Javier\dev\lang\eta\dhall\dhall-json-1.2.1>echo { a = ["caña","cañi"] } | etlas run exe:dhall-to-yaml
Up to date
---
a:
- "caña"
- "cañi"

[jneira]

• I've setup a project to wrap dhall-haskell and provide a friendly java api over dhall: https://github.com/eta-lang/dhall-eta
• It is a WIP but i've managed to write a simple export to be used from java:

module Dhall.Eta where

import qualified Dhall
import qualified Data.Text as Text
import Java


input :: Dhall.Type a ->  JString -> IO a
input ty = ( Dhall.input ty ) . Text.pack . fromJava

foreign export java "@static org.dhall.eta.Input.bool" bool
  :: JString -> IO Bool
bool = input Dhall.bool

foreign export java "@static org.dhall.eta.Input.str" str
  :: JString -> IO JString
str = fmap toJava . input Dhall.string

foreign export java "@static org.dhall.eta.Input.integer" integer
  :: JString -> IO JInteger
integer = fmap toJava . input Dhall.integer

foreign export java "@static org.dhall.eta.Input.natural" natural
  :: JString -> IO JInteger
natural = fmap ( toJava . toInteger ) . input Dhall.natural

package org.dhall.eta.example;

import org.dhall.eta.Input;

public class Client {
     public static void main (String[] args) {
        System.out.println("Testing dhall");
        System.out.println(Input.bool("True"));
        System.out.println(Input.bool("True && False"));
        try {
            System.out.println(Input.bool("1"));
        } catch (Exception e) {
            System.out.println(e.getLocalizedMessage());
        }
        System.out.println(Input.str("let str=\"dhall\" in \"Hello ${str}\""));
        System.out.println(Input.integer("+1234567"));
        System.out.println(Input.natural("2 * 3 + 4"));
        System.out.println("The end");
    }
}

Output:

Testing dhall
true
false

 [1;31mError [0m: Expression doesn't match annotation

- Bool
+ Natural


1 : Bool

(input):1:1

Hello dhall
1234567
10
The end

[Jyothsnasrinivas]

Awesome work @jneira !

[jneira]

We have started the integration between etlas and dhall: https://github.com/jneira/etlas/tree/dhall:

• The default configuration format for etlas will be dhall so if both dhall and cabal files are present it will choose the dhall file
• As suggested by @rahulmutt the dhall configuration file will be named etlas.dhall for all packages (like rust's Cargo.toml)
• We will integrate the caching mechanism of dhall imports as soon as it is available

[Gabriel439]

One thing that would help on my end is getting this integrated into nixpkgs (cc: @puffnfresh):

https://github.com/eta-lang/eta-nix

That would allow me to add an Eta build of Dhall to my CI so that I can catch potential Eta-related issues earlier (like adding new dependencies that might require work to port to Eta)

I tried using that repository directly but I ran into issues due to mismatch between that repository and nixpkgs (like missing support for the executableHaskellDepends field that cabal2nix generates)

[jneira]

@Gabriel439 that would be awesome, thank you very much
Maybe it would be useful add the build of dhall with the actual stack-lts-6.yaml in CI if possible, cause is the lts used by etlas/eta and it will catch some of the posssible issues (like dhall-lang/dhall-haskell#541) .

[puffnfresh]

@Gabriel439 I've got cabal2nix cabal://dhall instantiated. I don't know if it will compile but I'll at least turn it into valid Nix code. I'll push in a few minutes.

[puffnfresh]

Added a chunk of overrides to get Dhall close to compiling. Got stuck on Cryptonite - it has a jar dependency and I'll have to figure out a way to supply that.

[jneira]

Actually for build master version of dhall-haskell with etlas we would need patch the new dependecy cborg-0.2.0.0: typelead/eta-hackage#111. It seems it could take some effort cause it uses low level data representation and c ffi.

[rahulmutt]

Some updates on running dhall on Eta: I fixed the Bad Record MAC bug (was a bug in cryptonite patch) and the next step is to implement the zlib bits in streaming-commons.

[rahulmutt]

Ok great, https requests seem to work now with the latest patches on eta-hackage. @jneira Can you give dhall network imports a try?

[rahulmutt]

We have patched cborg-0.2.0.0 in typelead/eta-hackage@e400525 - just updating since that issue wasn't linked with @jneira's previous comment.

[jneira]

Hi, after patching the transitive dependency of cborg, serialise, we can build again master version of dhall-haskell. Moreover, with the recent work of @rahulmutt, http imports finally work!:

> echo https://raw.githubusercontent.com/dhall-lang/Prelude/35deff0d41f2bf86c42089c6ca16665537f54d75/List/replicate | etlas run exe:
dhall
Up to date
  λ(n : Natural)

→ λ(a : Type)
)
→ λ(x : a)
)
→ Natural/fold n (List a) (λ(`as` : List a) → [ x ] # `as`) ([] : List a) a)


> echo let rep=https://raw.githubusercontent.com/dhall-lang/Prelude/35deff0d41f2bf86c42089c6ca16665537f54d75/List/replicate in rep 5 Natural 1 | etlas run exe:dhall
Up to date
[ 1, 1, 1, 1, 1 ]

[puffnfresh]

@Gabriel439 I have nix-build '<nixpkgs>' -A 'etaPackages.dhall' building with my overlay.

When evaluating I get:

∀Peeked an empty style stack! Please report this as a bug.

I don't know where this problem is coming in. I'll try updating Eta and eta-hackage and see if it's still a problem.

[ocharles]

@puffnfresh do you mean when evaluating a Dhall expression you get that? It looks possibly like a bug with prettyprinter. I guess that ∀ is because the thing you're trying to evaluate is a forall?

[Gabriel439]

@puffnfresh: The problem you ran into sounds similar to this:

dhall-lang/dhall-haskell#280

What expression did you test on?

[Gabriel439]

@jneira: Would a new dependency on unix-compat be problematic for Eta? The reason I ask is that I'm looking for a cross-platform way to set group/other permissions on directories or files since System.Directory only supports setting user permissions and unix-compat was the closest thing I could find that didn't involve a sub-process call to chmod

[jneira]

@Gabriel439 I am afraid that eta doesnt support unix-compat for now so we will have to patch dhall to replace those calls with java ones (or maybe patch unix-compat itself). Anyway, imo there is no better option (cc @rahulmut) and we already had to patch dhall.

[rahulmutt]

@Gabriel439 You can go ahead and add the dependency. At worst, once the dhall integration is done, we can add an etlas.dhall file which doesn't contain the dependency and uses the Java standard library to perform the same function. We do eventually plan on patching unix and unix-compat once we get an idea of which functions are actually being used by the Hackage ecosystem. So far, we found that filesystem-related operations are the most common.

[jneira]

Although the wrapper of dhall for java is still a wip and full of bugs, i managed to implement almost all public api of Dhall.Parser, Dhall.Core and Dhall.TypeCheck(next will be Dhall.Import):

package org.dhall.eta.example;

import org.dhall.core.*;
import org.dhall.core.expr.ExprIntegerShow;
import org.dhall.parser.*;
import org.dhall.parser.error.*;
import org.dhall.typecheck.TypeError;

import org.dhall.eta.Parser;
import org.dhall.eta.TypeCheck;
import org.dhall.eta.Core;

import org.haskell.types.*;

public class Client {

    public static void main (String[] args) {
        Either<ParseError,Expr<Src,Import>> parsed = Parser.exprFromText("example","1");
        System.out.println("Parsing \"1\":");
        System.out.println(parsed);
        System.out.println("-----------------------------");

        Either<ParseError,Expr<Src,Import>> eParsedFun = 
        		Parser.exprFromText("example","λ (t : Text) -> 1");
        System.out.println("Parsing \"λ (t : Text) -> 1\":");
        System.out.println(eParsedFun);
        System.out.println("-----------------------------");
        
        Either.Matcher<ParseError, Expr<Src,Import>, Expr<Src,Import>> matcher = 
        		new Either.Matcher<>(any -> null);
        matcher.Right(r -> r.getValue());
        Expr<Src,Import> parsedFun =  matcher.match(eParsedFun);
        System.out.println("Pretty printing parsed fun");
        System.out.println(Core.pretty(parsedFun));
        System.out.println("-----------------------------");
        
        Expr<Unit,Import> norm = Core.normalize(parsedFun);
        System.out.println("Normalize fun");
        System.out.println(norm);
        System.out.println("-----------------------------");
        
        Expr<Unit,Import> alphaNorm = Core.alphaNormalize(norm);
        System.out.println("Alpha normalize fun");
        System.out.println(alphaNorm);
        System.out.println("-----------------------------");
        
        Expr<Src,Void> importedExpr = new ExprIntegerShow<>();
        Either<TypeError<Src, Void>,Expr<Src,Void>> checked = TypeCheck.typeOf(importedExpr);
        System.out.println("Type of ExprIntegerShow");
        System.out.println(checked);
        System.out.println("-----------------------------");
        
        System.out.println("The end");
    }
    
}

with this output:

Parsing "1":
Right [ExprNote [annotation=Src{begin=SourcePos{path=example,line=Pos[1],column=Pos[1]},end=SourcePos{path=example,line=Pos[1],column=Pos[2]},text="1"}, subexpr=ExprNatural [Natural [1]]]]
-----------------------------
Parsing "λ (t : Text) -> 1":
Right [ExprNote [annotation=Src{begin=SourcePos{path=example,line=Pos[1],column=Pos[1]},end=SourcePos{path=example,line=Pos[1],column=Pos[18]},text="λ (t : Text) -> 1"}, subexpr=ExprLam [name=t, type=ExprNote [annotation=Src{begin=SourcePos{path=example,line=Pos[1],column=Pos[8]},end=SourcePos{path=example,line=Pos[1],column=Pos[12]},text="Text"}, subexpr=ExprText], body=ExprNote [annotation=Src{begin=SourcePos{path=example,line=Pos[1],column=Pos[17]},end=SourcePos{path=example,line=Pos[1],column=Pos[18]},text="1"}, subexpr=ExprNatural [Natural [1]]]]]]
-----------------------------
Pretty printing parsed fun
λ(t : Text) → 1
-----------------------------
Normalize fun
ExprLam [name=t, type=ExprText, body=ExprNatural [Natural [1]]]
-----------------------------
Alpha normalize fun
ExprLam [name=_, type=ExprText, body=ExprNatural [Natural [1]]]
-----------------------------
Type of ExprIntegerShow
Right [ExprPi [name=_, kind=ExprInteger, body=ExprText]]
-----------------------------
The end

[jneira]

Hi, more advances in dhall-eta, it has more complete wrap over dhall main module, including a converter from dhall to classes. Suggestions about the api are welcome!

public class Client {

    public static void main (String[] args) {
        
        System.out.println("Testing dhall main module");
        
        Type<Boolean> tyBool = Types.bool();
        Boolean bool = Input.type(tyBool, "True");
        System.out.println(bool);
        
        Type<Optional<String>> optStrTy=Types.optional(Types.str());
        Optional<String> optStrIn = Input.type(optStrTy, "Some \"hello\"");
        System.out.println(optStrIn);
        
        Type<List<Natural>> nsTy = Types.list(Types.natural());
        List<Natural> ns = Input.type(nsTy, "[1, 2, 3]");
        System.out.println(ns);
        
        Project p = Input.type(Types.record(new ProjectType()),
        		"{ name = \"dhall\", description = \"desc\", stars = 123 }");
        System.out.println(p);
        System.out.println("The end");
    }
    
    public static class Project {
    	private String name;
    	private String description;
        private Natural stars;
	public Project(String name, String description, Natural stars) {
		super();
		this.name = name;
		this.description = description;
		this.stars = stars;
	}
	// getters and toString boilerplate
    }
    
    public static class ProjectType implements RecordType<Project> {
		
	public Map<String,Type<? extends Object>> getFieldsTypes() {
		LinkedHashMap<String,Type<? extends Object>> fields= new LinkedHashMap<>();
		fields.put("name", Types.str());
		fields.put("description", Types.str());
		fields.put("stars", Types.natural());
		return fields;
	}
		
	public Project fromFieldsValues(Map<String,Object> m) {
		return new Project((String)m.get("name") ,
				   (String)m.get("descripcion"), 
				   (Natural)m.get("stars"));
	}
   }
}

Output:

Testing dhall main module
true
Optional[hello]
[Natural [1], Natural [2], Natural [3]]
Project [name=dhall, description=null, stars=Natural [123]]
The end

[jneira]

We already have released the eta lib to expose a java friendly api over dhall-haskell!
https://github.com/eta-lang/dhall-eta

[ocharles]

Super stuff @jneira! Is this issue ready to be closed?

[jneira]

Well, only left a more complete etlas integration but we could close this one, if nobody disagrees