Safe Haskell | None |
---|---|
Language | Haskell2010 |
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
- newtype RecADT a = RecADT {
- unRecADT :: a
- 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
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
as well as derive Base
Expr ≔ ExprFFunctor
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
Intended to be used with DerivingVia
, as explained in the module documentation.
a
- your (recursive) ADT
Instances
RecFromDhall a => FromDhall (RecADT a) Source # | |
Defined in Dhall.Deriving.Recursive autoWith :: InputNormalizer -> Decoder (RecADT a) # | |
RecToDhall a => ToDhall (RecADT a) Source # | |
Defined in Dhall.Deriving.Recursive injectWith :: InputNormalizer -> Encoder (RecADT a) # |
Utilities
type RecFromDhall a = (FromDhall (Base a (Result (Base a))), Corecursive a) Source #
recAuto :: RecFromDhall a => Decoder a Source #
recAutoWith :: forall a. RecFromDhall a => InputNormalizer -> Decoder a Source #
recInject :: RecToDhall a => Encoder a Source #
recInjectWith :: forall a. RecToDhall a => InputNormalizer -> Encoder a Source #