Copyright	(c) gspia 2020-
License	BSD
Maintainer	gspia
Safe Haskell	Safe
Language	Haskell2010

Fcf.Alg.Morphism

Description

Fcf.Alg.Morphism

Type-level Cata and Ana can be used to do complex computation that live only on type-level or on compile-time. As an example, see the sorting algorithm in Fcf.Alg.Tree -module.

This module also provides some other type-level functions that probably will find other place after a while. E.g. First and Second and their instances on Either and tuple.

Synopsis

data Fix f = Fix (f (Fix f))
type Algebra f a = f a -> Exp a
type CoAlgebra f a = a -> Exp (f a)
data Cata :: Algebra f a -> Fix f -> Exp a
data Ana :: CoAlgebra f a -> a -> Exp (Fix f)
data Hylo :: Algebra f a -> CoAlgebra f b -> b -> Exp a
data First :: (a -> Exp b) -> f a c -> Exp (f b c)
data Second :: (c -> Exp d) -> f a c -> Exp (f a d)

Documentation

>>> import qualified GHC.TypeLits as TL
>>> import           Fcf.Alg.List
>>> import           Fcf.Data.Nat

data Fix f Source #

Structure that Cata can fold and that is a result structure of Ana.

Constructors

Fix (f (Fix f))

Instances

