Skip to content

Instantly share code, notes, and snippets.

@Icelandjack
Created August 13, 2021 21:14
Show Gist options
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save Icelandjack/14a61386721a156d22fa74bc47b8c722 to your computer and use it in GitHub Desktop.
Save Icelandjack/14a61386721a156d22fa74bc47b8c722 to your computer and use it in GitHub Desktop.
Simplify and Distribute GHC.Generics
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
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment