fcf-containers-0.7.0: Data structures and algorithms for first-class-families
Copyright(c) gspia 2020-
LicenseBSD
Maintainergspia
Safe HaskellSafe-Inferred
LanguageHaskell2010

Fcf.Control.Monad

Description

Fcf.Control.Monad

Synopsis

Documentation

data Return :: a -> Exp (m a) Source #

Return corresponds to the return at Monad or pure of Applicative.

:kind! Eval (Return 1) :: Maybe Nat :kind! Eval (Return 1) :: Either Symbol Nat

Instances

Instances details
type Eval (Return a :: [k] -> Type) Source # 
Instance details

Defined in Fcf.Control.Monad

type Eval (Return a :: [k] -> Type) = '[a]
type Eval (Return a2 :: Maybe a1 -> Type) Source # 
Instance details

Defined in Fcf.Control.Monad

type Eval (Return a2 :: Maybe a1 -> Type) = 'Just a2
type Eval (Return a2 :: Identity a1 -> Type) Source # 
Instance details

Defined in Fcf.Control.Monad

type Eval (Return a2 :: Identity a1 -> Type) = 'Identity a2
type Eval (Return a2 :: Tree a1 -> Type) Source # 
Instance details

Defined in Fcf.Data.Tree

type Eval (Return a2 :: Tree a1 -> Type) = 'Node a2 ('[] :: [Tree a1])
type Eval (Return a2 :: Either a1 b -> Type) Source # 
Instance details

Defined in Fcf.Control.Monad

type Eval (Return a2 :: Either a1 b -> Type) = 'Right a2 :: Either a1 b

data (<*>) :: f (a -> Exp b) -> f a -> Exp (f b) Source #

(*) corresponds to the value level <*>. Note that this clashes with the definition given at Fcf.Combinators.((*)).

Applicatives that we define include:

  • Identity
  • []
  • Maybe
  • Either

Example

Expand
>>> :kind! Eval ('Identity Plus2 <*> 'Identity 5)
Eval ('Identity Plus2 <*> 'Identity 5) :: Identity Nat
= 'Identity 7
>>> :kind! Eval ( (<*>) '[ (Fcf.+) 1, (Fcf.*) 10] '[4,5,6,7])
Eval ( (<*>) '[ (Fcf.+) 1, (Fcf.*) 10] '[4,5,6,7]) :: [Nat]
= '[5, 6, 7, 8, 40, 50, 60, 70]
>>> :kind! Eval ( (<*>) '[ (Fcf.+) 1, (Fcf.*) 10] '[])
Eval ( (<*>) '[ (Fcf.+) 1, (Fcf.*) 10] '[]) :: [Nat]
= '[]
>>> :kind! Eval ( (<*>) '[] '[4,5,6,7])
Eval ( (<*>) '[] '[4,5,6,7]) :: [b]
= '[]

Instances

