Generics.MRSOP.Examples.RoseTree

This module is analogous to RoseTreeTH, but we use no Template Haskell here.

Non-standard Rose-Tree datatype

Suppose we we have a mutually recursive family consisting of RoseTree's with some redundant constructor:

data R a

Non-standard Rose-tree datatype.

Instances

Family Singl FamRose CodesRose

Defined in Generics.MRSOP.Examples.RoseTree

Methods

sfrom' :: SNat ix -> El FamRose ix -> Rep Singl (El FamRose) (Lkup ix CodesRose)

sto' :: SNat ix -> Rep Singl (El FamRose) (Lkup ix CodesRose) -> El FamRose ix

HasDatatypeInfo Singl FamRose CodesRose

Defined in Generics.MRSOP.Examples.RoseTree

Methods

datatypeInfo :: Proxy FamRose -> SNat ix -> DatatypeInfo (Lkup ix CodesRose)

Eq (R Int)

Defined in Generics.MRSOP.Examples.RoseTree

Methods

(==) :: R Int -> R Int -> Bool

(/=) :: R Int -> R Int -> Bool

Show a => Show (R a)

Defined in Generics.MRSOP.Examples.RoseTree

Methods

showsPrec :: Int -> R a -> ShowS

show :: R a -> String

showList :: [R a] -> ShowS

Family Structure

The R Int family has many components, that must be encoded in the generics-mrsop format. These are:

type ListCode = '['[], '[I (S Z), I Z]]

Codes for the [R Int] type.

type RTCode = '['[K KInt, I Z], '[K KInt]]

Codes for the R Int type

type CodesRose = '[ListCode, RTCode]

All codes packed in a type-level list

type FamRose = '[[R Int], R Int]

The types corresponding the the codes in CodesRose appear in the same order.

Family Instance

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 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) :* Nil)
   sfrom' (SS SZ) (El (Leaf a))   = Rep $ There (Here (NA_K (SInt a) :* Nil))
   sfrom' SZ (El [])              = Rep $ Here Nil
   sfrom' SZ (El (x:xs))          = Rep $ There (Here (NA_I (El x) :* NA_I (El xs) :* Nil))
   sfrom' _ _ = error "unreachable"
 
   sto' SZ (Rep (Here Nil))
     = El []
   sto' SZ (Rep (There (Here (NA_I (El x) :* NA_I (El xs) :* Nil))))
     = El (x : xs)
   sto' (SS SZ) (Rep (Here (NA_K (SInt a) :* NA_I (El as) :* Nil)))
     = El (a :>: as)
   sto' (SS SZ) (Rep (There (Here (NA_K (SInt a) :* Nil))))
     = El (Leaf a)
   sto' _ _ = error "unreachable"

Generic Combinators

Next, we showcase some of the simpler generic combinators provided out of the box with generics-mrsop

testEq :: Bool

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.

normalize :: R Int -> R Int

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 :>: []]]

sumTree :: R Int -> Int

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

Orphan instances

Family Singl FamRose CodesRose

Methods

sfrom' :: SNat ix -> El FamRose ix -> Rep Singl (El FamRose) (Lkup ix CodesRose)

sto' :: SNat ix -> Rep Singl (El FamRose) (Lkup ix CodesRose) -> El FamRose ix