Dhall.Deriving.Recursive

Convert recursive ADTs from and to Dhall with only some boilerplate.

This module is intended to be used with DerivingVia.

Click Dhall.Deriving.Recursive for a compact example.

Walkthrough

Out of the box, dhall can not derive FromDhall/ToDhall for recursive ADTs like this one

>>> :{
data Expr = Lit Natural
          | Add Expr Expr
          | Mul Expr Expr
 deriving stock Show
:}

As Dhall has no recursion by design, it might be non-obvious how to encode this type in Dhall. Luckily, the Church/Böhm-Berarducci encoding exists, which is essentially a fancy name for the Go4 Visitor pattern, as explained in this blog post. Also make sure check out the official How-to on translating recursive code to Dhall.

Explicitly, consider the non-recursive ADT

>>> :{
data ExprF a = LitF Natural
             | AddF a a
             | MulF a a
:}

For any type a, this is a non-recursive sum type, which we can directly translate to a Dhall union type:

let ExprF = λ(a : Type) → < LitF : Natural | AddF : { _1 : a, _2 : a } | MulF : { _1 : a, _2 : a } >

We can derive FromDhall/ToDhall for ExprF a. Let us use the default Generic-powered version here, but we could also use e.g. Dhall.Deriving for customization (we use StandaloneDeriving here to be able to define the instances one by one).

>>> deriving stock    instance                Generic   (ExprF a)
>>> deriving anyclass instance FromDhall a => FromDhall (ExprF a)
>>> deriving anyclass instance ToDhall a   => ToDhall   (ExprF a)

Right now, Expr and ExprF are completely unrelated. The open type family Base and the type classes Recursive and Corecursive from recursion-schemes are exactly what we need.

We can derive Recursive and Corecursive for Expr as long as we derive Generic for it, and define Base Expr ≔ ExprF as well as derive Functor for ExprF.

>>> import Data.Functor.Foldable (Base, Recursive, Corecursive)
>>> type instance Base Expr = ExprF
>>> deriving stock    instance Functor     ExprF
>>> deriving stock    instance Generic     Expr
>>> deriving anyclass instance Recursive   Expr
>>> deriving anyclass instance Corecursive Expr

With this setup, we can finally derive FromDhall/ToDhall for Expr:

>>> deriving via RecADT Expr instance FromDhall Expr
>>> deriving via RecADT Expr instance ToDhall   Expr

To see how this works, consider this expression representing (1 + 2) * (3 + 4):

>>> expr = Mul (Add (Lit 1) (Lit 2)) (Add (Lit 3) (Lit 4))
>>> import qualified Dhall as D
>>> encodedExpr = D.embed D.inject expr

In Dhall, we can construct an Expr like this:

>>> import qualified Dhall as D
>>> import Yasi
>>> :{
dhallExpr <- D.inputExpr [i|
  let ExprF = λ(a : Type) → < LitF : Natural | AddF : { _1 : a, _2 : a } | MulF : { _1 : a, _2 : a } >
  let Expr  = ∀(a : Type) → (ExprF a → a) → a
  --
  let Lit : Natural → Expr     = λ(n : Natural) →
    λ(a : Type) → λ(make : ExprF a → a) → make ((ExprF a).LitF n)
  --
  let Add : Expr → Expr → Expr = λ(x : Expr) → λ(y : Expr) →
    λ(a : Type) → λ(make : ExprF a → a) → make ((ExprF a).AddF { _1 = x a make, _2 = y a make })
  --
  let Mul : Expr → Expr → Expr = λ(x : Expr) → λ(y : Expr) →
    λ(a : Type) → λ(make : ExprF a → a) → make ((ExprF a).MulF { _1 = x a make, _2 = y a make })
  --
  in  Mul (Add (Lit 1) (Lit 2)) (Add (Lit 3) (Lit 4))
  |]
:}

In fact, we have

>>> import Dhall.Core (judgmentallyEqual)
>>> encodedExpr `judgmentallyEqual` dhallExpr
True
>>> D.extract @Expr D.auto dhallExpr
Success (Mul (Add (Lit 1) (Lit 2)) (Add (Lit 3) (Lit 4)))

Compact example

We can still shorten the boilerplate a bit using makeBaseFunctor.

>>> import Data.Functor.Foldable.TH (makeBaseFunctor)
>>> :{
data Tree a = Leaf a | Branch (Tree a) (Tree a)
makeBaseFunctor ''Tree
:}

>>> deriving stock    instance                               Generic   (TreeF a b)
>>> deriving anyclass instance (FromDhall a, FromDhall b) => FromDhall (TreeF a b)
>>> deriving anyclass instance (ToDhall   a, ToDhall   b) => ToDhall   (TreeF a b)

>>> deriving via RecADT (Tree a) instance FromDhall a => FromDhall (Tree a)
>>> deriving via RecADT (Tree a) instance ToDhall   a => ToDhall   (Tree a)

The test suite contains an expanded example of this situation.

The DerivingVia newtype

newtype RecADT a

Intended to be used with DerivingVia, as explained in the module documentation.

a

your (recursive) ADT

Constructors

RecADT

Fields

• unRecADT :: a

Instances

RecFromDhall a => FromDhall (RecADT a)

Defined in Dhall.Deriving.Recursive

Methods

autoWith :: InputNormalizer -> Decoder (RecADT a)

RecToDhall a => ToDhall (RecADT a)

Defined in Dhall.Deriving.Recursive

Methods

injectWith :: InputNormalizer -> Encoder (RecADT a)

Utilities

If you don't want to derive FromDhall/ToDhall with DerivingVia, use these functions instead.

type RecFromDhall a = (FromDhall (Base a (Result (Base a))), Corecursive a)

recAuto :: RecFromDhall a => Decoder a

recAutoWith :: forall a. RecFromDhall a => InputNormalizer -> Decoder a

type RecToDhall a = (ToDhall (Base a (Result (Base a))), Recursive a)

recInject :: RecToDhall a => Encoder a

recInjectWith :: forall a. RecToDhall a => InputNormalizer -> Encoder a