Begin work using Template Haskell to automate Base functor generation.

It doesn't quite work yet, but it's a start. It'll need a rewrite to work, hence the commit.
Current known bugs:
* References to `r` do not take into account the skip pos.
* Generation of `forall r` even when r is not used.
* The `forall r` isn't placed where I want it to be.
* The code is horrifically bad.
* There are certainly other bugs I don't know about yet.

monoids-in-the-categoy-of-endofunctors.cabal

@@ -4,7 +4,7 @@ cabal-version: 2.2
 --
 -- see: https://github.com/sol/hpack
 --
--- hash: ccbe65df6ff8c44717a5cad0ce46e39a026a6e35f58b942545be94a2080cc645
+-- hash: 4d5299830f70602c840afe07491da0f469a43100f9e7c8ccb7452202fe810a77
 
 name:           monoids-in-the-categoy-of-endofunctors
 version:        0.1.0.0
@@ -31,6 +31,8 @@ library
       Category.Constraint
       Category.Functor
       Category.Functor.Foldable
+      Category.Functor.Foldable.TH
+      Category.Functor.Foldable.THT
       Data.Dict
       Data.Fin
       Data.Nat
@@ -41,7 +43,8 @@ library
   hs-source-dirs:
       src
   default-extensions: BlockArguments ConstraintKinds DataKinds DefaultSignatures FlexibleContexts FlexibleInstances FunctionalDependencies GADTs ImportQualifiedPost InstanceSigs LambdaCase MultiParamTypeClasses NoImplicitPrelude PolyKinds QuantifiedConstraints RankNTypes ScopedTypeVariables TypeApplications TypeFamilies TypeOperators
-  ghc-options: -Weverything -Wno-missing-export-lists -Wno-missing-import-lists -Wno-safe -Wno-missing-safe-haskell-mode
+  ghc-options: -Weverything -Wno-missing-export-lists -Wno-missing-import-lists -Wno-missing-safe-haskell-mode -Wno-safe -Wno-unsafe
   build-depends:
       base >=4.13 && <5
+    , template-haskell >=2.16 && <3
   default-language: Haskell2010

package.yaml

@@ -38,11 +38,13 @@ ghc-options:
 #- -Werror
 - -Wno-missing-export-lists
 - -Wno-missing-import-lists
-- -Wno-safe
 - -Wno-missing-safe-haskell-mode
+- -Wno-safe
+- -Wno-unsafe
 
 dependencies:
 - base >= 4.13 && < 5
+- template-haskell >= 2.16 && < 3
 
 library:
   source-dirs: src

src/Category/Functor/Foldable/TH.hs

