Generics.MRSOP.TH

Provides a simple way for the end-user to derive the Family instance for a mutually recursive family.

Let's take a simple example:

data Rose a = a :>: [Rose a] | Leaf a
deriveFamily [t| Rose Int |]

Will derive the following code:

type FamRoseInt   = '[Rose Int, [Rose Int]]
type CodesRoseInt = '['['[K KInt, I (S Z)], '[K KInt]], '['[], '[I Z, I (S Z)]]]

-- Type index SNat synonyms
pattern IdxRoseInt     = SZ
pattern IdxListRoseInt = SS SZ

-- (:>:) pattern syn
pattern RoseInt_Ifx0 :: kon KInt -> phi (S Z) -> View kon phi (Lkup Z CodesRoseInt)
pattern RoseInt_Ifx0 p q = Tag CZ (NA_K p :* (NA_I q :* Nil))

-- Leaf pattern syn
pattern RoseIntLeaf_ :: kon KInt -> View kon phi (Lkup Z CodesRoseInt)
pattern RoseIntLeaf_ p = Tag (CS CZ) (NA_K p :* Nil)

-- [] pattern syn
pattern ListRoseInt_Ifx0 :: View kon phi (Lkup (S Z) CodesRoseInt)
pattern ListRoseInt_Ifx0 = Tag CZ Nil

-- (:) pattern syn
pattern ListRoseInt_Ifx1 :: phi Z -> phi (S Z) -> View kon phi (Lkup (S Z) CodesRoseInt)
pattern ListRoseInt_Ifx1 p q = Tag (CS CZ) (NA_I p :* (NA_I q :* Nil))

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"

instance HasDatatypeInfo Singl FamRose CodesRose where
  datatypeInfo _ SZ
    = ADT "module" (Name "[]" :@: (Name "R" :@: Name "Int"))
      $  (Constructor "[]")
      :* (Infix ":" RightAssociative 5)
      :* Nil
  datatypeInfo _ (SS SZ)
    = ADT "module" (Name "R" :@: Name "Int")
      $  (Infix ":>:" NotAssociative 0)
      :* (Constructor "Leaf")
      :* Nil
  datatypeInfo _ _
    = error "unreachable"

To illustrate the pattern synonym generation, let us look at a selection of a more involved example

Consider the following family:

data Stmt var
  = SAssign var (Exp var)
  | SIf     (Exp var) (Stmt var) (Stmt var)
  | SSeq    (Stmt var) (Stmt var)
  | SReturn (Exp var)
  | SDecl (Decl var)
  | SSkip
  deriving Show

data Decl var
  = DVar var
  | DFun var var (Stmt var)
  deriving Show

data Exp var
  = EVar  var
  | ECall var (Exp var)
  | EAdd (Exp var) (Exp var)
  | ESub (Exp var) (Exp var)
  | ELit Int
  deriving Show

In this case, running deriveFamily [t| Stmt String |] will generate the following types:

type FamStmtString   = '[Stmt String, Exp String, Decl String]
type CodesStmtString =
    '['['[K KString, I (S Z)],
        '[I (S Z), I Z, I Z],
        '[I Z, I Z],
        '[I (S Z)],
        '[I (S (S Z))],
        '[]],
      '['[K KString],
        '[K KString, I (S Z)],
        '[I (S Z), I (S Z)],
        '[I (S Z), I (S Z)],
        '[K KInt]],
      '['[K KString], '[K KString, K KString, I Z]]]
pattern IdxStmtString = SZ
pattern IdxExpString = SS SZ
pattern IdxDeclString = SS (SS SZ)

-- Here are the declared patterns for 'View'
pattern StmtStringSAssign_ 
pattern StmtStringSIf_ 
pattern StmtStringSSeq_ 
pattern StmtStringSReturn_ 
pattern StmtStringSDecl_ 
pattern StmtStringSSkip_ 
pattern ExpStringEVar_ 
pattern ExpStringECall_ 
pattern ExpStringEAdd_ 
pattern ExpStringESub_ 
pattern ExpStringELit_ 
pattern DeclStringDVar_ 
pattern DeclStringDFun_ 

We did ommit the definitions and Family and HasDatatypeInfo instances for brevity here. If you want to see the actual generated code, compile with

stack build ghc-options="-ddump-splices -ddump-to-file"

You can find the spliced files with

find -name "*.dump-splices"

This module was based in the TH generication from generic-sop ( https://hackage.haskell.org/package/generics-sop-0.3.2.0/docs/src/Generics-SOP-TH.html )

Documentation

deriveFamilyWith :: Name -> Q Type -> Q [Dec]

Given the name of the first element in the family, derives:

1. The other types in the family and opaque types one needs.
2. the SOP code for each of the datatypes involved
3. The Family instance
4. Metadada information for each of the datatypes involved
5. Uses the opaque-type universe provided.

deriveFamilyWithTy :: Q Type -> Q Type -> Q [Dec]

Reifies the type given for opaque types, then calls deriveFamilyWith

deriveFamily :: Q Type -> Q [Dec]

Same as deriveFamilyWith ''Singl

genFamilyDebug :: STy -> [(STy, Int, DTI IK)] -> Q [Dec]

Generates a bunch of strings for debug purposes. The generated strings are named tyInfo_0, tyInfo_1, ...