Fcf.Control.Monad

Fcf.Control.Monad

Documentation

>>> import qualified GHC.TypeLits as TL
>>> import qualified Fcf.Combinators as C

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

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

type Eval (Return a2 :: Identity a1 -> Type)

Defined in Fcf.Control.Monad

type Eval (Return a2 :: Identity a1 -> Type) = 'Identity a2

type Eval (Return a2 :: Tree a1 -> Type)

Defined in Fcf.Data.Tree

type Eval (Return a2 :: Tree a1 -> Type) = 'Node a2 ('[] :: [Tree a1])

type Eval (Return a2 :: Maybe a1 -> Type)

Defined in Fcf.Control.Monad

type Eval (Return a2 :: Maybe a1 -> Type) = 'Just a2

type Eval (Return a :: [k] -> Type)

Defined in Fcf.Control.Monad

type Eval (Return a :: [k] -> Type) = '[a]

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

Defined in Fcf.Control.Monad

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

type Eval (Return a :: (k1, k2) -> Type)

Defined in Fcf.Control.Monad

type Eval (Return a :: (k1, k2) -> Type) = '(MEmpty :: k1, a)

type Eval (Return a :: (k1, k2, k3) -> Type)

Defined in Fcf.Control.Monad

type Eval (Return a :: (k1, k2, k3) -> Type) = '(MEmpty :: k1, MEmpty :: k2, a)

type Eval (Return a :: (k1, k2, k3, k4) -> Type)

Defined in Fcf.Control.Monad

type Eval (Return a :: (k1, k2, k3, k4) -> Type) = '(MEmpty :: k1, MEmpty :: k2, MEmpty :: k3, a)

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

(*) 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

>>> :kind! Eval ('Identity Plus2 <*> 'Identity 5)
Eval ('Identity Plus2 <*> 'Identity 5) :: Identity Natural
= 'Identity 7

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

Instances

type Eval ('Identity f <*> m :: Identity b -> Type)

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)

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 ('Just f <*> m :: Maybe b -> Type)

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)

Defined in Fcf.Control.Monad