Instances details
type Eval (_1 <*> ('[] :: [a]) :: [b] -> Type) Source # 
Instance details

Defined in Fcf.Control.Monad

type Eval (_1 <*> ('[] :: [a]) :: [b] -> Type) = '[] :: [b]
type Eval (('[] :: [a -> Exp b]) <*> _1 :: [b] -> Type) Source # 
Instance details

Defined in Fcf.Control.Monad

type Eval (('[] :: [a -> Exp b]) <*> _1 :: [b] -> Type) = '[] :: [b]
type Eval ((f ': fs) <*> (a2 ': as) :: [b] -> Type) Source # 
Instance details

Defined in Fcf.Control.Monad

type Eval ((f ': fs) <*> (a2 ': as) :: [b] -> Type) = Eval (Eval (Star_ f (a2 ': as)) ++ Eval (fs <*> (a2 ': as)))
type Eval ('Just f <*> m :: Maybe b -> Type) Source # 
Instance details

Defined in Fcf.Control.Monad

type Eval ('Just f <*> m :: Maybe b -> Type) = Eval (Map f m)
type Eval (('Nothing :: Maybe (a -> Exp b)) <*> _1 :: Maybe b -> Type) Source # 
Instance details

Defined in Fcf.Control.Monad

type Eval (('Nothing :: Maybe (a -> Exp b)) <*> _1 :: Maybe b -> Type) = 'Nothing :: Maybe b
type Eval ('Identity f <*> m :: Identity b -> Type) Source # 
Instance details

Defined in Fcf.Control.Monad

type Eval ('Identity f <*> m :: Identity b -> Type) = Eval (Map f m)
type Eval ('Node f tfs <*> 'Node x txs :: Tree b -> Type) Source # 
Instance details

Defined in Fcf.Data.Tree

type Eval ('Node f tfs <*> 'Node x txs :: Tree b -> Type) = 'Node (Eval (f x)) (Eval (Eval (Map (Map f :: Tree a -> Tree b -> Type) txs) ++ Eval (Map (StarTx ('Node x txs) :: Tree (a -> Exp b) -> Tree b -> Type) tfs)))
type Eval (('Right f :: Either a2 (a1 -> Exp b)) <*> m :: Either a2 b -> Type) Source # 
Instance details

Defined in Fcf.Control.Monad

type Eval (('Right f :: Either a2 (a1 -> Exp b)) <*> m :: Either a2 b -> Type) = Eval (Map f m)
type Eval (('Left e :: Either a1 (a2 -> Exp b)) <*> _1 :: Either a1 b -> Type) Source # 
Instance details

Defined in Fcf.Control.Monad

type Eval (('Left e :: Either a1 (a2 -> Exp b)) <*> _1 :: Either a1 b -> Type) = 'Left e :: Either a1 b

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

Helper for the [] applicative instance.

Instances

Instances details
type Eval (Star_ f (a2 ': as) :: [b] -> Type) Source # 
Instance details

Defined in Fcf.Control.Monad

type Eval (Star_ f (a2 ': as) :: [b] -> Type) = Eval (f a2) ': Eval (Star_ f as)
type Eval (Star_ _1 ('[] :: [a]) :: [b] -> Type) Source # 
Instance details

Defined in Fcf.Control.Monad

type Eval (Star_ _1 ('[] :: [a]) :: [b] -> Type) = '[] :: [b]

data Plus1 :: Nat -> Exp Nat Source #

Instances

Instances details
type Eval (Plus1 n :: Nat -> Type) Source # 
Instance details

Defined in Fcf.Control.Monad

type Eval (Plus1 n :: Nat -> Type) = n + 1

data Plus2 :: Nat -> Exp Nat Source #

Instances

Instances details
type Eval (Plus2 n :: Nat -> Type) Source # 
Instance details

Defined in Fcf.Control.Monad

type Eval (Plus2 n :: Nat -> Type) = n + 2

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

Type level LiftA2.

Example

Expand
>>> :kind! Eval (LiftA2 (Fcf.+) '[1,2] '[3,4])
Eval (LiftA2 (Fcf.+) '[1,2] '[3,4]) :: [Nat]
= '[4, 5, 5, 6]

Instances

Instances details
type Eval (LiftA2 f (a2 ': as) ('[] :: [b]) :: [c] -> Type) Source # 
Instance details

Defined in Fcf.Control.Monad

type Eval (LiftA2 f (a2 ': as) ('[] :: [b]) :: [c] -> Type) = '[] :: [c]
type Eval (LiftA2 f ('[] :: [a]) _1 :: [c] -> Type) Source # 
Instance details

Defined in Fcf.Control.Monad

type Eval (LiftA2 f ('[] :: [a]) _1 :: [c] -> Type) = '[] :: [c]
type Eval (LiftA2 f (a3 ': as) (b ': bs) :: [c] -> Type) Source # 
Instance details

Defined in Fcf.Control.Monad

type Eval (LiftA2 f (a3 ': as) (b ': bs) :: [c] -> Type) = Eval (Eval (LiftA2_ f a3 (b ': bs)) ++ Eval (LiftA2 f as (b ': bs)))
type Eval (LiftA2 f ('Just a3) ('Just b2) :: Maybe a2 -> Type) Source # 
Instance details

Defined in Fcf.Control.Monad

type Eval (LiftA2 f ('Just a3) ('Just b2) :: Maybe a2 -> Type) = 'Just (Eval (f a3 b2))
type Eval (LiftA2 f _1 ('Nothing :: Maybe b) :: Maybe c -> Type) Source # 
Instance details

Defined in Fcf.Control.Monad

type Eval (LiftA2 f _1 ('Nothing :: Maybe b) :: Maybe c -> Type) = 'Nothing :: Maybe c
type Eval (LiftA2 f ('Nothing :: Maybe a) _1 :: Maybe c -> Type) Source # 
Instance details

Defined in Fcf.Control.Monad

type Eval (LiftA2 f ('Nothing :: Maybe a) _1 :: Maybe c -> Type) = 'Nothing :: Maybe c
type Eval (LiftA2 f ('Right a3 :: Either a2 a1) ('Right b3 :: Either a2 b1) :: Either a2 b2 -> Type) Source # 
Instance details

Defined in Fcf.Control.Monad

type Eval (LiftA2 f ('Right a3 :: Either a2 a1) ('Right b3 :: Either a2 b1) :: Either a2 b2 -> Type) = 'Right (Eval (f a3 b3)) :: Either a2 b2
type Eval (LiftA2 f ('Right _1 :: Either a2 a1) ('Left e :: Either a2 b) :: Either a2 c -> Type) Source # 
Instance details

Defined in Fcf.Control.Monad

type Eval (LiftA2 f ('Right _1 :: Either a2 a1) ('Left e :: Either a2 b) :: Either a2 c -> Type) = 'Left e :: Either a2 c
type Eval (LiftA2 f ('Left e :: Either a2 a1) _1 :: Either a2 c -> Type) Source # 
Instance details

Defined in Fcf.Control.Monad

type Eval (LiftA2 f ('Left e :: Either a2 a1) _1 :: Either a2 c -> Type) = 'Left e :: Either a2 c

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

Instances

Instances details
type Eval (LiftA2_ f a2 (b2 ': bs) :: [c] -> Type) Source # 
Instance details

Defined in Fcf.Control.Monad

type Eval (LiftA2_ f a2 (b2 ': bs) :: [c] -> Type) = Eval (f a2 b2) ': Eval (LiftA2_ f a2 bs)
type Eval (LiftA2_ f a2 ('[] :: [b]) :: [c] -> Type) Source # 
Instance details

Defined in Fcf.Control.Monad

type Eval (LiftA2_ f a2 ('[] :: [b]) :: [c] -> Type) = '[] :: [c]

data (>>=) :: m a -> (a -> Exp (m b)) -> Exp (m b) Source #

Type level Bind corresponding to the value level bind >>= operator. Note that name (>>=) clashes with the definition given at Fcf.Combinators.(>>=). (It doesn't export it yet, though.)

Monads that we define include:

  • Identity
  • []
  • Maybe
  • Either

Example

Expand

Example: double the length of the input list and increase the numbers at the same time.

>>> :kind! Eval ('[5,6,7] >>= Plus2M)
Eval ('[5,6,7] >>= Plus2M) :: [Nat]
= '[7, 8, 8, 9, 9, 10]
>>> :kind! Eval (XsPlusYsMonadic '[1,2,3] '[4,5,6])
Eval (XsPlusYsMonadic '[1,2,3] '[4,5,6]) :: [Nat]
= '[5, 6, 7, 6, 7, 8, 7, 8, 9]

Instances

Instances details
type Eval ((x ': xs) >>= f :: [b] -> Type) Source # 
Instance details

Defined in Fcf.Control.Monad

type Eval ((x ': xs) >>= f :: [b] -> Type) = Eval ((f @@ x) ++ Eval (xs >>= f))
type Eval (('[] :: [a]) >>= _1 :: [b] -> Type) Source # 
Instance details

Defined in Fcf.Control.Monad

type Eval (('[] :: [a]) >>= _1 :: [b] -> Type) = '[] :: [b]
type Eval ('Just a2 >>= f :: Maybe b -> Type) Source # 
Instance details

Defined in Fcf.Control.Monad

type Eval ('Just a2 >>= f :: Maybe b -> Type) = Eval (f a2)
type Eval (('Nothing :: Maybe a) >>= f :: Maybe b -> Type) Source # 
Instance details

Defined in Fcf.Control.Monad

type Eval (('Nothing :: Maybe a) >>= f :: Maybe b -> Type) = 'Nothing :: Maybe b
type Eval ('Identity a2 >>= f :: Identity b -> Type) Source # 
Instance details

Defined in Fcf.Control.Monad

type Eval ('Identity a2 >>= f :: Identity b -> Type) = Eval (f a2)
type Eval (('Right a3 :: Either a2 a1) >>= f :: Either a2 b -> Type) Source # 
Instance details

Defined in Fcf.Control.Monad

type Eval (('Right a3 :: Either a2 a1) >>= f :: Either a2 b -> Type) = Eval (f a3)
type Eval (('Left a3 :: Either a1 a2) >>= _1 :: Either a1 b -> Type) Source # 
Instance details

Defined in Fcf.Control.Monad

type Eval (('Left a3 :: Either a1 a2) >>= _1 :: Either a1 b -> Type) = 'Left a3 :: Either a1 b

data Plus2M :: Nat -> Exp [Nat] Source #

Instances

Instances details
type Eval (Plus2M n :: [Nat] -> Type) Source # 
Instance details

Defined in Fcf.Control.Monad

type Eval (Plus2M n :: [Nat] -> Type) = '[n + 2, n + 3]

data PureXPlusY :: Nat -> Nat -> Exp [Nat] Source #

Instances

Instances details
type Eval (PureXPlusY x y :: [Nat] -> Type) Source # 
Instance details

Defined in Fcf.Control.Monad

type Eval (PureXPlusY x y :: [Nat] -> Type) = Eval (Return (x + y) :: [Nat] -> Type)

data XPlusYs :: Nat -> [Nat] -> Exp [Nat] Source #

Instances

Instances details
type Eval (XPlusYs x ys :: [Nat] -> Type) Source # 
Instance details

Defined in Fcf.Control.Monad

type Eval (XPlusYs x ys :: [Nat] -> Type) = Eval (ys >>= PureXPlusY x)

data XsPlusYsMonadic :: [Nat] -> [Nat] -> Exp [Nat] Source #

An example implementing

sumM xs ys = do x <- xs y <- ys return (x + y)

or

sumM xs ys = xs >>= (x -> ys >>= (y -> pure (x+y)))

Note the use of helper functions. This is a bit awkward, a type level lambda would be nice.

Instances

Instances details
type Eval (XsPlusYsMonadic xs ys :: [Nat] -> Type) Source # 
Instance details

Defined in Fcf.Control.Monad

type Eval (XsPlusYsMonadic xs ys :: [Nat] -> Type) = Eval (xs >>= Flip XPlusYs ys)

data (>>) :: m a -> m b -> Exp (m b) Source #

Instances

Instances details
type Eval ((x ': xs) >> b2 :: [b1] -> Type) Source # 
Instance details

Defined in Fcf.Control.Monad

type Eval ((x ': xs) >> b2 :: [b1] -> Type) = b2
type Eval (('[] :: [a]) >> _1 :: [b] -> Type) Source # 
Instance details

Defined in Fcf.Control.Monad

type Eval (('[] :: [a]) >> _1 :: [b] -> Type) = '[] :: [b]
type Eval ('Just a2 >> b2 :: Maybe b1 -> Type) Source # 
Instance details

Defined in Fcf.Control.Monad

type Eval ('Just a2 >> b2 :: Maybe b1 -> Type) = b2
type Eval (('Nothing :: Maybe a) >> b2 :: Maybe b1 -> Type) Source # 
Instance details

Defined in Fcf.Control.Monad

type Eval (('Nothing :: Maybe a) >> b2 :: Maybe b1 -> Type) = 'Nothing :: Maybe b1
type Eval (('Right _1 :: Either a2 a1) >> b2 :: Either a2 b1 -> Type) Source # 
Instance details

Defined in Fcf.Control.Monad

type Eval (('Right _1 :: Either a2 a1) >> b2 :: Either a2 b1 -> Type) = b2
type Eval (('Left a3 :: Either a1 a2) >> _1 :: Either a1 b -> Type) Source # 
Instance details

Defined in Fcf.Control.Monad

type Eval (('Left a3 :: Either a1 a2) >> _1 :: Either a1 b -> Type) = 'Left a3 :: Either a1 b

data MapM :: (a -> Exp (m b)) -> t a -> Exp (m (t b)) Source #

MapM

Example

Expand
>>> :kind! Eval (MapM (ConstFn '[ 'True, 'False]) '["a","b","c"])
Eval (MapM (ConstFn '[ 'True, 'False]) '["a","b","c"]) :: [[Bool]]
= '[ '[ 'True, 'True, 'True], '[ 'True, 'True, 'False],
     '[ 'True, 'False, 'True], '[ 'True, 'False, 'False],
     '[ 'False, 'True, 'True], '[ 'False, 'True, 'False],
     '[ 'False, 'False, 'True], '[ 'False, 'False, 'False]]

Instances

Instances details
type Eval (MapM f2 ta :: f1 (t a2) -> Type) Source # 
Instance details

Defined in Fcf.Control.Monad

type Eval (MapM f2 ta :: f1 (t a2) -> Type) = Eval (Sequence ((Map f2 :: t a1 -> t (f1 a2) -> Type) @@ ta))

data ForM :: t a -> (a -> Exp (m b)) -> Exp (m (t b)) Source #

ForM = Flip MapM

Instances

Instances details
type Eval (ForM ta f :: m (t b) -> Type) Source # 
Instance details

Defined in Fcf.Control.Monad

type Eval (ForM ta f :: m (t b) -> Type) = Eval (MapM f ta)

data Traverse :: (a -> Exp (f b)) -> t a -> Exp (f (t b)) Source #

Traverse

Example

Expand
>>> :kind! Eval (Traverse Id '[ '[1,2], '[3,4]])
Eval (Traverse Id '[ '[1,2], '[3,4]]) :: [[Nat]]
= '[ '[1, 3], '[1, 4], '[2, 3], '[2, 4]]

Instances

Instances details
type Eval (Traverse f2 ('Right x :: Either a3 a1) :: f1 (Either a3 a2) -> Type) Source # 
Instance details

Defined in Fcf.Control.Monad

type Eval (Traverse f2 ('Right x :: Either a3 a1) :: f1 (Either a3 a2) -> Type) = Eval (Map (Pure1 ('Right :: a2 -> Either a3 a2)) (Eval (f2 x)))
type Eval (Traverse f2 ('Left e :: Either a2 a1) :: f1 (Either a2 b) -> Type) Source # 
Instance details

Defined in Fcf.Control.Monad

type Eval (Traverse f2 ('Left e :: Either a2 a1) :: f1 (Either a2 b) -> Type) = Eval (Return ('Left e :: Either a2 b) :: f1 (Either a2 b) -> Type)
type Eval (Traverse f2 ('Just x) :: f1 (Maybe a2) -> Type) Source # 
Instance details

Defined in Fcf.Control.Monad

type Eval (Traverse f2 ('Just x) :: f1 (Maybe a2) -> Type) = Eval (Map (Pure1 ('Just :: a2 -> Maybe a2)) (Eval (f2 x)))
type Eval (Traverse f2 ('Nothing :: Maybe a) :: f1 (Maybe b) -> Type) Source # 
Instance details

Defined in Fcf.Control.Monad

type Eval (Traverse f2 ('Nothing :: Maybe a) :: f1 (Maybe b) -> Type) = Eval (Return ('Nothing :: Maybe b) :: f1 (Maybe b) -> Type)
type Eval (Traverse f2 lst :: f1 [b] -> Type) Source # 
Instance details

Defined in Fcf.Control.Monad

type Eval (Traverse f2 lst :: f1 [b] -> Type) = Eval (Foldr (Cons_f f2) (Eval (Return ('[] :: [b]) :: f1 [b] -> Type)) lst)
type Eval (Traverse f2 ('Node x ts) :: f1 (Tree b) -> Type) Source # 
Instance details

Defined in Fcf.Data.Tree

type Eval (Traverse f2 ('Node x ts) :: f1 (Tree b) -> Type) = Eval (LiftA2 (Pure2 ('Node :: b -> [Tree b] -> Tree b)) (Eval (f2 x)) (Eval (Traverse (Traverse f2 :: Tree a -> f1 (Tree b) -> Type) ts)))

data Cons_f :: (a -> Exp (f b)) -> a -> f [b] -> Exp (f [b]) Source #

Helper for [] traverse

Instances

Instances details
type Eval (Cons_f f2 x ys :: f1 [a2] -> Type) Source # 
Instance details

Defined in Fcf.Control.Monad

type Eval (Cons_f f2 x ys :: f1 [a2] -> Type) = Eval (LiftA2 (Pure2 ('(:) :: a2 -> [a2] -> [a2])) (Eval (f2 x)) ys)

data Id :: a -> Exp a Source #

Id function correspondes to term level id-function.

Instances

Instances details
type Eval (Id a2 :: a1 -> Type) Source # 
Instance details

Defined in Fcf.Control.Monad

type Eval (Id a2 :: a1 -> Type) = a2

data Sequence :: t (f a) -> Exp (f (t a)) Source #

Sequence

Example

Expand
>>> :kind! Eval (Sequence ('Just ('Right 5)))
Eval (Sequence ('Just ('Right 5))) :: Either a (Maybe Nat)
= 'Right ('Just 5)
>>> :kind! Eval (Sequence '[ 'Just 3, 'Just 5, 'Just 7])
Eval (Sequence '[ 'Just 3, 'Just 5, 'Just 7]) :: Maybe [Nat]
= 'Just '[3, 5, 7]
>>> :kind! Eval (Sequence '[ 'Just 3, 'Nothing, 'Just 7])
Eval (Sequence '[ 'Just 3, 'Nothing, 'Just 7]) :: Maybe [Nat]
= 'Nothing
>>> :kind! Eval (Sequence '[ '[1,2], '[3,4]])
Eval (Sequence '[ '[1,2], '[3,4]]) :: [[Nat]]
= '[ '[1, 3], '[1, 4], '[2, 3], '[2, 4]]

Instances

Instances details
type Eval (Sequence tfa :: f (t b) -> Type) Source # 
Instance details

Defined in Fcf.Control.Monad

type Eval (Sequence tfa :: f (t b) -> Type) = Eval (Traverse (Id :: f b -> f b -> Type) tfa)