Merge pull request #52 from VictorCMiraldo/candidate-2.1.0

Version 2.1.0

generics-mrsop.cabal

@@ -1,5 +1,5 @@
 name:                generics-mrsop
-version:             2.0.0
+version:             2.1.0
 
 synopsis:            Generic Programming with Mutually Recursive Sums of Products.
 
@@ -36,6 +36,7 @@ library
     Generics.MRSOP.Base,
     Generics.MRSOP.Opaque,
     Generics.MRSOP.Util,
+    Generics.MRSOP.Holes
     Generics.MRSOP.TH,
     Generics.MRSOP.Zipper,
     Generics.MRSOP.Zipper.Deep,
@@ -80,4 +81,4 @@ source-repository head
 source-repository this
   type:     git
   location: https://github.com/VictorCMiraldo/generics-mrsop
-  tag: v2.0.0
+  tag: v2.1.0

src/Generics/MRSOP/AG.hs

@@ -11,68 +11,65 @@ module Generics.MRSOP.AG where
 
 import Generics.MRSOP.Base
 
--- | Annotated version of Fix.   This is basically the 'Cofree' datatype,
--- but for n-ary functors
+-- * Annotated Fixpoints
+
+-- $annfixpoints
+--
+-- Annotated fixpoints are a very useful construction. Suppose the generic
+-- algorithm at hand frequently requires the height of the tree being processed.
+-- Instead of recomputing the height of the trees everytime we need them,
+-- we can annotate the whole tree with its height at each given point.
+--
+-- Given an algebra that computes height at one point, assuming
+-- the recursive positions have been substituted with their own heights,
+--
+--   > heightAlgebra :: Rep ki (Const Int) xs -> Const Int iy
+--   > heightAlgebra = Const . (1+) . elimRep (const 0) getConst (maximum . (0:))
+--
+-- We can annotate each node with their height with the 'synthesize' function.
+--
+--   > synthesize heightAlgebra :: Fix ki codes ix -> AnnFix ki codes (Const Int) ix
+--
+-- Note how using just 'cata' would simply count the number of nodes, forgetting
+-- the intermediate values.
+--
+--   > cata heightAlgebra :: Fix ki codes ix -> Const Int ix
+--
+
+-- | Annotated version of Fix. This is basically the 'Cofree' datatype,
+-- but for n-ary functors. 
 data AnnFix (ki :: kon -> *) (codes :: [[[Atom kon]]]) (phi :: Nat -> *) (n :: Nat) =
-  AnnFix (phi n)
-         (Rep ki (AnnFix ki codes phi) (Lkup n codes))
+  AnnFix (phi n) (Rep ki (AnnFix ki codes phi) (Lkup n codes))
 
+-- |Retrieves the top annotation at the current value.
 getAnn :: AnnFix ki codes ann ix -> ann ix
 getAnn (AnnFix a _) = a
 
+-- |Catamorphism with access to the annotations
 annCata :: IsNat ix
-        => (forall iy. IsNat iy => chi iy -> Rep ki phi (Lkup iy codes) -> phi iy)
+        => (forall iy. IsNat iy => chi iy -> Rep ki phi (Lkup iy codes) -> phi iy) -- ^
         -> AnnFix ki codes chi ix
         -> phi ix
 annCata f (AnnFix a x) = f a (mapRep (annCata f) x)
 
--- | Forget the annotations
+-- | Forgetful natural transformation back into 'Fix'
 forgetAnn :: AnnFix ki codes a ix -> Fix ki codes ix
 forgetAnn (AnnFix _ rep) = Fix (mapRep forgetAnn rep)
 
+-- | Maps over the annotations within an annotated fixpoint
 mapAnn :: (IsNat ix)
-       => (forall iy. chi iy -> phi iy)
+       => (forall iy. chi iy -> phi iy) -- ^
        -> AnnFix ki codes chi ix
        -> AnnFix ki codes phi ix
 mapAnn f = synthesizeAnn (\x _ -> f x)
 
--- | Synthesized attributes
-synthesizeAnn :: forall ki codes chi phi ix
-               . (IsNat ix)
-              => 
-                 (forall iy. chi iy -> Rep ki phi (Lkup iy codes) -> phi iy)
-              -> AnnFix ki codes chi ix
-              -> AnnFix ki codes phi ix
-synthesizeAnn f = annCata alg
-  where
-    alg :: forall iy
-         . chi iy
-        -> Rep ki (AnnFix ki codes phi) (Lkup iy codes)
-        -> AnnFix ki codes phi iy
-    alg ann rep = AnnFix (f ann (mapRep getAnn rep)) rep
-
 
