Simplify and Distribute GHC.Generics

Generics_Distr.hs

norm :: Generic1 f => Summs (Rep1 f) => f ~> Summ (Rep1 f) Zero
norm as = summs (from1 as) (Proxy @Zero)

class Summs rep where
 type Summ rep (end :: Type -> Type) :: Type -> Type

 summs :: rep a -> Proxy end -> Summ rep end a
 skips :: Proxy rep -> end a -> Summ rep end a

instance Summs Zero where
 type Summ Zero end = end
 summs :: Zero a -> Proxy end -> end a
 summs = \case

 skips :: Proxy Zero -> end a -> end a
 skips Proxy = id

instance (Summs rep, Summs rep1) => Summs (rep :+: rep1) where
 type Summ (rep :+: rep1) end = Summ rep (Summ rep1 end)

 summs :: forall a end. (rep :+: rep1) a -> Proxy end -> Summ rep (Summ rep1 end) a
 summs (L1 as) Proxy = summs as (Proxy @(Summ rep1 end))
 summs (R1 bs) end   = skips (Proxy @rep) (summs bs end)

 skips :: Proxy (rep :+: rep1) -> end a -> Summ rep (Summ rep1 end) a
 skips Proxy end = skips (Proxy @rep) (skips (Proxy @rep1) end)

instance Summs rep => Summs (D1 meta rep) where
 type Summ (D1 meta rep) end = Summ rep end
 summs :: D1 meta rep a -> Proxy end -> Summ rep end a
 summs (M1 as) end = summs as end

 skips :: Proxy (D1 meta rep) -> end a -> Summ rep end a
 skips Proxy end = skips (Proxy @rep) end

instance Prods rep => Summs (C1 meta rep) where
 type Summ (C1 meta rep) end = Prod rep One :+: end

 summs :: C1 meta rep a -> Proxy end -> (Prod rep One :+: end) a
 summs (M1 as) Proxy = L1 (prods as U1)

 skips :: Proxy (C1 meta rep) -> end a -> (Prod rep One :+: end) a
 skips Proxy = R1

class Prods rep where
 type Prod rep (end :: Type -> Type) :: Type -> Type
 prods :: rep a -> end a -> Prod rep end a

instance (Prods rep, Prods rep1) => Prods (rep :*: rep1) where
 type Prod (rep :*: rep1) end = Prod rep (Prod rep1 end)

 prods :: (rep :*: rep1) a -> end a -> Prod rep (Prod rep1 end) a
 prods (as :*: bs) = prods as . prods bs

instance Prods U1 where
 type Prod U1 end = end

 prods :: U1 a -> end a -> end a
 prods U1 xs = xs

instance Prods (S1 meta rep) where
 type Prod (S1 meta rep) end = rep :*: end

 prods :: S1 meta rep a -> end a -> (rep :*: end) a
 prods (M1 as) end = as :*: end

--

data ATOM a = IN a | SUM (ATOM a) (ATOM a)

type SUM  = []
type PROD = []

flatSOP :: SUM (PROD (ATOM a)) -> SUM (PROD a)
flatSOP []          = []
flatSOP (prod:sums) = flatP prod ++ flatSOP sums

flatP :: PROD (ATOM a) -> SUM (PROD a)
flatP              [] = pure []
flatP    (IN a:prods) = [ a:as | as <- flatP prods ]
flatP (SUM f g:prods) = flatP (f:prods) ++ flatP (g:prods)

class DistribSumms (rep :: k -> Type) where
 type DistribSumm (rep :: k -> Type) :: (k -> Type)

 distribSumms :: rep ~> DistribSumm rep

instance DistribSumms Zero where
 type DistribSumm Zero = Zero
 distribSumms :: Zero ~> Zero
 distribSumms = id

-- flatP :: PROD (ATOM a) -> SUM (PROD a)
-- flatSOP (prod:sums) = flatP prod ++ flatSOP sums
instance (ConcatC (DistribProd (DistribProdsF rep) rep) (DistribSumm rep1), DistribProds (DistribProdsF rep) rep, DistribSumms rep1) => DistribSumms (rep :+: rep1) where
 type DistribSumm (rep :+: rep1) = ConcatCF (DistribProd (DistribProdsF rep) rep) (DistribSumm rep1)

 distribSumms :: rep :+: rep1 ~> ConcatCF (DistribProd (DistribProdsF rep) rep) (DistribSumm rep1)
 distribSumms (L1 as) = concatCL1 @(DistribProd (DistribProdsF rep) rep) @(DistribSumm rep1) (distribProds as)
 distribSumms (R1 bs) = concatCR1 @(DistribProd (DistribProdsF rep) rep) @(DistribSumm rep1) (distribSumms bs)

class ConcatC as bs where
 type ConcatCF as bs :: Type -> Type

 concatCL1 :: as ~> ConcatCF as bs
 concatCR1 :: bs ~> ConcatCF as bs

instance ConcatC Zero end where
 type ConcatCF Zero end = end
 concatCL1 :: Zero ~> end
 concatCL1 = \case

 concatCR1 :: end ~> end
 concatCR1 = id

instance ConcatC fs end => ConcatC (f :+: fs) end where
 type ConcatCF (f :+: fs) end = f :+: ConcatCF fs end
 concatCL1 :: (f :+: fs) ~> (f :+: ConcatCF fs end)
 concatCL1 (L1 as) = L1 as

 concatCR1 :: end ~> (f :+: ConcatCF fs end)
 concatCR1 end = R1 (concatCR1 @fs end)

