dhall-recursive-adt (empty) → 0.1.0.0
raw patch · 8 files changed
+535/−0 lines, 8 filesdep +basedep +data-fixdep +dhall
Dependencies added: base, data-fix, dhall, dhall-recursive-adt, either, hedgehog, neat-interpolation, recursion-schemes, tasty, tasty-hedgehog, tasty-hunit
Files
- CHANGELOG.md +5/−0
- LICENSE +121/−0
- README.md +7/−0
- dhall-recursive-adt.cabal +72/−0
- src/Dhall/Deriving/Recursive.hs +200/−0
- test/Docspec.hs +8/−0
- test/Tasty.hs +79/−0
- test/tree.dhall +43/−0
+ CHANGELOG.md view
@@ -0,0 +1,5 @@+# Revision history for dhall-recursive-adt++## 0.1.0.0 -- 2021-01-28++* First version. Released on an uNsUsPeCtInG world.
+ LICENSE view
@@ -0,0 +1,121 @@+Creative Commons Legal Code++CC0 1.0 Universal++ CREATIVE COMMONS CORPORATION IS NOT A LAW FIRM AND DOES NOT PROVIDE+ LEGAL SERVICES. DISTRIBUTION OF THIS DOCUMENT DOES NOT CREATE AN+ ATTORNEY-CLIENT RELATIONSHIP. CREATIVE COMMONS PROVIDES THIS+ INFORMATION ON AN "AS-IS" BASIS. CREATIVE COMMONS MAKES NO WARRANTIES+ REGARDING THE USE OF THIS DOCUMENT OR THE INFORMATION OR WORKS+ PROVIDED HEREUNDER, AND DISCLAIMS LIABILITY FOR DAMAGES RESULTING FROM+ THE USE OF THIS DOCUMENT OR THE INFORMATION OR WORKS PROVIDED+ HEREUNDER.++Statement of Purpose++The laws of most jurisdictions throughout the world automatically confer+exclusive Copyright and Related Rights (defined below) upon the creator+and subsequent owner(s) (each and all, an "owner") of an original work of+authorship and/or a database (each, a "Work").++Certain owners wish to permanently relinquish those rights to a Work for+the purpose of contributing to a commons of creative, cultural and+scientific works ("Commons") that the public can reliably and without fear+of later claims of infringement build upon, modify, incorporate in other+works, reuse and redistribute as freely as possible in any form whatsoever+and for any purposes, including without limitation commercial purposes.+These owners may contribute to the Commons to promote the ideal of a free+culture and the further production of creative, cultural and scientific+works, or to gain reputation or greater distribution for their Work in+part through the use and efforts of others.++For these and/or other purposes and motivations, and without any+expectation of additional consideration or compensation, the person+associating CC0 with a Work (the "Affirmer"), to the extent that he or she+is an owner of Copyright and Related Rights in the Work, voluntarily+elects to apply CC0 to the Work and publicly distribute the Work under its+terms, with knowledge of his or her Copyright and Related Rights in the+Work and the meaning and intended legal effect of CC0 on those rights.++1. Copyright and Related Rights. A Work made available under CC0 may be+protected by copyright and related or neighboring rights ("Copyright and+Related Rights"). Copyright and Related Rights include, but are not+limited to, the following:++ i. the right to reproduce, adapt, distribute, perform, display,+ communicate, and translate a Work;+ ii. moral rights retained by the original author(s) and/or performer(s);+iii. publicity and privacy rights pertaining to a person's image or+ likeness depicted in a Work;+ iv. rights protecting against unfair competition in regards to a Work,+ subject to the limitations in paragraph 4(a), below;+ v. rights protecting the extraction, dissemination, use and reuse of data+ in a Work;+ vi. database rights (such as those arising under Directive 96/9/EC of the+ European Parliament and of the Council of 11 March 1996 on the legal+ protection of databases, and under any national implementation+ thereof, including any amended or successor version of such+ directive); and+vii. other similar, equivalent or corresponding rights throughout the+ world based on applicable law or treaty, and any national+ implementations thereof.++2. Waiver. To the greatest extent permitted by, but not in contravention+of, applicable law, Affirmer hereby overtly, fully, permanently,+irrevocably and unconditionally waives, abandons, and surrenders all of+Affirmer's Copyright and Related Rights and associated claims and causes+of action, whether now known or unknown (including existing as well as+future claims and causes of action), in the Work (i) in all territories+worldwide, (ii) for the maximum duration provided by applicable law or+treaty (including future time extensions), (iii) in any current or future+medium and for any number of copies, and (iv) for any purpose whatsoever,+including without limitation commercial, advertising or promotional+purposes (the "Waiver"). Affirmer makes the Waiver for the benefit of each+member of the public at large and to the detriment of Affirmer's heirs and+successors, fully intending that such Waiver shall not be subject to+revocation, rescission, cancellation, termination, or any other legal or+equitable action to disrupt the quiet enjoyment of the Work by the public+as contemplated by Affirmer's express Statement of Purpose.++3. Public License Fallback. Should any part of the Waiver for any reason+be judged legally invalid or ineffective under applicable law, then the+Waiver shall be preserved to the maximum extent permitted taking into+account Affirmer's express Statement of Purpose. In addition, to the+extent the Waiver is so judged Affirmer hereby grants to each affected+person a royalty-free, non transferable, non sublicensable, non exclusive,+irrevocable and unconditional license to exercise Affirmer's Copyright and+Related Rights in the Work (i) in all territories worldwide, (ii) for the+maximum duration provided by applicable law or treaty (including future+time extensions), (iii) in any current or future medium and for any number+of copies, and (iv) for any purpose whatsoever, including without+limitation commercial, advertising or promotional purposes (the+"License"). The License shall be deemed effective as of the date CC0 was+applied by Affirmer to the Work. Should any part of the License for any+reason be judged legally invalid or ineffective under applicable law, such+partial invalidity or ineffectiveness shall not invalidate the remainder+of the License, and in such case Affirmer hereby affirms that he or she+will not (i) exercise any of his or her remaining Copyright and Related+Rights in the Work or (ii) assert any associated claims and causes of+action with respect to the Work, in either case contrary to Affirmer's+express Statement of Purpose.++4. Limitations and Disclaimers.++ a. No trademark or patent rights held by Affirmer are waived, abandoned,+ surrendered, licensed or otherwise affected by this document.+ b. Affirmer offers the Work as-is and makes no representations or+ warranties of any kind concerning the Work, express, implied,+ statutory or otherwise, including without limitation warranties of+ title, merchantability, fitness for a particular purpose, non+ infringement, or the absence of latent or other defects, accuracy, or+ the present or absence of errors, whether or not discoverable, all to+ the greatest extent permissible under applicable law.+ c. Affirmer disclaims responsibility for clearing rights of other persons+ that may apply to the Work or any use thereof, including without+ limitation any person's Copyright and Related Rights in the Work.+ Further, Affirmer disclaims responsibility for obtaining any necessary+ consents, permissions or other rights required for any use of the+ Work.+ d. Affirmer understands and acknowledges that Creative Commons is not a+ party to this document and has no duty or obligation with respect to+ this CC0 or use of the Work.
+ README.md view
@@ -0,0 +1,7 @@+# dhall-recursive-adt+[](https://github.com/amesgen/dhall-recursive-adt/actions)+[](https://hackage.haskell.org/package/dhall-recursive-adt)++Convert recursive Haskell ADTs from and to [Dhall](https://dhall-lang.org).++See [the haddocks](https://hackage.haskell.org/package/dhall-recursive-adt/docs/Dhall-Deriving-Recursive.html) for documentation.
+ dhall-recursive-adt.cabal view
@@ -0,0 +1,72 @@+cabal-version: 2.4+name: dhall-recursive-adt+version: 0.1.0.0++synopsis: Convert recursive ADTs from and to Dhall+description:+ Convert recursive ADTs from and to Dhall by automating derivation of @FromDhall@/@ToDhall@ as much as possible+category: Dhall++homepage: https://github.com/amesgen/dhall-recursive-adt+bug-reports: https://github.com/amesgen/dhall-recursive-adt/issues+license: CC0-1.0+license-file: LICENSE+extra-source-files: README.md+author: amesgen+maintainer: amesgen@amesgen.de+extra-source-files:+ CHANGELOG.md++ test/tree.dhall++source-repository head+ location: https://github.com/amesgen/dhall-recursive-adt+ type: git++common commons+ default-language: Haskell2010+ ghc-options: -Wall -Wincomplete-record-updates -Wincomplete-uni-patterns -Wredundant-constraints -Wmissing-export-lists -fno-warn-name-shadowing -fhide-source-paths+ if impl(ghc >= 8.8)+ ghc-options: -Wmissing-deriving-strategies+ if impl(ghc >= 8.10)+ ghc-options: -Wunused-packages+ default-extensions: BlockArguments ConstraintKinds DeriveAnyClass DeriveFoldable DeriveGeneric DeriveTraversable DerivingVia FlexibleContexts GeneralizedNewtypeDeriving LambdaCase ScopedTypeVariables StandaloneDeriving TypeApplications TypeFamilies OverloadedStrings++library+ import: commons+ hs-source-dirs: src+ exposed-modules:+ Dhall.Deriving.Recursive+ build-depends:+ base >= 4.12 && < 5+ , dhall ^>= 1.38+ , data-fix ^>= 0.3+ , recursion-schemes ^>= 5.2++test-suite tasty+ import: commons+ type: exitcode-stdio-1.0+ main-is: Tasty.hs+ hs-source-dirs: test+ ghc-options: -threaded -rtsopts -with-rtsopts=-N+ build-depends:+ base+ , dhall-recursive-adt+ , dhall+ , either ^>= 5+ , recursion-schemes+ , tasty >= 1.3 && <= 1.5+ , tasty-hunit ^>= 0.10+ , tasty-hedgehog ^>= 1+ , hedgehog ^>= 1++test-suite docspec+ import: commons+ if impl(ghc >= 8.10)+ ghc-options: -fno-warn-unused-packages+ type: exitcode-stdio-1.0+ main-is: Docspec.hs+ hs-source-dirs: test+ build-depends:+ base+ , neat-interpolation ^>= 0.5
+ src/Dhall/Deriving/Recursive.hs view
@@ -0,0 +1,200 @@+{-# LANGUAGE UndecidableInstances #-}++-- | Convert /recursive/ ADTs from and to Dhall with only /some/ boilerplate.+--+-- This module is intended to be used with+-- [@DerivingVia@](https://downloads.haskell.org/~ghc/latest/docs/html/users_guide/glasgow_exts.html#extension-DerivingVia).+--+-- Click "Dhall.Deriving.Recursive#example" for a compact example.+module Dhall.Deriving.Recursive+ ( -- * Walkthrough+ -- $walkthrough++ -- * Compact example+ -- $example++ -- * The @DerivingVia@ newtype+ RecADT (..),++ -- * Utilities+ -- $utilities+ RecFromDhall,+ recAuto,+ recAutoWith,+ RecToDhall,+ recInject,+ recInjectWith,+ )+where++import Data.Fix (Fix)+import Data.Functor.Contravariant (contramap)+import Data.Functor.Foldable (Base, Corecursive, Recursive, refix)+import qualified Dhall as D++-- | Intended to be used with @DerivingVia@, as explained in the module documentation.+--+-- [@a@]: your (recursive) ADT++-- We could work without UndecidableInstances if we added a type parameter f (~ Base a).+-- This wouldn't be a disaster, but it is a bit less convenient.+newtype RecADT a = RecADT {unRecADT :: a}++instance RecFromDhall a => D.FromDhall (RecADT a) where+ autoWith = fmap RecADT . recAutoWith++instance RecToDhall a => D.ToDhall (RecADT a) where+ injectWith = contramap unRecADT . recInjectWith++type RecFromDhall a = (D.FromDhall (Base a (D.Result (Base a))), Corecursive a)++recAuto :: RecFromDhall a => D.Decoder a+recAuto = recAutoWith D.defaultInputNormalizer++recAutoWith :: forall a. RecFromDhall a => D.InputNormalizer -> D.Decoder a+recAutoWith = fmap refix . D.autoWith @(Fix (Base a))++type RecToDhall a = (D.ToDhall (Base a (D.Result (Base a))), Recursive a)++recInject :: RecToDhall a => D.Encoder a+recInject = recInjectWith D.defaultInputNormalizer++recInjectWith :: forall a. RecToDhall a => D.InputNormalizer -> D.Encoder a+recInjectWith = contramap refix . D.injectWith @(Fix (Base a))++-- $setup+--+-- >>> import Numeric.Natural (Natural)+-- >>> import GHC.Generics (Generic)+-- >>> import Dhall (FromDhall, ToDhall)+-- >>> :set -XDerivingVia+-- >>> :set -XDeriveAnyClass+-- >>> :set -XDeriveFunctor+-- >>> :set -XDeriveFoldable+-- >>> :set -XDeriveTraversable+-- >>> :set -XDeriveGeneric+-- >>> :set -XOverloadedStrings+-- >>> :set -XQuasiQuotes+-- >>> :set -XStandaloneDeriving+-- >>> :set -XTemplateHaskell+-- >>> :set -XTypeApplications+-- >>> :set -XTypeFamilies++-- $walkthrough+--+-- Out of the box, [dhall](https://hackage.haskell.org/package/dhall) can not derive 'D.FromDhall'/'D.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](https://en.wikipedia.org/wiki/Visitor_pattern), as explained in+-- [this blog post](https://www.haskellforall.com/2021/01/the-visitor-pattern-is-essentially-same.html).+-- Also make sure check out the+-- [official How-to on translating recursive code to Dhall](https://docs.dhall-lang.org/howtos/How-to-translate-recursive-code-to-Dhall.html).+--+-- 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 'D.FromDhall'\/'D.ToDhall' for @ExprF a@. Let us use the default 'GHC.Generics.Generic'-powered+-- version here, but we could also use e.g. "Dhall.Deriving" for customization (we use+-- [@StandaloneDeriving@](https://downloads.haskell.org/~ghc/latest/docs/html/users_guide/glasgow_exts.html#extension-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](https://hackage.haskell.org/package/recursion-schemes)+-- are exactly what we need.+--+-- We can derive 'Recursive' and 'Corecursive' for @Expr@ as long as we derive 'GHC.Generics.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 'D.FromDhall'\/'D.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 NeatInterpolation+-- >>> :{+-- dhallExpr <- D.inputExpr [trimming|+-- 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)))++-- $example+-- #example#+--+-- We can still shorten the boilerplate a bit using 'Data.Functor.Foldable.TH.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.++-- $utilities+--+-- If you don't want to derive 'D.FromDhall'/'D.ToDhall' with @DerivingVia@, use these functions instead.
+ test/Docspec.hs view
@@ -0,0 +1,8 @@+module Main (main) where++main :: IO ()+main = do+ putStrLn "This test-suite exists only to add dependencies"+ putStrLn "To run docspecs:"+ putStrLn " cabal build --enable-tests"+ putStrLn " ./docspec.sh"
+ test/Tasty.hs view
@@ -0,0 +1,79 @@+module Main (main) where++import Control.Monad (join)+import Data.Coerce (coerce)+import Data.Either.Validation (Validation (..), validationToEither)+import Data.Functor.Foldable (Base, Corecursive, Recursive, cata)+import qualified Dhall as D+import qualified Dhall.Core as D+import Dhall.Deriving.Recursive (RecADT (RecADT))+import GHC.Generics (Generic)+import Hedgehog+import qualified Hedgehog.Gen as Gen+import qualified Hedgehog.Range as Range+import Numeric.Natural (Natural)+import Test.Tasty+import Test.Tasty.HUnit+import Test.Tasty.Hedgehog++data Tree a = Leaf a | Branch (Tree a) (Tree a)+ deriving stock (Show, Eq, Generic)+ deriving anyclass (Recursive, Corecursive)+ deriving (D.FromDhall, D.ToDhall) via (RecADT (Tree a))++type instance Base (Tree a) = TreeF a++data TreeF a b = LeafF a | BranchF b b+ deriving stock (Functor, Generic)+ deriving anyclass (D.FromDhall, D.ToDhall)++main :: IO ()+main = do+ let fld = ("(./test/tree.dhall)." <>)+ dhallTree <- D.inputExpr $ fld "exampleTree"+ dhallLeafList :: Tree Natural -> [Natural] <- D.input D.auto $ fld "leafList"++ defaultMain . testGroup "tests" $+ [ testCase "Haskell → Dhall" $+ JExpr dhallTree @=? JExpr do D.embed D.inject haskellTree,+ testCase "Dhall → Haskell" $+ assertValidation haskellTree $ D.extract D.auto dhallTree,+ testProperty "Dhall function = Haskell function" $ property do+ t <- forAll genTree+ dhallLeafList t === haskellLeafList t,+ testProperty "roundtrip Haskell → Dhall → Haskell" $ property do+ t <- forAll genTree+ let roundtrip = D.extract D.auto . D.embed D.inject+ t' <- evalEither . validationToEither $ roundtrip t+ t === t',+ testProperty "roundtrip Dhall → Haskell → Dhall" $ property do+ t <- D.embed D.inject <$> forAll genTree+ let roundtrip = fmap (D.embed D.inject) . D.extract (D.auto @(Tree Natural))+ t' <- evalEither . validationToEither $ roundtrip t+ JExpr t === JExpr t'+ ]+ where+ haskellTree :: Tree Natural+ haskellTree = Branch (Branch (Branch (Leaf 0) (Leaf 5)) (Branch (Leaf 4) (Leaf 3))) (Leaf 6)++ haskellLeafList :: Tree a -> [a]+ haskellLeafList = cata \case+ LeafF a -> [a]+ BranchF t t' -> t <> t'++ genTree :: MonadGen m => m (Tree Natural)+ genTree =+ Gen.recursive+ Gen.choice+ [Leaf <$> Gen.integral_ (Range.linear 0 100)]+ [join Gen.subterm2 genTree Branch]++newtype JExpr s a = JExpr (D.Expr s a)+ deriving newtype (Show)++instance Eq a => Eq (JExpr s a) where+ (==) = coerce (D.judgmentallyEqual @a @s @s)++assertValidation :: (HasCallStack, Show e, Show a, Eq a) => a -> Validation e a -> Assertion+assertValidation a (Success a') = a @=? a'+assertValidation _ (Failure e) = assertFailure $ show e
+ test/tree.dhall view
@@ -0,0 +1,43 @@+let TreeF =+ λ(A : Type) → λ(b : Type) → < LeafF : A | BranchF : { _1 : b, _2 : b } >++let Tree = λ(A : Type) → ∀(b : Type) → (TreeF A b → b) → b++let Leaf+ : ∀(A : Type) → A → Tree A+ = λ(A : Type) →+ λ(a : A) →+ λ(b : Type) →+ λ(make : TreeF A b → b) →+ make ((TreeF A b).LeafF a)++let Branch+ : ∀(A : Type) → Tree A → Tree A → Tree A+ = λ(A : Type) →+ λ(t : Tree A) →+ λ(u : Tree A) →+ λ(b : Type) →+ λ(make : TreeF A b → b) →+ make ((TreeF A b).BranchF { _1 = t b make, _2 = u b make })++let leafList+ : ∀(A : Type) → Tree A → List A+ = λ(A : Type) →+ λ(t : Tree A) →+ t+ (List A)+ ( λ(tf : TreeF A (List A)) →+ merge+ { LeafF = λ(a : A) → [ a ]+ , BranchF = λ(t : { _1 : List A, _2 : List A }) → t._1 # t._2+ }+ tf+ )++let l = Leaf Natural++let b = Branch Natural++in { exampleTree = b (b (b (l 0) (l 5)) (b (l 4) (l 3))) (l 6)+ , leafList = leafList Natural+ }