dhall-recursive-adt-0.1.0.1: Convert recursive ADTs from and to Dhall
Safe HaskellNone
LanguageHaskell2010

Dhall.Deriving.Recursive

Description

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.

Synopsis

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 Source #

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

a
your (recursive) ADT

Constructors

RecADT 

Fields

Instances

Instances details
RecFromDhall a => FromDhall (RecADT a) Source # 
Instance details

Defined in Dhall.Deriving.Recursive

RecToDhall a => ToDhall (RecADT a) Source # 
Instance details

Defined in Dhall.Deriving.Recursive

Utilities

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