Hello everyone. I have some experiments in haskell with first-class-families. This is small example
type Base :: Type -> (Type -> Type)
type family Base t
data Embed :: Base a a -> Exp a
data Project :: a -> Exp (Base a a)
type Algebra f a = f a -> Exp a
type GAlgebra w f a = f (w a) -> Exp a
type PAlgebra f a = GAlgebra ((,) f) (Base f) a
type CoAlgebra f a = a -> Exp (f a)
type GCoalgebra m f a = a -> Exp (f (m a))
type AAlgebra f a = GCoalgebra (Either f) (Base f) a
data Cata :: Algebra (Base t) a -> t -> Exp a
type instance Eval (Cata alg x) = alg @@ Eval (Map (Cata alg) (Project @@ x))
data ListF a b = ConsF a b | NilF
type instance Base [a] = ListF a
type instance Eval (Map f 'NilF) = 'NilF
type instance Eval (Map f ('ConsF a b)) = 'ConsF a (f @@ b)
$(pure [])
type instance Eval (Project '[]) = 'NilF
type instance Eval (Project (x ': xs)) = ('ConsF x xs)
type instance Eval (Embed 'NilF) = '[]
type instance Eval (Embed ('ConsF x xs)) = x ': xs
data LengthAlg :: Algebra (ListF a) Nat
type instance Eval (LengthAlg 'NilF) = 0
type instance Eval (LengthAlg ('ConsF a b)) = 1 TL.+ b
data Length :: [a] -> Exp Nat
type instance Eval (Length as) = Cata LengthAlg @@ as
-- >>> :kind! Length @@ '[1,2,3,4,5,6,7]
-- Length @@ '[1,2,3,4,5,6,7] :: Nat
-- = 7
But now I don’t understand how I can port it to purescript with purescript-typelevel-eval.
Thx