--- |Example of using 'synthesize' to annotate a tree with its size
--- at every node.
---
---   > sizeAlgebra :: Rep ki (Const (Sum Int)) xs -> Const (Sum Int) iy
---   > sizeAlgebra = (Const 1 <>) . monoidAlgebra
---
--- Annotate each node with the number of subtrees
---
---   > sizeGeneric' :: (IsNat ix)
---   >              => Fix ki codes ix -> AnnFix ki codes (Const (Sum Int)) ix
---   > sizeGeneric' = synthesize sizeAlgebra
---
--- Note how using just 'cata' will simply count the number of nodes
---
---   > sizeGeneric :: (IsNat ix)
---   >             => Fix ki codes ix -> Const (Sum Int) ix
---   > sizeGeneric = cata sizeAlgebra
---
+-- |Annotates a tree at every node with the result
+-- of the catamorphism with the supplied algebra called at
+-- each node.
 synthesize :: forall ki phi codes ix
             . (IsNat ix)
-           => (forall iy . (IsNat iy) => Rep ki phi (Lkup iy codes) -> phi iy)
+           => (forall iy . (IsNat iy) => Rep ki phi (Lkup iy codes) -> phi iy) -- ^
            -> Fix ki codes ix
            -> AnnFix ki codes phi ix
 synthesize f = cata alg
@@ -83,3 +80,32 @@ synthesize f = cata alg
         -> AnnFix ki codes phi iy
     alg xs = AnnFix (f (mapRep getAnn xs)) xs
 
+
+-- |Monadic variant of 'synthesize'
+synthesizeM :: forall ki phi codes ix m
+              . (Monad m , IsNat ix)
+             => (forall iy  . IsNat iy => Rep ki phi (Lkup iy codes) -> m (phi iy)) -- ^
+             -> Fix ki codes ix
+             -> m (AnnFix ki codes phi ix)
+synthesizeM f = cataM alg
+  where
+    alg :: forall iy
+         . (IsNat iy)
+        => Rep ki (AnnFix ki codes phi) (Lkup iy codes)
+        -> m (AnnFix ki codes phi iy)
+    alg xs = flip AnnFix xs <$> f (mapRep getAnn xs)
+
+-- | Synthesized attributes with an algebra that has access to the annotations.
+synthesizeAnn :: forall ki codes chi phi ix
+               . (IsNat ix)
+              => (forall iy. chi iy -> Rep ki phi (Lkup iy codes) -> phi iy) -- ^
+              -> AnnFix ki codes chi ix
+              -> AnnFix ki codes phi ix
+synthesizeAnn f = annCata alg
+  where
+    alg :: forall iy
+         . chi iy
+        -> Rep ki (AnnFix ki codes phi) (Lkup iy codes)
+        -> AnnFix ki codes phi iy
+    alg ann rep = AnnFix (f ann (mapRep getAnn rep)) rep
+

src/Generics/MRSOP/Base.hs