--

class MapCons f as where
 type MapConsF f as :: Type -> Type
 mapCons :: f a -> as a -> MapConsF f as a

instance MapCons f Zero where
 type MapConsF f Zero = Zero
 mapCons :: f a -> Zero a -> Zero a
 mapCons as = id

instance
  MapCons f bs
 =>
  MapCons f (as :+: bs)
 where
  type MapConsF f (as :+: bs) = (f :*: as) :+: MapConsF f bs
  mapCons :: f a -> (as :+: bs) a -> ((f :*: as) :+: MapConsF f bs) a
  mapCons fs = \case
   L1 as -> L1 (fs :*: as)
   R1 bs -> R1 (mapCons fs bs)

-- flatP :: PROD (ATOM a) -> SUM (PROD a)
-- flatP              [] = pure []
-- flatP    (IN a:prods) = [ a:as | as <- flatP prods ]
-- flatP (SUM f g:prods) = flatP (f:prods) ++ flatP (g:prods)

type family
 DistribProdsF as where
 DistribProdsF One       = DistribProdsOne
 DistribProdsF (Rec1 (f :+: g) :*: rep1) = DistribProdsProd2
 DistribProdsF (f :*: g) = DistribProdsProd

data DistribProdsTag = DistribProdsOne | DistribProdsProd | DistribProdsProd2

class tag ~ DistribProdsF rep => DistribProds tag rep where
 type DistribProd tag rep :: Type -> Type
 distribProds :: rep ~> DistribProd tag rep

instance DistribProds DistribProdsOne One where
 type DistribProd DistribProdsOne One = One :+: Zero

 distribProds :: One ~> One :+: Zero
 distribProds U1 = L1 U1

instance (DistribProdsF (rep :*: rep1) ~ DistribProdsProd, MapCons rep (DistribProd (DistribProdsF rep1) rep1), DistribProds (DistribProdsF rep1) rep1) => DistribProds DistribProdsProd (rep :*: rep1) where
 type DistribProd DistribProdsProd (rep :*: rep1) = MapConsF rep (DistribProd (DistribProdsF rep1) rep1)

 distribProds :: rep :*: rep1 ~> MapConsF rep (DistribProd (DistribProdsF rep1) rep1)
 distribProds (as :*: bs) = mapCons @rep @(DistribProd (DistribProdsF rep1) rep1) as (distribProds bs)

-- flatP :: PROD (ATOM a) -> SUM (PROD a)
-- flatP (SUM f g:prods) = flatP (f:prods) ++ flatP (g:prods)
instance
 ( ConcatC
     (DistribProd (DistribProdsF (Rec1 f :*: rep)) (Rec1 f :*: rep))
     (DistribProd (DistribProdsF (Rec1 g :*: rep)) (Rec1 g :*: rep))
 , DistribProds (DistribProdsF (Rec1 f :*: rep)) (Rec1 f :*: rep)
 , DistribProds (DistribProdsF (Rec1 g :*: rep)) (Rec1 g :*: rep)
 )
  =>
  DistribProds DistribProdsProd2 ((Rec1 (f :+: g)) :*: rep)
 where
  type DistribProd DistribProdsProd2 ((Rec1 (f :+: g)) :*: rep) =
    DistribProd (DistribProdsF (Rec1 f :*: rep)) (Rec1 f :*: rep)
      `ConcatCF`
    DistribProd (DistribProdsF (Rec1 g :*: rep)) (Rec1 g :*: rep)

  distribProds :: (Rec1 (f :+: g) :*: rep)
               ~> (DistribProd (DistribProdsF (Rec1 f :*: rep)) (Rec1 f :*: rep)
                    `ConcatCF`
                   DistribProd (DistribProdsF (Rec1 g :*: rep)) (Rec1 g :*: rep))
  distribProds (Rec1 (L1 as) :*: end) = concatCL1
   @(DistribProd (DistribProdsF (Rec1 f :*: rep)) (Rec1 f :*: rep))
   @(DistribProd (DistribProdsF (Rec1 g :*: rep)) (Rec1 g :*: rep))
   (distribProds @_ @(Rec1 f :*: rep) (Rec1 as :*: end))
  distribProds (Rec1 (R1 bs) :*: end) = concatCR1
   @(DistribProd (DistribProdsF (Rec1 f :*: rep)) (Rec1 f :*: rep))
   @(DistribProd (DistribProdsF (Rec1 g :*: rep)) (Rec1 g :*: rep))
   (distribProds @_ @(Rec1 g :*: rep) (Rec1 bs :*: end))

data T a = T a a a deriving Generic1

--    norm @T @Int
-- :: T ~> ((Id * Id * Id * One) + Zero)
-- :: T ~> '['[Id,Id,Id]]

--    norm @T >>> distribSumms
-- :: T ~> (:+:) ((Id :*: Id :*: Id :*: One) :+: Zero) :+: Zero

--    norm @T >>> distribSumms
-- :: T ~> (Id :*: Id :*: Id :*: One) :+: Zero
data Fr f a = Fr (f a) deriving Generic1

--    norm @(Fr [])
-- :: Fr [] ~> (Rec1 [] :*: One) :+: Zero
--
--    norm @(Fr []) >>> distribSumms
-- :: Fr [] ~> (Rec1 [] :*: One) :+: Zero

--    norm @(Fr (Par1 :+: Par1)) >>> distribSumms
-- :: Fr (Id:+:Id) ~> (Rec1 Id :*: One) :+: (Rec1 Id :*: One) :+: Zero