fcf-containers-0.4.0: Data structures and algorithms for first-class-families

Copyright(c) gspia 2020-
LicenseBSD
Maintainergspia
Safe HaskellSafe
LanguageHaskell2010

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

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 (FibAlgebra (Succ (Fix (AnnF ((,) (Succ (Fix (AnnF ((,) _ n)))) m)))) :: Nat -> Type) Source # 
Instance details

Defined in Fcf.Alg.Tree

type Eval (FibAlgebra (Succ (Fix (AnnF ((,) (Succ (Fix (AnnF ((,) _ n)))) m)))) :: Nat -> Type) = Eval (n + m)
type Eval (FibAlgebra (Succ (Fix (AnnF ((,) (Zero :: NatF (Fix (AnnF NatF Nat))) _)))) :: Nat -> Type) Source # 
Instance details

Defined in Fcf.Alg.Tree

type Eval (FibAlgebra (Succ (Fix (AnnF ((,) (Zero :: NatF (Fix (AnnF NatF Nat))) _)))) :: Nat -> Type) = 1
type Eval (FibAlgebra (Zero :: NatF (Ann NatF Nat))) Source # 
Instance details

Defined in Fcf.Alg.Tree

type Eval (FibAlgebra (Zero :: NatF (Ann NatF Nat))) = 0
type Eval (Attr (Fix (AnnF ((,) _ a2))) :: a1 -> Type) Source # 
Instance details

Defined in Fcf.Alg.Morphism

type Eval (Attr (Fix (AnnF ((,) _ a2))) :: a1 -> Type) = a2
type Eval (RecNTF n :: Fix NatF -> Type) Source # 
Instance details

Defined in Fcf.Alg.Tree

type Eval (RecNTF n :: Fix NatF -> Type) = Fix (Succ (Eval (NatToFix n)))
type Eval (NatToFix n :: Fix NatF -> Type) Source # 
Instance details

Defined in Fcf.Alg.Tree

type Eval (NatToFix n :: Fix NatF -> Type) = Eval (If (Eval (n < 1)) (Pure (Fix (Zero :: NatF (Fix NatF)))) (RecNTF =<< (n - 1)))
type Eval (DedupAlg (ConsF ((,) a2 as) ((,) _fxs past)) :: [a1] -> Type) Source # 
Instance details

Defined in Fcf.Alg.List