type Eval (ListToFix (a2 ': as) :: Fix (ListF a1) -> Type) Source #
Instance details Defined in Fcf.Alg.List type Eval (ListToFix (a2 ': as) :: Fix (ListF a1) -> Type) = Fix (ConsF a2 (Eval (ListToFix as)))
type Eval (ListToFix ([] :: [a]) :: Fix (ListF a) -> Type) Source #
Instance details Defined in Fcf.Alg.List type Eval (ListToFix ([] :: [a]) :: Fix (ListF a) -> Type) = Fix (NilF :: ListF a (Fix (ListF a)))
type Eval (TreeToFix (Node a2 (b ': bs)) :: Fix (TreeF a1) -> Type) Source #
Instance details Defined in Fcf.Alg.Tree type Eval (TreeToFix (Node a2 (b ': bs)) :: Fix (TreeF a1) -> Type) = Fix (NodeF a2 (Eval (Map (TreeToFix :: Tree a1 -> Fix (TreeF a1) -> Type) (b ': bs))))
type Eval (TreeToFix (Node a2 ([] :: [Tree a1])) :: Fix (TreeF a1) -> Type) Source #
Instance details Defined in Fcf.Alg.Tree type Eval (TreeToFix (Node a2 ([] :: [Tree a1])) :: Fix (TreeF a1) -> Type) = Fix (NodeF a2 ([] :: [Fix (TreeF a1)]))
type Eval (Ana coalg a2 :: Fix f -> Type) Source #
Instance details Defined in Fcf.Alg.Morphism type Eval (Ana coalg a2 :: Fix f -> Type) = Fix (Eval (Map (Ana coalg) (Eval (coalg a2))))

type Algebra f a = f a -> Exp a Source #

Commonly used name describing the method Cata eats.

type CoAlgebra f a = a -> Exp (f a) Source #

Commonly used name describing the method Ana eats.

data Cata :: Algebra f a -> Fix f -> Exp a Source #

Write the function to give a Fix, and feed it in together with an Algebra.

Check Fcf.Alg.List to see example algebras in use.

Instances

type Eval (Cata alg (Fix b2) :: b1 -> Type) Source #
Instance details Defined in Fcf.Alg.Morphism type Eval (Cata alg (Fix b2) :: b1 -> Type) = alg @@ Eval (Map (Cata alg) b2)

data Ana :: CoAlgebra f a -> a -> Exp (Fix f) Source #

Ana can also be used to build a Fix structure.

Example

>>> data NToOneCoA :: CoAlgebra (ListF Nat) Nat
>>> :{
  type instance Eval (NToOneCoA b) = 
    If (Eval (b < 1) )
        'NilF
        ('ConsF b ( b TL.- 1))
:}

>>> :kind! Eval (Ana NToOneCoA 3)
Eval (Ana NToOneCoA 3) :: Fix (ListF Nat)
= 'Fix ('ConsF 3 ('Fix ('ConsF 2 ('Fix ('ConsF 1 ('Fix 'NilF))))))

Instances

type Eval (Ana coalg a2 :: Fix f -> Type) Source #
Instance details Defined in Fcf.Alg.Morphism type Eval (Ana coalg a2 :: Fix f -> Type) = Fix (Eval (Map (Ana coalg) (Eval (coalg a2))))

data Hylo :: Algebra f a -> CoAlgebra f b -> b -> Exp a Source #

Hylomorphism uses first Ana to build a structure (unfold) and then Cata to process the structure (fold).

Example

>>> data NToOneCoA :: CoAlgebra (ListF Nat) Nat
>>> :{
  type instance Eval (NToOneCoA b) = 
    If (Eval (b < 1) )
        'NilF
        ('ConsF b ( b TL.- 1))
:}

>>> :kind! Eval (Hylo SumAlg NToOneCoA 5)
Eval (Hylo SumAlg NToOneCoA 5) :: Nat
= 15

Instances

type Eval (Hylo alg coalg a3 :: a2 -> Type) Source #
Instance details Defined in Fcf.Alg.Morphism type Eval (Hylo alg coalg a3 :: a2 -> Type) = Eval (Cata alg =<< Ana coalg a3)

data First :: (a -> Exp b) -> f a c -> Exp (f b c) Source #

Type-level First. Tuples (,) and Either have First-instances.

Example

>>> :kind! Eval (First ((+) 1) '(3,"a"))
Eval (First ((+) 1) '(3,"a")) :: (Nat, TL.Symbol)
= '(4, "a")

Instances

type Eval (First f (Right b3 :: Either a b2) :: Either b1 b2 -> Type) Source #
Instance details Defined in Fcf.Alg.Morphism type Eval (First f (Right b3 :: Either a b2) :: Either b1 b2 -> Type) = (Right b3 :: Either b1 b2)
type Eval (First f (Left a2 :: Either k c) :: Either a1 c -> Type) Source #
Instance details Defined in Fcf.Alg.Morphism type Eval (First f (Left a2 :: Either k c) :: Either a1 c -> Type) = (Left (f @@ a2) :: Either a1 c)
type Eval (First f ((,) a b) :: (k2, k3) -> Type) Source #
Instance details Defined in Fcf.Alg.Morphism type Eval (First f ((,) a b) :: (k2, k3) -> Type) = (,) (f @@ a) b

data Second :: (c -> Exp d) -> f a c -> Exp (f a d) Source #

Type-level Second. Tuples (,) and Either have Second-instances.

Example

>>> :kind! Eval (Second ((+) 1) '("a",3))
Eval (Second ((+) 1) '("a",3)) :: (TL.Symbol, Nat)
= '("a", 4)

Instances

type Eval (Second f (Right b2 :: Either a k) :: Either a b1 -> Type) Source #
Instance details Defined in Fcf.Alg.Morphism type Eval (Second f (Right b2 :: Either a k) :: Either a b1 -> Type) = (Right (f @@ b2) :: Either a b1)
type Eval (Second f (Left a2 :: Either a1 c) :: Either a1 d -> Type) Source #
Instance details Defined in Fcf.Alg.Morphism type Eval (Second f (Left a2 :: Either a1 c) :: Either a1 d -> Type) = (Left a2 :: Either a1 d)
type Eval (Second f ((,) a b) :: (k3, k2) -> Type) Source #
Instance details Defined in Fcf.Alg.Morphism type Eval (Second f ((,) a b) :: (k3, k2) -> Type) = (,) a (f @@ b)