@@ -6,7 +6,19 @@
 {-# LANGUAGE DataKinds            #-}
 {-# LANGUAGE PolyKinds            #-}
 {-# LANGUAGE ScopedTypeVariables  #-}
--- | Re-exports everything from under @Generics.MRSOP.Base@
+-- | Re-exports everything from under @Generics.MRSOP.Base@ and
+-- @Generics.MRSOP.Util@:
+--
+--  - "Generics.MRSOP.Base.NS"
+--  - "Generics.MRSOP.Base.NP"
+--  - "Generics.MRSOP.Base.Universe"
+--  - "Generics.MRSOP.Base.Class"
+--  - "Generics.MRSOP.Base.Metadata"
+--  - "Generics.MRSOP.Base.Combinators"
+--  - "Generics.MRSOP.Util"
+--
+-- For a lightweight example on how to use the library, please refer to "Generics.MRSOP.Examples.RoseTree"
+-- or to the full <https://victorcmiraldo.github.io/data/tyde2018_draft.pdf paper> for a more in-depth explanation 
 module Generics.MRSOP.Base (module Export) where
 
 import Generics.MRSOP.Base.NS          as Export

src/Generics/MRSOP/Base/Universe.hs

@@ -64,7 +64,7 @@ instance (TestEquality ki) => TestEquality (NA ki phi) where
   testEquality (NA_I _) (NA_K _) = Nothing
   testEquality (NA_K _) (NA_I _) = Nothing
   testEquality (NA_I i) (NA_I i') =
-    case testEquality (sNatFixIdx i) (sNatFixIdx i') of
+    case testEquality (snatFixIdx i) (snatFixIdx i') of
       Just Refl -> Just Refl
       Nothing -> Nothing
   testEquality (NA_K k) (NA_K k') =
@@ -292,17 +292,25 @@ instance EqHO ki => Eq (Fix ki codes ix) where
 
 -- | Catamorphism over fixpoints
 cata :: (IsNat ix)
-  => (forall iy. IsNat iy => Rep ki phi (Lkup iy codes) -> phi iy)
+  => (forall iy. IsNat iy => Rep ki phi (Lkup iy codes) -> phi iy) -- ^ 
   -> Fix ki codes ix
   -> phi ix
 cata f (Fix x) = f (mapRep (cata f) x)
 
+-- |Monadic variant
+cataM :: (Monad m , IsNat ix)
+      => (forall iy  . IsNat iy => Rep ki phi (Lkup iy codes) -> m (phi iy)) -- ^
+      -> Fix ki codes ix
+      -> m (phi ix)
+cataM f (Fix x) = mapRepM (cataM f) x >>= f
+
 -- |Retrieves the index of a 'Fix'
 proxyFixIdx :: phi ix -> Proxy ix
 proxyFixIdx _ = Proxy
 
-sNatFixIdx :: IsNat ix => phi ix -> SNat ix
-sNatFixIdx x = getSNat (proxyFixIdx x)
+-- |Retrieves the index of a 'Fix' as a singleton.
+snatFixIdx :: IsNat ix => phi ix -> SNat ix
+snatFixIdx x = getSNat (proxyFixIdx x)
 
 -- |Maps over the values of opaque types within the
 --  fixpoint.

src/Generics/MRSOP/Examples/LambdaAlphaEqTH.hs

@@ -10,6 +10,7 @@
 {-# LANGUAGE GADTs                 #-}
 {-# LANGUAGE TypeApplications      #-}
 {-# LANGUAGE PatternSynonyms       #-}
+{-# OPTIONS_HADDOCK hide, prune, ignore-exports #-}
 {-# OPTIONS_GHC -Wno-missing-pattern-synonym-signatures #-}
 {-# OPTIONS_GHC -Wno-missing-signatures                 #-}
 {-# OPTIONS_GHC -Wno-incomplete-patterns                #-}

src/Generics/MRSOP/Examples/RoseTree.hs

@@ -13,17 +13,37 @@
 {-# OPTIONS_GHC -Wno-missing-pattern-synonym-signatures #-}
 {-# OPTIONS_GHC -Wno-incomplete-patterns                #-}
 {-# OPTIONS_GHC -Wno-orphans                            #-}
+{-# OPTIONS_GHC -Wno-unused-top-binds                   #-}
 -- |This module is analogous to 'Generics.MRSOP.Examples.RoseTreeTH',
 --  but we use no Template Haskell here.
-module Generics.MRSOP.Examples.RoseTree where
+module Generics.MRSOP.Examples.RoseTree (
+  -- * Non-standard Rose-Tree datatype
+  -- $exp01
+    R
+  -- ** Family Structure
+  -- $exp02
+  , ListCode,RTCode,CodesRose,FamRose
+
+  -- ** 'Family' Instance
+  -- $exp03
+
+  -- * Generic Combinators
+  -- $exp04
+  , testEq , normalize , sumTree 
+  ) where
 
 import Data.Function (on)
 
 import Generics.MRSOP.Base
 import Generics.MRSOP.Opaque
 
--- * Standard Rose-Tree datatype
 
+-- $exp01
+--
+-- Suppose we we have a mutually recursive family
+-- consisting of RoseTree's with some redundant constructor:
+
+-- | Non-standard Rose-tree datatype.
 data R a = a :>: [R a]
          | Leaf a
          deriving Show
@@ -33,16 +53,56 @@ value1 = 1 :>: [2 :>: [], 3 :>: []]
 value2 = 1 :>: [2 :>: [] , Leaf 12]
 value3 = 3 :>: [Leaf 23 , value1 , value2]
 
--- ** Family Structure
 
+-- $exp02
+--
+-- The @R Int@ family has many components, that must be encoded in
+-- the generics-mrsop format. These are:
+
+-- |Codes for the @[R Int]@ type.
 type ListCode = '[ '[] , '[ 'I ('S 'Z) , 'I 'Z] ]
+
+-- |Codes for the @R Int@ type
 type RTCode   = '[ '[ 'K 'KInt , 'I 'Z] , '[ 'K 'KInt] ]
 
+-- |All codes packed in a type-level list
 type CodesRose = '[ListCode , RTCode]
+
+-- |The types corresponding the the codes in 'CodesRose'
+-- appear in the same order.
 type FamRose   = '[ [R Int] , R Int] 
 
 -- ** Instance Decl
 
+-- $exp03
+--
+-- Which in turn, allows us to write the 'Family' instance for
+-- @R Int@. The @instance Family Singl FamRose CodesRose@ states that
+-- the types in 'FamRose' follow the codes in 'CodesRose' with
+-- its opaque parts represented by 'Singl' Check the source code for more details
+-- on the instance.
+--
+-- It is worth mentioning that 'Generics.MRSOP.TH.deriveFamily' will derive
+-- this code automatically.
+--
+-- >instance Family Singl FamRose CodesRose where
+-- >   sfrom' (SS SZ) (El (a :>: as)) = Rep $ Here (NA_K (SInt a) :* NA_I (El as) :* NP0)
+-- >   sfrom' (SS SZ) (El (Leaf a))   = Rep $ There (Here (NA_K (SInt a) :* NP0))
+-- >   sfrom' SZ (El [])              = Rep $ Here NP0
+-- >   sfrom' SZ (El (x:xs))          = Rep $ There (Here (NA_I (El x) :* NA_I (El xs) :* NP0))
+-- >   sfrom' _ _ = error "unreachable"
+-- > 
+-- >   sto' SZ (Rep (Here NP0))
+-- >     = El []
+-- >   sto' SZ (Rep (There (Here (NA_I (El x) :* NA_I (El xs) :* NP0))))
+-- >     = El (x : xs)
+-- >   sto' (SS SZ) (Rep (Here (NA_K (SInt a) :* NA_I (El as) :* NP0)))
+-- >     = El (a :>: as)
+-- >   sto' (SS SZ) (Rep (There (Here (NA_K (SInt a) :* NP0))))
+-- >     = El (Leaf a)
+-- >   sto' _ _ = error "unreachable"
+
+
 instance Family Singl FamRose CodesRose where
   sfrom' (SS SZ) (El (a :>: as)) = Rep $ Here (NA_K (SInt a) :* NA_I (El as) :* NP0)
   sfrom' (SS SZ) (El (Leaf a))   = Rep $ There (Here (NA_K (SInt a) :* NP0))
@@ -74,28 +134,56 @@ instance HasDatatypeInfo Singl FamRose CodesRose where
   datatypeInfo _ _
     = error "unreachable"
 
--- * Eq Instance
+-- $exp04
+--
+-- Next, we showcase some of the simpler generic combinators provided
+-- out of the box with /generics-mrsop/
 
 instance Eq (R Int) where
   (==) = geq eqSingl `on` (into @FamRose)
 
+-- |We can use generic equality out of the box:
+--
+-- > instance Eq (R Int) where
+-- >   (==) = geq eqSingl `on` (into @FamRose)
+--
+-- If we run 'testEq' it must return @True@, naturally.
 testEq :: Bool
 testEq = value1 == value1
       && value2 /= value1
 
--- * Compos test
 
 pattern RInt_ = SS SZ
 
+-- |Here is an example of 'compos'; used to substitute the redundant 'Leaf'
+-- constructor by its standard rose tree representation.
+--
+-- > normalize :: R Int -> R Int
+-- > normalize = unEl . go (SS SZ) . into
+-- >   where
+-- >     go :: forall iy. (IsNat iy) => SNat iy -> El FamRose iy -> El FamRose iy
+-- >     go (SS SZ) (El (Leaf a)) = El (a :>: []) -- (SS SZ) is the index of 'R Int' in 'CodesRose'
+-- >     go _       x             = compos go x
+--
+-- Then, for example,
+-- 
+-- > normalize (42 :>: [Leaf 10 , 15 :>: [Leaf 20]]) == 42 :>: [10 :>: [] , 15 :>: [20 :>: []]]
+--
 normalize :: R Int -> R Int
 normalize = unEl . go (SS SZ) . into
   where
     go :: forall iy. (IsNat iy) => SNat iy -> El FamRose iy -> El FamRose iy
     go RInt_ (El (Leaf a)) = El (a :>: [])
     go _       x           = compos go x
 
--- * Crush test
-
+-- |Another generic combinator is 'crush'. We can 'crush' a rose tree and compute the sum
+-- of all the ints stored within said tree.
+--
+-- > sumTree :: R Int -> Int
+-- > sumTree = crush k sum . (into @FamRose)
+-- >   where k :: Singl x -> Int
+-- >         k (SInt n) = n
+--
 sumTree :: R Int -> Int
 sumTree = crush k sum . (into @FamRose)
   where k :: Singl x -> Int

src/Generics/MRSOP/Examples/RoseTreeTH.hs

@@ -12,6 +12,7 @@
 {-# LANGUAGE TemplateHaskell         #-}
 {-# LANGUAGE LambdaCase              #-}
 {-# LANGUAGE PatternSynonyms         #-}
+{-# OPTIONS_HADDOCK hide, prune, ignore-exports #-}
 {-# OPTIONS_GHC -Wno-missing-pattern-synonym-signatures #-}
 {-# OPTIONS_GHC -Wno-missing-signatures                 #-}
 {-# OPTIONS_GHC -Wno-incomplete-patterns                #-}