@@ -0,0 +1,113 @@
+{-# LANGUAGE TemplateHaskell #-}
+module Category.Functor.Foldable.TH where
+
+import Data.Char (GeneralCategory (..), generalCategory)
+import Data.Maybe (fromMaybe, isNothing)
+import Language.Haskell.TH
+import Language.Haskell.TH.Syntax
+import Prelude
+
+-- Copied from recursion-schemes
+isPuncChar :: Char -> Bool
+isPuncChar c = c `elem` ",;()[]{}`"
+
+isSymbolChar :: Char -> Bool
+isSymbolChar c = not (isPuncChar c) && case generalCategory c of
+    MathSymbol              -> True
+    CurrencySymbol          -> True
+    ModifierSymbol          -> True
+    OtherSymbol             -> True
+    DashPunctuation         -> True
+    OtherPunctuation        -> c `notElem` "'\""
+    ConnectorPunctuation    -> c /= '_'
+    _                       -> False
+
+fName :: Name -> Name
+fName orig = mkName (f (nameBase orig))
+    where f name | isInfixName name = name ++ "$"
+                 | otherwise        = name ++ "F"
+
+          isInfixName :: String -> Bool
+          isInfixName = all isSymbolChar
+
+unBndr :: TyVarBndr -> Kind
+unBndr (KindedTV _ k) = k
+unBndr _ = error "Automatically generated variable binders should have kind annotations."
+
+-- | For a type `MyType (a :: i) (b :: j) :: k -> l -> Type`,
+-- create a base functor `MyTypeF (a :: i) (b :: j) (r :: k -> l -> Type) :: k -> l -> Type`
+-- such that `Fix (MyTypeF a b) c d` is isomorphic to `MyType a b c d`.
+makeBaseFunctor :: Name -> Int -> DecsQ
+makeBaseFunctor refName pos = do
+    -- The name for the variable for instances of recursion.
+    recName <- newName "r"
+    TyConI (DataD ctx origName varBndrs kind' origCons _) <- reify refName
+    let newN = fName origName
+    let actualVars = take pos varBndrs
+    let kind = if pos == length varBndrs && isNothing kind'
+        then Nothing
+        else Just (foldr (\ty tys -> AppT (AppT ArrowT (unBndr ty)) tys) (fromMaybe StarT kind') (drop pos varBndrs))
+    -- The kind of the recursive variable should be the same as the kind of the original data type.
+    -- Similarly, the kind of the new datatype is the same as the kind of the old.
+    let recBndr = maybe (KindedTV recName StarT) (KindedTV recName) kind
+    pure [DataD ctx newN (actualVars ++ [recBndr]) kind (map (ForallC [recBndr] [] . makeBaseConstructor (length varBndrs - pos) origName recName (concatMap conn origCons)) origCons) []]
+  where
+    conn :: Con -> [Name]
+    conn (NormalC n _) = [n]
+    conn (RecC n _) = [n]
+    conn (InfixC _ n _) = [n]
+    conn (ForallC _ _ con) = conn con
+    conn (GadtC ns _ _) = ns
+    conn (RecGadtC ns _ _) = ns
+
+    makeBaseType :: Name -> Name -> [Name] -> Type -> Type
+    makeBaseType orig recn conns = makeBaseType'
+      where
+        makeBaseType' (ForallT vars ctx ty) = ForallT vars (map makeBaseType' ctx) (makeBaseType' ty)
+        makeBaseType' (ForallVisT vars ty) = ForallVisT vars (makeBaseType' ty)
+        makeBaseType' (AppT t1 t2) = AppT (makeBaseType' t1) (makeBaseType' t2)
+        makeBaseType' (AppKindT ty kn) = AppKindT (makeBaseType' ty) (makeBaseType' kn)
+        makeBaseType' (SigT ty kn) = SigT (makeBaseType' ty) (makeBaseType' kn)
+        makeBaseType' (VarT name) = VarT name
+        makeBaseType' (ConT name)
+            | name == orig = VarT recn
+            | otherwise = ConT name
+        makeBaseType' (PromotedT name)
+            | name `elem` conns = PromotedT (fName name)
+            | otherwise = PromotedT name
+        makeBaseType' (InfixT ty1 name ty2) = InfixT (makeBaseType' ty1) name (makeBaseType' ty2)
+        makeBaseType' (UInfixT ty1 name ty2) = UInfixT (makeBaseType' ty1) name (makeBaseType' ty2)
+        makeBaseType' (ParensT ty) = ParensT (makeBaseType' ty)
+        makeBaseType' o@(TupleT _) = o
+        makeBaseType' o@(UnboxedTupleT _) = o
+        makeBaseType' o@(UnboxedSumT _) = o
+        makeBaseType' ArrowT = ArrowT
+        makeBaseType' EqualityT = EqualityT
+        makeBaseType' ListT = ListT
+        makeBaseType' o@(PromotedTupleT _) = o
+        makeBaseType' PromotedNilT = PromotedNilT
+        makeBaseType' PromotedConsT = PromotedConsT
+        makeBaseType' StarT = StarT
+        makeBaseType' ConstraintT = ConstraintT
+        makeBaseType' o@(LitT _) = o
+        makeBaseType' WildCardT = WildCardT
+        makeBaseType' (ImplicitParamT s ty) = ImplicitParamT s (makeBaseType' ty)
+
+    makeBaseBangType :: Name -> Name -> [Name] -> BangType -> BangType
+    makeBaseBangType orig recn conns (bng, ty) = (bng, makeBaseType orig recn conns ty)
+
+    makeBaseVarBangType :: Name -> Name -> [Name] -> VarBangType -> VarBangType
+    makeBaseVarBangType orig recn conns (var, bng, ty) = (fName var, bng, makeBaseType orig recn conns ty)
+
+    fixGadtTy :: Int -> Name -> Name -> [Name] -> Name -> Type -> Type
+    fixGadtTy 0   orig recn conns name o          = AppT (fixGadtTy (-1)      orig recn conns name o) (VarT recn)
+    fixGadtTy pos orig recn conns name (AppT a b) = AppT (fixGadtTy (pos - 1) orig recn conns name a) (makeBaseType orig recn conns b)
+    fixGadtTy _   _    _    _     name _          = ConT (fName name)
+
+    makeBaseConstructor :: Int -> Name -> Name -> [Name] -> Con -> Con
+    makeBaseConstructor pos orig recn conns (NormalC name tys) = NormalC (fName name) (map (makeBaseBangType orig recn conns) tys)
+    makeBaseConstructor pos orig recn conns (RecC name tys) = RecC (fName name) (map (makeBaseVarBangType orig recn conns) tys)
+    makeBaseConstructor pos orig recn conns (InfixC ty1 name ty2) = InfixC (makeBaseBangType orig recn conns ty1) (fName name) (makeBaseBangType orig recn conns ty2)
+    makeBaseConstructor pos orig recn conns (ForallC vars ctx con) = ForallC vars (map (makeBaseType orig recn conns) ctx) (makeBaseConstructor pos orig recn conns con)
+    makeBaseConstructor pos orig recn conns (GadtC names tys ty) = GadtC (map fName names) (map (makeBaseBangType orig recn conns) tys) (fixGadtTy pos orig recn conns orig ty)
+    makeBaseConstructor pos orig recn conns (RecGadtC names tys ty) = RecGadtC (map fName names) (map (makeBaseVarBangType orig recn conns) tys) (fixGadtTy pos orig recn conns orig ty)

src/Category/Functor/Foldable/THT.hs

@@ -0,0 +1,53 @@
+{-# LANGUAGE TemplateHaskell #-}
+module Category.Functor.Foldable.THT where
+
+import Category.Functor.Foldable.TH
+import Data.Kind (Type)
+
+import Category
+import Category.Functor.Foldable
+
+data N = Z | S N
+
+makeBaseFunctor ''N 0
+
+data Fin :: N -> Type where
+    FZ :: forall n. Fin ('S n)
+    FS :: forall n. Fin n -> Fin ('S n)
+
+makeBaseFunctor ''Fin 0
+type instance Base Fin = FinF
+
+instance Functor Fin where
+    type Dom Fin = (:~:)
+    type Cod Fin = (->)
+    map Refl x = x
+
+instance Functor (FinF r) where
+    type Dom (FinF r) = (:~:)
+    type Cod (FinF r) = (->)
+    map Refl x = x
+
+instance Functor FinF where
+    type Dom FinF = Nat (:~:) (->)
+    type Cod FinF = Nat (:~:) (->)
+    map :: forall f g. Nat (:~:) (->) f g -> Nat (:~:) (->) (FinF f) (FinF g)
+    map (Nat f) = Nat \_ -> \case
+        FZF -> FZF
+        (FSF r) -> FSF (f Refl r)
+
+instance Recursive Fin where
+    project = Nat \_ -> \case
+        FZ -> FZF
+        (FS r) -> FSF r
+
+instance Corecursive Fin where
+    embed = Nat \_ -> \case
+        FZF -> FZ
+        (FSF r) -> FS r
+
+data Vec a :: N -> Type where
+    VZ :: Vec a 'Z
+    VS :: a -> Vec a n -> Vec a ('S n)
+
+makeBaseFunctor ''Vec 0

src/Data/Fin.hs

@@ -2,12 +2,13 @@ module Data.Fin where
 
 import Category
 import Category.Functor.Foldable
+import Data.Kind (Type)
 import Data.Nat
 
-data Fin n where
+data Fin :: N -> Type where
     FZ :: Fin ('S n)
     FS :: Fin n -> Fin ('S n)
-data FinF r n where
+data FinF r :: N -> Type where
     FZF :: FinF r ('S n)
     FSF :: r n -> FinF r ('S n)
 type instance Base Fin = FinF

src/Data/Nat.hs

@@ -2,6 +2,7 @@ module Data.Nat where
 
 import Category
 import Category.Functor.Foldable
+import Category.Functor.Foldable.TH
 import Data.Kind (Type)
 import Data.Maybe (Maybe (Nothing, Just))
 import Quantifier

src/Data/Vec.hs

@@ -7,10 +7,10 @@ import Data.Kind (Type)
 import Data.Nat
 import Quantifier
 
-data Vec a n where
+data Vec a :: N -> Type where
     VZ :: Vec a 'Z
     VS :: a -> Vec a n -> Vec a ('S n)
-data VecF a r n where
+data VecF a r :: N -> Type where
     VZF :: VecF a r 'Z
     VSF :: a -> r n -> VecF a r ('S n)
 type instance Base (Vec a) = (VecF a)