Dhall for HTML templating about dhall-haskell HOT 6 CLOSED

Alright, dhall-text is up on Hackage now and I also wrote a post on using Dhall as a template engine:

http://www.haskellforall.com/2017/06/dhall-is-now-template-engine.html

I will go ahead and close this since I believe the original problem was solved

from dhall-haskell.

I have a lot to say on this subject!

First, note that list annotations are no longer required for non-empty lists in more recent versions of Dhall, so people can be simplified to:

[ { name = "Maria" , upvotes = +14 }
, { name = "Jordan", upvotes =  +2 }
, { name = "Pranav", upvotes =  +1 }
]

Second, note that master supports Nix-style multi-line string literals and string interpolation, so you can actually use Dhall as a templating engine. For example, you can write your single-item.html file as a Dhall expression and in my opinion it's just as readable as the original HTML version you proposed:

-- single-item.dhall

    λ(person : ./Person.dhall)
→   ''
    <li class="list-group-item">
      <span class="badge">${Natural/show person.upvotes}</span>
      ${person.name}
    </li>
    ''

... and you can similarly rewrite all-items.html as:

-- all-items.dhall

    let List/map = https://ipfs.io/ipfs/Qmbh2ifwcpX9a384vJMehySbV7rdvYhzVbL5ySs84k8BgY/Prelude/List/map
in  let Text/concat = https://ipfs.io/ipfs/Qmbh2ifwcpX9a384vJMehySbV7rdvYhzVbL5ySs84k8BgY/Prelude/Text/concat
in  λ(people : List ./Person.dhall)
→   Text/concat (List/map ./Person.dhall Text ./single-item.dhall people)

... which you can use like this:

$ dhall <<< './all-items.dhall ./people.dhall'
Text

"\n<li class=\"list-group-item\">\n  <span class=\"badge\">+14</span>\n  Maria\n</li>\n\n<li class=\"list-group-item\">\n  <span class=\"badge\">+2</span>\n  Jordan\n</li>\n\n<li class=\"list-group-item\">\n  <span class=\"badge\">+1</span>\n  Pranav\n</li>\n"

There's one missing piece of the puzzle to make dhall a complete templating engine, which is for me to provide a dhall-text utility that checks that the input has type Text and then prints out the normalized Text unescaped. If you had such a utility then you would get:

$ dhall-text <<< './all-items.dhall ./people.dhall'

<li class="list-group-item">
  <span class="badge">+14</span>
  Maria
</li>

<li class="list-group-item">
  <span class="badge">+2</span>
  Jordan
</li>

<li class="list-group-item">
  <span class="badge">+1</span>
  Pranav
</li>

... and I plan on creating such a dhall-text package in the near future

Third, you can define recursive types in Dhall (or System F in general). For example, suppose you had the following contrived Haskell types for representing HTML:

data Node = Items Item | Div Node | Lit Text

data Item = MakeItem [Node]

You can embed that in Dhall, like this:

$ cat Node 
let Node : Type
    =   ∀(Node : Type)
    →   ∀(Item : Type)
    →   ∀(Items : Item → Node)
    →   ∀(Div  : Node → Node)
    →   ∀(Lit : Text → Node)
    →   ∀(MakeItem : List Node → Item)
    →   Node

in  Node

$ cat Item
let Item : Type
    =   ∀(Node : Type)
    →   ∀(Item : Type)
    →   ∀(Items : Item → Node)
    →   ∀(Div  : Node → Node)
    →   ∀(Lit : Text → Node)
    →   ∀(MakeItem : List Node → Item)
    →   Item

in  Item

$ cat Items
let Items : ./Item → ./Node
    =   λ(x : ./Item)
    →   λ(Node : Type)
    →   λ(Item : Type)
    →   λ(Items : Item → Node)
    →   λ(Div  : Node → Node)
    →   λ(Lit : Text → Node)
    →   λ(MakeItem : List Node → Item)
    →   Items (x Node Item Items Div Lit MakeItem)

in  Items

$ cat Div
let Div : ./Node → ./Node
    =   λ(x : ./Node)
    →   λ(Node : Type)
    →   λ(Item : Type)
    →   λ(Items : Item → Node)
    →   λ(Div  : Node → Node)
    →   λ(Lit : Text → Node)
    →   λ(MakeItem : List Node → Item)
    →   Div (x Node Item Items Div Lit MakeItem)

in  Div

$ cat Lit
let Lit : Text → ./Node
    =   λ(x : Text)
    →   λ(Node : Type)
    →   λ(Item : Type)
    →   λ(Items : Item → Node)
    →   λ(Div  : Node → Node)
    →   λ(Lit : Text → Node)
    →   λ(MakeItem : List Node → Item)
    →   Lit x

in  Lit