type Eval (DedupAlg (ConsF ((,) a2 as) ((,) _fxs past)) :: [a1] -> Type) = Eval (If (Eval (TyEq (Eval (Elem a2 past)) True)) (Pure past) (Pure (a2 ': as)))
type Eval (DedupAlg (NilF :: ListF (a, [a]) (Fix (ListF (a, [a])), [a])) :: [a] -> Type) Source # 
Instance details

Defined in Fcf.Alg.List

type Eval (DedupAlg (NilF :: ListF (a, [a]) (Fix (ListF (a, [a])), [a])) :: [a] -> Type) = ([] :: [a])
type Eval (EvensStrip (ConsF x y) :: [a] -> Type) Source # 
Instance details

Defined in Fcf.Alg.List

type Eval (EvensStrip (ConsF x y) :: [a] -> Type) = x ': Eval (Attr y)
type Eval (EvensStrip (NilF :: ListF a (Ann (ListF a) [a])) :: [a] -> Type) Source # 
Instance details

Defined in Fcf.Alg.List

type Eval (EvensStrip (NilF :: ListF a (Ann (ListF a) [a])) :: [a] -> Type) = ([] :: [a])
type Eval (EvensAlg (ConsF _ rst) :: [a] -> Type) Source # 
Instance details

Defined in Fcf.Alg.List

type Eval (EvensAlg (ConsF _ rst) :: [a] -> Type) = Eval ((EvensStrip :: ListF a (Ann (ListF a) [a]) -> [a] -> Type) =<< Strip rst)
type Eval (EvensAlg (NilF :: ListF a (Ann (ListF a) [a])) :: [a] -> Type) Source # 
Instance details

Defined in Fcf.Alg.List

type Eval (EvensAlg (NilF :: ListF a (Ann (ListF a) [a])) :: [a] -> Type) = ([] :: [a])
type Eval (ListToParaFix (a2 ': as) :: Fix (ListF (a1, [a1])) -> Type) Source # 
Instance details

Defined in Fcf.Alg.List

type Eval (ListToParaFix (a2 ': as) :: Fix (ListF (a1, [a1])) -> Type) = Fix (ConsF ((,) a2 as) (Eval (ListToParaFix as)))
type Eval (ListToParaFix ([] :: [a]) :: Fix (ListF (a, [a])) -> Type) Source # 
Instance details

Defined in Fcf.Alg.List

type Eval (ListToParaFix ([] :: [a]) :: Fix (ListF (a, [a])) -> Type) = Fix (NilF :: ListF (a, [a]) (Fix (ListF (a, [a]))))
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 (SlidingAlg n (ConsF ((,) a2 as) ((,) _fxs past)) :: [[a1]] -> Type) Source # 
Instance details

Defined in Fcf.Alg.List

type Eval (SlidingAlg n (ConsF ((,) a2 as) ((,) _fxs past)) :: [[a1]] -> Type) = Eval (Take n (a2 ': as)) ': past
type Eval (SlidingAlg _ (NilF :: ListF (a, [a]) (Fix (ListF (a, [a])), [[a]])) :: [[a]] -> Type) Source # 
Instance details

Defined in Fcf.Alg.List

type Eval (SlidingAlg _ (NilF :: ListF (a, [a]) (Fix (ListF (a, [a])), [[a]])) :: [[a]] -> Type) = ([] :: [[a]])
type Eval (Strip (Fix (AnnF ((,) x _))) :: f (Ann f a) -> Type) Source # 
Instance details

Defined in Fcf.Alg.Morphism

type Eval (Strip (Fix (AnnF ((,) x _))) :: f (Ann f a) -> Type) = x
type Eval (AnnConstr fxp :: Fix (AnnF f a) -> Type) Source # 
Instance details

Defined in Fcf.Alg.Morphism

type Eval (AnnConstr fxp :: Fix (AnnF f a) -> Type) = Eval (Pure (Fix (AnnF fxp)))
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 Eval (Sizes fx :: Ann f Nat -> Type) Source #

Sizes example from Recursion Schemes by example, Tim Williams. This annotes each node with the size of its subtree.

Example

>>> :kind! Eval (Sizes =<< Ana BuildNodeCoA 1)
Eval (Sizes =<< Ana BuildNodeCoA 1) :: Fix (AnnF (TreeF Nat) Nat)
= 'Fix
    ('AnnF
       '( 'NodeF
            1
            '[ 'Fix
                 ('AnnF
                    '( 'NodeF
                         2
                         '[ 'Fix ('AnnF '( 'NodeF 4 '[], 1)),
                            'Fix ('AnnF '( 'NodeF 5 '[], 1))],
                       3)),
               'Fix
                 ('AnnF
                    '( 'NodeF
                         3
                         '[ 'Fix ('AnnF '( 'NodeF 6 '[], 1)),
                            'Fix ('AnnF '( 'NodeF 7 '[], 1))],
                       3))],
          7))
Instance details

Defined in Fcf.Alg.Tree

type Eval (Sizes fx :: Ann f Nat -> Type) = Eval (Synthesize ((+) 1 <=< (FSum :: f Nat -> Nat -> Type)) fx)
type Eval (Fanout ralg (Fix f2) :: (Fix f1, k) -> Type) Source # 
Instance details

Defined in Fcf.Alg.Morphism

type Eval (Fanout ralg (Fix f2) :: (Fix f1, k) -> Type) = (,) (Fix f2) (Eval (Para ralg (Fix f2)))
type Eval (SynthAlg alg faf :: Ann f a -> Type) Source # 
Instance details

Defined in Fcf.Alg.Morphism

type Eval (SynthAlg alg faf :: Ann f a -> Type) = Eval (AnnConstr ((,) faf (Eval (alg =<< Map (Attr :: Ann f a -> a -> Type) faf))))
type Eval (Synthesize f2 fx :: Ann f1 a -> Type) Source # 
Instance details

Defined in Fcf.Alg.Morphism

type Eval (Synthesize f2 fx :: Ann f1 a -> Type) = Eval (Cata (SynthAlg f2) fx)
type Eval (HistoAlg alg faf :: Ann f a -> Type) Source # 
Instance details

Defined in Fcf.Alg.Morphism

type Eval (HistoAlg alg faf :: Ann f a -> Type) = Eval (AnnConstr ((,) faf (Eval (alg faf))))

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.

type RAlgebra f a = f (Fix f, a) -> Exp a Source #

Commonly used name describing the method Para 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. There we have e.g. ListToFix-function.

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

Expand
>>> 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

Expand
>>> 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 Fanout :: RAlgebra f a -> Fix f -> Exp (Fix f, a) Source #

Instances
type Eval (Fanout ralg (Fix f2) :: (Fix f1, k) -> Type) Source # 
Instance details

Defined in Fcf.Alg.Morphism

type Eval (Fanout ralg (Fix f2) :: (Fix f1, k) -> Type) = (,) (Fix f2) (Eval (Para ralg (Fix f2)))

data Para :: RAlgebra f a -> Fix f -> Exp a Source #

Write a function to give a Fix, and feed it in together with an RAlgebra

Check Fcf.Alg.List to see example algebras in use. There we have e.g. ListToParaFix-function.

Instances
type Eval (Para ralg (Fix a2) :: a1 -> Type) Source # 
Instance details

Defined in Fcf.Alg.Morphism

type Eval (Para ralg (Fix a2) :: a1 -> Type) = ralg @@ Eval (Map (Fanout ralg) a2)

newtype AnnF f a r Source #

Annotate (f r) with attribute a (from Recursion Schemes by example, Tim Williams).

Constructors

AnnF (f r, a) 
Instances
type Eval (FibAlgebra (Succ (Fix (AnnF ((,) (Succ (Fix (AnnF ((,) _ n)))) m)))) :: Nat -> Type) Source # 
Instance details

Defined in Fcf.Alg.Tree

type Eval (FibAlgebra (Succ (Fix (AnnF ((,) (Succ (Fix (AnnF ((,) _ n)))) m)))) :: Nat -> Type) = Eval (n + m)
type Eval (FibAlgebra (Succ (Fix (AnnF ((,) (Zero :: NatF (Fix (AnnF NatF Nat))) _)))) :: Nat -> Type) Source # 
Instance details

Defined in Fcf.Alg.Tree

type Eval (FibAlgebra (Succ (Fix (AnnF ((,) (Zero :: NatF (Fix (AnnF NatF Nat))) _)))) :: Nat -> Type) = 1
type Eval (FibAlgebra (Zero :: NatF (Ann NatF Nat))) Source # 
Instance details

Defined in Fcf.Alg.Tree

type Eval (FibAlgebra (Zero :: NatF (Ann NatF Nat))) = 0
type Eval (Attr (Fix (AnnF ((,) _ a2))) :: a1 -> Type) Source # 
Instance details

Defined in Fcf.Alg.Morphism

type Eval (Attr (Fix (AnnF ((,) _ a2))) :: a1 -> Type) = a2
type Eval (EvensStrip (ConsF x y) :: [a] -> Type) Source # 
Instance details

Defined in Fcf.Alg.List

type Eval (EvensStrip (ConsF x y) :: [a] -> Type) = x ': Eval (Attr y)
type Eval (EvensStrip (NilF :: ListF a (Ann (ListF a) [a])) :: [a] -> Type) Source # 
Instance details

Defined in Fcf.Alg.List

type Eval (EvensStrip (NilF :: ListF a (Ann (ListF a) [a])) :: [a] -> Type) = ([] :: [a])
type Eval (EvensAlg (ConsF _ rst) :: [a] -> Type) Source # 
Instance details

Defined in Fcf.Alg.List

type Eval (EvensAlg (ConsF _ rst) :: [a] -> Type) = Eval ((EvensStrip :: ListF a (Ann (ListF a) [a]) -> [a] -> Type) =<< Strip rst)
type Eval (EvensAlg (NilF :: ListF a (Ann (ListF a) [a])) :: [a] -> Type) Source # 
Instance details

Defined in Fcf.Alg.List

type Eval (EvensAlg (NilF :: ListF a (Ann (ListF a) [a])) :: [a] -> Type) = ([] :: [a])
type Eval (Strip (Fix (AnnF ((,) x _))) :: f (Ann f a) -> Type) Source # 
Instance details

Defined in Fcf.Alg.Morphism

type Eval (Strip (Fix (AnnF ((,) x _))) :: f (Ann f a) -> Type) = x
type Eval (AnnConstr fxp :: Fix (AnnF f a) -> Type) Source # 
Instance details

Defined in Fcf.Alg.Morphism

type Eval (AnnConstr fxp :: Fix (AnnF f a) -> Type) = Eval (Pure (Fix (AnnF fxp)))
type Eval (Sizes fx :: Ann f Nat -> Type) Source #

Sizes example from Recursion Schemes by example, Tim Williams. This annotes each node with the size of its subtree.

Example

>>> :kind! Eval (Sizes =<< Ana BuildNodeCoA 1)
Eval (Sizes =<< Ana BuildNodeCoA 1) :: Fix (AnnF (TreeF Nat) Nat)
= 'Fix
    ('AnnF
       '( 'NodeF
            1
            '[ 'Fix
                 ('AnnF
                    '( 'NodeF
                         2
                         '[ 'Fix ('AnnF '( 'NodeF 4 '[], 1)),
                            'Fix ('AnnF '( 'NodeF 5 '[], 1))],
                       3)),
               'Fix
                 ('AnnF
                    '( 'NodeF
                         3
                         '[ 'Fix ('AnnF '( 'NodeF 6 '[], 1)),
                            'Fix ('AnnF '( 'NodeF 7 '[], 1))],
                       3))],
          7))
Instance details

Defined in Fcf.Alg.Tree

type Eval (Sizes fx :: Ann f Nat -> Type) = Eval (Synthesize ((+) 1 <=< (FSum :: f Nat -> Nat -> Type)) fx)
type Eval (SynthAlg alg faf :: Ann f a -> Type) Source # 
Instance details

Defined in Fcf.Alg.Morphism

type Eval (SynthAlg alg faf :: Ann f a -> Type) = Eval (AnnConstr ((,) faf (Eval (alg =<< Map (Attr :: Ann f a -> a -> Type) faf))))
type Eval (Synthesize f2 fx :: Ann f1 a -> Type) Source # 
Instance details

Defined in Fcf.Alg.Morphism

type Eval (Synthesize f2 fx :: Ann f1 a -> Type) = Eval (Cata (SynthAlg f2) fx)
type Eval (HistoAlg alg faf :: Ann f a -> Type) Source # 
Instance details

Defined in Fcf.Alg.Morphism

type Eval (HistoAlg alg faf :: Ann f a -> Type) = Eval (AnnConstr ((,) faf (Eval (alg faf))))

type Ann f a = Fix (AnnF f a) Source #

Annotated fixed-point type. A cofree comonad (from Recursion Schemes by example, Tim Williams).

data Attr :: Ann f a -> Exp a Source #

Attribute of the root node (from Recursion Schemes by example, Tim Williams).

Instances
type Eval (Attr (Fix (AnnF ((,) _ a2))) :: a1 -> Type) Source # 
Instance details

Defined in Fcf.Alg.Morphism

type Eval (Attr (Fix (AnnF ((,) _ a2))) :: a1 -> Type) = a2

data Strip :: Ann f a -> Exp (f (Ann f a)) Source #

Strip attribute from root (from Recursion Schemes by example, Tim Williams).

Instances
type Eval (Strip (Fix (AnnF ((,) x _))) :: f (Ann f a) -> Type) Source # 
Instance details

Defined in Fcf.Alg.Morphism

type Eval (Strip (Fix (AnnF ((,) x _))) :: f (Ann f a) -> Type) = x

data AnnConstr :: (f (Ann f a), a) -> Exp (Fix (AnnF f a)) Source #

Annotation constructor (from Recursion Schemes by example, Tim Williams).

Instances
type Eval (AnnConstr fxp :: Fix (AnnF f a) -> Type) Source # 
Instance details

Defined in Fcf.Alg.Morphism

type Eval (AnnConstr fxp :: Fix (AnnF f a) -> Type) = Eval (Pure (Fix (AnnF fxp)))

data SynthAlg :: (f a -> Exp a) -> f (Ann f a) -> Exp (Ann f a) Source #

Synthesized attributes are created in a bottom-up traversal using a catamorphism (from Recursion Schemes by example, Tim Williams).

This is the algebra that is fed to the cata.

Instances
type Eval (SynthAlg alg faf :: Ann f a -> Type) Source # 
Instance details

Defined in Fcf.Alg.Morphism

type Eval (SynthAlg alg faf :: Ann f a -> Type) = Eval (AnnConstr ((,) faf (Eval (alg =<< Map (Attr :: Ann f a -> a -> Type) faf))))

data Synthesize :: (f a -> Exp a) -> Fix f -> Exp (Ann f a) Source #

Synthesized attributes are created in a bottom-up traversal using a catamorphism (from Recursion Schemes by example, Tim Williams).

For the example, see Fcf.Data.Alg.Tree.Sizes.

Instances
type Eval (Synthesize f2 fx :: Ann f1 a -> Type) Source # 
Instance details

Defined in Fcf.Alg.Morphism

type Eval (Synthesize f2 fx :: Ann f1 a -> Type) = Eval (Cata (SynthAlg f2) fx)

data HistoAlg :: (f (Ann f a) -> Exp a) -> f (Ann f a) -> Exp (Ann f a) Source #

Histo takes annotation algebra and takes a Fix-structure (from Recursion Schemes by example, Tim Williams).

This is a helper for Histo as it is implemented with Cata.

Instances
type Eval (HistoAlg alg faf :: Ann f a -> Type) Source # 
Instance details

Defined in Fcf.Alg.Morphism

type Eval (HistoAlg alg faf :: Ann f a -> Type) = Eval (AnnConstr ((,) faf (Eval (alg faf))))

data Histo :: (f (Ann f a) -> Exp a) -> Fix f -> Exp a Source #

Histo takes annotation algebra and takes a Fix-structure (from Recursion Schemes by example, Tim Williams).

Examples can be found from Fcf.Data.Alg.Tree and Fcf.Data.Alg.List modules.

Instances
type Eval (Histo alg fx :: a -> Type) Source # 
Instance details

Defined in Fcf.Alg.Morphism

type Eval (Histo alg fx :: a -> Type) = Eval ((Attr :: Ann f a -> a -> Type) =<< Cata (HistoAlg alg) fx)

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

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

Example

Expand
>>> :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

Expand
>>> :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)