Copyright | (c) gspia 2020- |
---|---|

License | BSD |

Maintainer | gspia |

Safe Haskell | Safe |

Language | Haskell2010 |

# 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`

## Instances

type Eval (ListToFix (a2 ': as) :: Fix (ListF a1) -> Type) Source # | |

type Eval (ListToFix ([] :: [a]) :: Fix (ListF a) -> Type) Source # | |

type Eval (TreeToFix (Node a2 (b ': bs)) :: Fix (TreeF a1) -> Type) Source # | |

type Eval (TreeToFix (Node a2 ([] :: [Tree a1])) :: Fix (TreeF a1) -> Type) Source # | |

type Eval (Ana coalg a2 :: Fix f -> Type) Source # | |

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)) :}`:{`

`>>>`

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

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)) :}`:{`

`>>>`

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

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

Type-level First. Tuples `(,)`

and `Either`

have First-instances.

**Example**

`>>>`

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

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

Type-level Second. Tuples `(,)`

and `Either`

have Second-instances.

**Example**

`>>>`

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