$ cat MakeItem 
let MakeItem : List ./Node → ./Item
    =   λ(xs : List ./Node)
    →   λ(Node : Type)
    →   λ(Item : Type)
    →   λ(Items : Item → Node)
    →   λ(Div  : Node → Node)
    →   λ(Lit : Text → Node)
    →   λ(MakeItem : List Node → Item)
    →   let List/map = https://ipfs.io/ipfs/Qmbh2ifwcpX9a384vJMehySbV7rdvYhzVbL5ySs84k8BgY/Prelude/List/map
    in  let f = λ(x : ./Node) → x Node Item Items Div Lit MakeItem
    in  MakeItem (List/map ./Node Node f xs)

in  MakeItem

... which you can then use like this:

$ dhall
./Items
(   ./MakeItem
    [   ./Lit "ABC"
    ,   ./Div
        (   ./Items
            (   ./MakeItem
                [   ./Lit "DEF"
                ,   ./Lit "GHI"
                ]
            )
        )
    ]
)
<Ctrl-D>
∀(Node : Type) → ∀(Item : Type) → ∀(Items : Item → Node) → ∀(Div : Node → Node) → ∀(Lit : Text → Node) → ∀(MakeItem : List Node → Item) → Node

λ(Node : Type) → λ(Item : Type) → λ(Items : Item → Node) → λ(Div : Node → Node) → λ(Lit : Text → Node) → λ(MakeItem : List Node → Item) → Items (MakeItem ([Lit "ABC", Div (Items (MakeItem ([Lit "DEF", Lit "GHI"] : List Node)))] : List Node))

... and you can verify that it has type ./Node

It turns out that there are a large class of recursive types that you can embed in a non-recursive System F in this way. The original paper which explains how to do this is:

• Automatic synthesis of typed Λ-programs on term algebras

... and I wrote three blog posts on this subject here:

• Morte: an intermediate language for super-optimizing functional programs
• The internet of code
• Data is code

... and a talk:

• The internet of code

... and a library which implements the above mechanical translation of recursive types to non-recursive types:

• Annah library

Fourth, even though it is possible to translate recursive code to non-recursive code you don't even need to this in the first place. A much simpler approach is to just use the Dhall library API directly to implement your templating engine and when you type check the expression you use the Dhall.TypeCheck.typeWith function instead of Dhall.TypeCheck.typeOf. The typeWith function lets you supply your own custom context to use for type-checking and you can add the builtins that your templating engine needs directly to the context. In this case, your context would just be:

Node : Type
Item : Type
Items : Item → Node
Div : Node → Node
Lit : Text → Node
MakeItem : List Node → Item

... and then after you are done type-checking and normalizing the code you just traverse the syntax tree and replace all free variables that match those names with your built-in Haskell types and/or functions.

So, to summarize, there are three solutions you have available to you:

• Once I provide a dhall-text package you can use Dhall to template the text directly using its built-in support for multi-line string literals and string interpolation
• You can alternatively embed your recursive data type within the Dhall language using a Boehm-Berarducci encoding
• Or if you are willing to use the Dhall API directly you can just type check the expression with your own custom context

from dhall-haskell.

Thanks! That was very helpful. I had not considered the Boehm-Berarducci encoding, so I'm going to read up on that just because it seems interesting. The approach using typeWith seems like it will probably work out the best (especially for end-user error messages), so I'm actually going try implementing that. Also, it's good to hear about dhall-text. I'm a little concerned about how that will play with syntax highlighting in the HTML scenario, but that's definitely just a useful thing to have for a number of cases. It seems like λtext but with types as well.

from dhall-haskell.

@Gabriel439 I started trying to actually do this, and I realized I'm not actually sure how to make the Context that you described. If I start like this:

domContext :: Context (Expr s X)
domContext = DC.empty
  & DC.insert "Node" (Const Type)

That doesn't seem right. I don't want to say that Node is Type; I want to say that the type of Node is Type. Similarly, I don't know what to assign to Div:

domContext :: Context (Expr s X)
domContext = DC.empty
  & DC.insert "Node" ...
  & DC.insert "Div" (Lam "x" (Var "Node") ...)

It's unclear what the right-hand side of the arrow should be.

from dhall-haskell.

Actually, you had it right the first time. The value associated with each key is the type of that key. So if you insert a key-value pair where "Node" is the key and Const Type is the value then that's the same as adding Node : Type to the context

For Div you would use Pi "_" "Node" "Node". This is because a → b is a shorthand for ∀(_ : a) → b and ∀ is internally denoted using the Pi constructor (since universal quantification and pi types are the same thing in a pure type system, which is what Dhall uses under the hood)

from dhall-haskell.

Also, I put up a dhall-text library here: https://github.com/Gabriel439/Haskell-Dhall-Text-Library

I'll release it after the next release of dhall to Hackage

from dhall-haskell.