type Eval (('Nothing :: Maybe (a -> Exp b)) <*> _1 :: Maybe b -> Type) = 'Nothing :: Maybe b

type Eval (('[] :: [a -> Exp b]) <*> _1 :: [b] -> Type)

Defined in Fcf.Control.Monad

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

type Eval (_1 <*> ('[] :: [a]) :: [b] -> Type)

Defined in Fcf.Control.Monad

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

type Eval ((f ': fs) <*> (a2 ': as) :: [b] -> Type)

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 (('Left e :: Either a1 (a2 -> Exp b)) <*> _1 :: Either a1 b -> Type)

Defined in Fcf.Control.Monad

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

type Eval (('Right f :: Either a1 (a2 -> Exp b)) <*> m :: Either a1 b -> Type)

Defined in Fcf.Control.Monad

type Eval (('Right f :: Either a1 (a2 -> Exp b)) <*> m :: Either a1 b -> Type) = Eval (Map f m)

type Eval ('(u, f) <*> '(v, x) :: (k1, k2) -> Type)

For tuples, the Monoid constraint determines how the first values merge. For example, Symbols concatenate:

>>> :kind! Eval ('("hello", (Fcf.+) 15) <*> '("world!", 2002))
Eval ('("hello", (Fcf.+) 15) <*> '("world!", 2002)) :: (TL.Symbol,
                                                        Natural)
= '("helloworld!", 2017)

Defined in Fcf.Control.Monad

type Eval ('(u, f) <*> '(v, x) :: (k1, k2) -> Type) = '(u <> v, Eval (f x))

type Eval ('(a2, b, f) <*> '(a', b', x) :: (k1, k2, k3) -> Type)

Defined in Fcf.Control.Monad

type Eval ('(a2, b, f) <*> '(a', b', x) :: (k1, k2, k3) -> Type) = '(a2 <> a', b <> b', Eval (f x))

type Eval ('(a2, b, c, f) <*> '(a', b', c', x) :: (k1, k2, k3, k4) -> Type)

Defined in Fcf.Control.Monad

type Eval ('(a2, b, c, f) <*> '(a', b', c', x) :: (k1, k2, k3, k4) -> Type) = '(a2 <> a', b <> b', c <> c', Eval (f x))

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

Type level LiftA2.

Example

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

Instances

type Eval (LiftA2 f2 fa fb :: f1 b -> Type)

Defined in Fcf.Control.Monad

type Eval (LiftA2 f2 fa fb :: f1 b -> Type) = Eval (Eval (Map (App2 f2) fa) <*> fb)

data LiftA3 :: (a -> b -> c -> Exp d) -> f a -> f b -> f c -> Exp (f d)

Type level LiftA3.

Example

>>> :kind! Eval (LiftA3 Tuple3 '[1,2] '[3,4] '[5,6])
Eval (LiftA3 Tuple3 '[1,2] '[3,4] '[5,6]) :: [(Natural, Natural,
                                               Natural)]
= '[ '(1, 3, 5), '(1, 3, 6), '(1, 4, 5), '(1, 4, 6), '(2, 3, 5),
     '(2, 3, 6), '(2, 4, 5), '(2, 4, 6)]

>>> :kind! Eval (LiftA3 Tuple3 ('Right 5) ('Right 6) ('Left "fail"))
Eval (LiftA3 Tuple3 ('Right 5) ('Right 6) ('Left "fail")) :: Either
                                                               TL.Symbol (Natural, Natural, c)
= 'Left "fail"

Instances

type Eval (LiftA3 f2 fa fb fc :: f1 b -> Type)

Defined in Fcf.Control.Monad

type Eval (LiftA3 f2 fa fb fc :: f1 b -> Type) = Eval (Eval (Eval (Map (App3 f2) fa) <*> fb) <*> fc)

data LiftA4 :: (a -> b -> c -> d -> Exp e) -> f a -> f b -> f c -> f d -> Exp (f e)

Type level LiftA4.

Instances

type Eval (LiftA4 f2 fa fb fc fd :: f1 b -> Type)

Defined in Fcf.Control.Monad

type Eval (LiftA4 f2 fa fb fc fd :: f1 b -> Type) = Eval (Eval (Eval (Eval (Map (App4 f2) fa) <*> fb) <*> fc) <*> fd)

data LiftA5 :: (a -> b -> c -> d -> e -> Exp g) -> f a -> f b -> f c -> f d -> f e -> Exp (f g)

Type level LiftA5.

Instances

type Eval (LiftA5 f2 fa fb fc fd fe :: f1 b -> Type)

Defined in Fcf.Control.Monad

type Eval (LiftA5 f2 fa fb fc fd fe :: f1 b -> Type) = Eval (Eval (Eval (Eval (Eval (Map (App5 f2) fa) <*> fb) <*> fc) <*> fd) <*> fe)

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

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

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) :: [Natural]
= '[7, 8, 8, 9, 9, 10]

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

Instances

type Eval ('Identity a2 >>= f :: Identity b -> Type)

Defined in Fcf.Control.Monad

type Eval ('Identity a2 >>= f :: Identity b -> Type) = Eval (f a2)

type Eval (('Nothing :: Maybe a) >>= f :: Maybe b -> Type)

Defined in Fcf.Control.Monad

type Eval (('Nothing :: Maybe a) >>= f :: Maybe b -> Type) = 'Nothing :: Maybe b

type Eval ('Just a2 >>= f :: Maybe b -> Type)

Defined in Fcf.Control.Monad

type Eval ('Just a2 >>= f :: Maybe b -> Type) = Eval (f a2)

type Eval ((x ': xs) >>= f :: [b] -> Type)

Defined in Fcf.Control.Monad

type Eval ((x ': xs) >>= f :: [b] -> Type) = Eval ((f @@ x) ++ Eval (xs >>= f))

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

Defined in Fcf.Control.Monad

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

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

Defined in Fcf.Control.Monad

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

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

Defined in Fcf.Control.Monad

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

type Eval ('(u, a2) >>= k2 :: (k1, b) -> Type)

Defined in Fcf.Control.Monad

type Eval ('(u, a2) >>= k2 :: (k1, b) -> Type) = Eval ('(u, Id :: b -> b -> Type) <*> Eval (k2 a2))

type Eval ('(u, v, a2) >>= k3 :: (k1, k2, b) -> Type)

Defined in Fcf.Control.Monad

type Eval ('(u, v, a2) >>= k3 :: (k1, k2, b) -> Type) = Eval ('(u, v, Id :: b -> b -> Type) <*> Eval (k3 a2))

type Eval ('(u, v, w, a2) >>= k4 :: (k1, k2, k3, b) -> Type)

Defined in Fcf.Control.Monad

type Eval ('(u, v, w, a2) >>= k4 :: (k1, k2, k3, b) -> Type) = Eval ('(u, v, w, Id :: b -> b -> Type) <*> Eval (k4 a2))

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

Type level >>

Example

>>> :kind! Eval ( 'Just 1 >> 'Just 2)
Eval ( 'Just 1 >> 'Just 2) :: Maybe Natural
= 'Just 2
>>> :kind! Eval ( 'Nothing >> 'Just 2)
Eval ( 'Nothing >> 'Just 2) :: Maybe Natural
= 'Nothing

Instances

type Eval (m2 >> k :: m1 b -> Type)

Defined in Fcf.Control.Monad

type Eval (m2 >> k :: m1 b -> Type) = Eval (m2 >>= (ConstFn k :: a -> m1 b -> Type))

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

MapM

Example

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

type Eval (MapM f2 ta :: f1 (t a1) -> Type)

Defined in Fcf.Control.Monad

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

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

ForM = Flip MapM

Instances

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

Defined in Fcf.Control.Monad

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

data FoldlM :: (b -> a -> Exp (m b)) -> b -> t a -> Exp (m b)

FoldlM

Example

>>> import GHC.TypeLits as TL (Symbol, type (-))
>>> data Lambda :: Nat -> Nat -> Exp (Either Symbol Natural)
>>> type instance Eval (Lambda a b) = If (Eval (a >= b)) ('Right (a TL.- b)) ('Left "Nat cannot be negative")
>>> :kind! Eval (FoldlM Lambda 5 '[1,1,1])
Eval (FoldlM Lambda 5 '[1,1,1]) :: Either Symbol Natural
= 'Right 2
>>> :kind! Eval (FoldlM Lambda 5 '[1,4,1])
Eval (FoldlM Lambda 5 '[1,4,1]) :: Either Symbol Natural
= 'Left "Nat cannot be negative"

Instances

type Eval (FoldlM f z0 xs :: m b -> Type)

Defined in Fcf.Control.Monad

type Eval (FoldlM f z0 xs :: m b -> Type) = Eval (Eval (Foldr (FoldlMHelper f) (Return :: b -> m b -> Type) xs) z0)

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

Traverse

Example

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

Instances

type Eval (Traverse f2 ('Right x :: Either a1 a3) :: f1 (Either a1 a2) -> Type)

Defined in Fcf.Control.Monad

type Eval (Traverse f2 ('Right x :: Either a1 a3) :: f1 (Either a1 a2) -> Type) = Eval (Map (Pure1 ('Right :: a2 -> Either a1 a2)) (Eval (f2 x)))

type Eval (Traverse f2 ('Left e :: Either a1 a2) :: f1 (Either a1 b) -> Type)

Defined in Fcf.Control.Monad

type Eval (Traverse f2 ('Left e :: Either a1 a2) :: f1 (Either a1 b) -> Type) = Eval (Return ('Left e :: Either a1 b) :: f1 (Either a1 b) -> Type)

type Eval (Traverse f2 ('Node x ts) :: f1 (Tree b) -> Type)

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

type Eval (Traverse f2 ('Just x) :: f1 (Maybe a1) -> Type)

Defined in Fcf.Control.Monad

type Eval (Traverse f2 ('Just x) :: f1 (Maybe a1) -> Type) = Eval (Map (Pure1 ('Just :: a1 -> Maybe a1)) (Eval (f2 x)))

type Eval (Traverse f2 ('Nothing :: Maybe a) :: f1 (Maybe b) -> Type)

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 '(x, y) :: f1 (a1, a2) -> Type)

Defined in Fcf.Control.Monad

type Eval (Traverse f2 '(x, y) :: f1 (a1, a2) -> Type) = Eval (Map (Tuple2 x :: a2 -> (a1, a2) -> Type) (Eval (f2 y)))

type Eval (Traverse f2 lst :: f1 [b] -> Type)

Defined in Fcf.Control.Monad

type Eval (Traverse f2 lst :: f1 [b] -> Type) = Eval (Foldr (ConsHelper f2) (Eval (Return ('[] :: [b]) :: f1 [b] -> Type)) lst)

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

Sequence

Example

>>> :kind! Eval (Sequence ('Just ('Right 5)))
Eval (Sequence ('Just ('Right 5))) :: Either a (Maybe Natural)
= 'Right ('Just 5)

>>> :kind! Eval (Sequence '[ 'Just 3, 'Just 5, 'Just 7])
Eval (Sequence '[ 'Just 3, 'Just 5, 'Just 7]) :: Maybe [Natural]
= 'Just '[3, 5, 7]

>>> :kind! Eval (Sequence '[ 'Just 3, 'Nothing, 'Just 7])
Eval (Sequence '[ 'Just 3, 'Nothing, 'Just 7]) :: Maybe [Natural]
= 'Nothing

>>> :kind! Eval (Sequence '[ '[1,2], '[3,4]])
Eval (Sequence '[ '[1,2], '[3,4]]) :: [[Natural]]
= '[ '[1, 3], '[1, 4], '[2, 3], '[2, 4]]

Instances

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

Defined in Fcf.Control.Monad

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

data Id :: a -> Exp a

Id function correspondes to term level id-function.

Instances

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

Defined in Fcf.Control.Monad

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

data App2 :: (a -> b -> c) -> a -> Exp (b -> c)

Needed by LiftA2 instance to partially apply function

Instances

type Eval (App2 f a2 :: (b -> c) -> Type)

Defined in Fcf.Control.Monad

type Eval (App2 f a2 :: (b -> c) -> Type) = f a2

data App3 :: (a -> b -> c -> d) -> a -> Exp (b -> Exp (c -> d))

Needed by LiftA3 instance to partially apply function

Instances

type Eval (App3 f a2 :: (b -> Exp (c -> d)) -> Type)

Defined in Fcf.Control.Monad

type Eval (App3 f a2 :: (b -> Exp (c -> d)) -> Type) = Pure2 f a2

data App4 :: (a -> b -> c -> d -> e) -> a -> Exp (b -> Exp (c -> Exp (d -> e)))

Needed by LiftA4 instance to partially apply function

Instances

type Eval (App4 f a3 :: (a1 -> Exp (b -> Exp (c -> d))) -> Type)

Defined in Fcf.Control.Monad

type Eval (App4 f a3 :: (a1 -> Exp (b -> Exp (c -> d))) -> Type) = App3 (f a3)

data App5 :: (a -> b -> c -> d -> e -> g) -> a -> Exp (b -> Exp (c -> Exp (d -> Exp (e -> g))))

Needed by LiftA5 instance to partially apply function

Instances

type Eval (App5 f a3 :: (a1 -> Exp (b -> Exp (c -> Exp (d -> e)))) -> Type)

Defined in Fcf.Control.Monad

type Eval (App5 f a3 :: (a1 -> Exp (b -> Exp (c -> Exp (d -> e)))) -> Type) = App4 (f a3)

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

Helper for the [] applicative instance.

Instances

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

Defined in Fcf.Control.Monad

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

type Eval (Star_ f (a2 ': as) :: [b] -> Type)

Defined in Fcf.Control.Monad

type Eval (Star_ f (a2 ': as) :: [b] -> Type) = Eval (f a2) ': Eval (Star_ f as)

data FoldlMHelper :: (b -> a -> Exp (m b)) -> a -> (b -> Exp (m b)) -> Exp (b -> Exp (m b))

Helper for FoldlM

Instances

type Eval (FoldlMHelper f a2 b2 :: (a1 -> Exp (m a1)) -> Type)

Defined in Fcf.Control.Monad

type Eval (FoldlMHelper f a2 b2 :: (a1 -> Exp (m a1)) -> Type) = Flip ((>>=) :: m a1 -> (a1 -> Exp (m a1)) -> m a1 -> Type) b2 <=< Flip f a2

data ConsHelper :: (a -> Exp (f b)) -> a -> f [b] -> Exp (f [b])

Helper for [] traverse

Instances

type Eval (ConsHelper f2 x ys :: f1 [a1] -> Type)

Defined in Fcf.Control.Monad

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

data Plus1 :: Nat -> Exp Nat

For Applicative documentation example

Instances

type Eval (Plus1 n :: Nat -> Type)

Defined in Fcf.Control.Monad

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

data Plus2 :: Nat -> Exp Nat

For Applicative documentation example

Instances

type Eval (Plus2 n :: Nat -> Type)

Defined in Fcf.Control.Monad

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

data Plus2M :: Nat -> Exp [Nat]

For the example. Turn an input number to list of two numbers of a bit larger numbers.

Instances

type Eval (Plus2M n :: [Nat] -> Type)

Defined in Fcf.Control.Monad

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

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

Part of an example

Instances

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

Defined in Fcf.Control.Monad

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

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

Part of an example

Instances

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

Defined in Fcf.Control.Monad

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

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

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

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

Defined in Fcf.Control.Monad

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