Data.Binder.Unfix

Functors of endofunctors

Simple functors

type (~>) f g = forall a. f a -> g a

class forall f. Functor f => Functor (h f) => Functor1 (h :: (* -> *) -> * -> *) where

Methods

fmap1 :: (Functor f, Functor g) => (f ~> g) -> h f ~> h g

fmap1 :: (Generic1 (h f), Generic1 (h g), GFunctor1 (Rep1 (h f)) (Rep1 (h g)) f g, Functor f, Functor g) => (f ~> g) -> h f ~> h g

Instances

Functor1 Var

Methods

fmap1 :: (Functor f, Functor g) => (f ~> g) -> Var f ~> Var g

(Functor1 h, Functor1 j) => Functor1 (Either2 h j)

Methods

fmap1 :: (Functor f, Functor g) => (f ~> g) -> Either2 h j f ~> Either2 h j g

class Functor1 h => Strong1 h where

The intuition behind Strong1 h is that h acts on monads. Indeed if f=g=m is a monad, then x -> strength1 x join :: h m (m a) -> h m a. This is a limited explanation, but I don't know much more yet.

As additional background, for the curious programmer: from a mathematical point of view, strenght1 is a functorial strength. For regular functors, a strength is a function (f a, b) -> f (a, b). But for regular functor, there is always such a strength: (fa, b) -> (, b) $ fa (this strength is implicitly but critically used in the definition of the do-notation). However functors of endofunctors don't necessarily have a strength (in fact Var below doesn't have one). So we need an additional type class to record that functors are strong.

Like in the infamous phrase "a monad is a monoid in the category of endofunctors", the natural product of endofunctors is composition. It is not hard to verify that, up to map1, the type of strength1 is equivalent to h f Compose g ~> h (f Compose g). We choose this formulation because it avoids annotations to convert between Compose f g a and f (g a).

In any case, this is a natural notion from a mathematics point of view. And not as ad hoc as it may appear at first glance. However, because we wouldn't have interesting instance without it, we restrict g to be an applicative functor. There does not seem to be a need for f to be applicative as well, therefore we depart from usual mathematical practice and only restrict g.

Methods

strength1 :: (Functor f, Applicative g, Functor i) => h f (g a) -> (forall b. f (g b) -> i b) -> h i a

strength1 :: (Generic1 (h f), Generic1 (h i), GStrong1 (Rep1 (h f)) (Rep1 (h i)) f g i, Functor f, Applicative g, Functor i) => h f (g a) -> (forall b. f (g b) -> i b) -> h i a

Instances

(Strong1 h, Strong1 j) => Strong1 (Either2 h j)

Methods

strength1 :: (Functor f, Applicative g, Functor i) => Either2 h j f (g a) -> (forall b. f (g b) -> i b) -> Either2 h j i a

data Either2 (h :: (* -> *) -> * -> *) (j :: (* -> *) -> * -> *) (f :: * -> *) (a :: *)

Constructors

Left2 (h f a)

Right2 (j f a)

Instances

Strong1 h => Monad (Mu (Either2 Var h))

Methods

(>>=) :: Mu (Either2 Var h) a -> (a -> Mu (Either2 Var h) b) -> Mu (Either2 Var h) b

(>>) :: Mu (Either2 Var h) a -> Mu (Either2 Var h) b -> Mu (Either2 Var h) b

return :: a -> Mu (Either2 Var h) a

fail :: String -> Mu (Either2 Var h) a

Strong1 h => Applicative (Mu (Either2 Var h))

Methods

pure :: a -> Mu (Either2 Var h) a

(<*>) :: Mu (Either2 Var h) (a -> b) -> Mu (Either2 Var h) a -> Mu (Either2 Var h) b

liftA2 :: (a -> b -> c) -> Mu (Either2 Var h) a -> Mu (Either2 Var h) b -> Mu (Either2 Var h) c

(*>) :: Mu (Either2 Var h) a -> Mu (Either2 Var h) b -> Mu (Either2 Var h) b

(<*) :: Mu (Either2 Var h) a -> Mu (Either2 Var h) b -> Mu (Either2 Var h) a

Generic1 (Either2 h j f :: * -> *)

Associated Types

type Rep1 (Either2 h j f) :: k -> *

Methods

from1 :: Either2 h j f a -> Rep1 (Either2 h j f) a

to1 :: Rep1 (Either2 h j f) a -> Either2 h j f a

(Strong1 h, Strong1 j) => Strong1 (Either2 h j)

Methods

strength1 :: (Functor f, Applicative g, Functor i) => Either2 h j f (g a) -> (forall b. f (g b) -> i b) -> Either2 h j i a

(Functor1 h, Functor1 j) => Functor1 (Either2 h j)

Methods

fmap1 :: (Functor f, Functor g) => (f ~> g) -> Either2 h j f ~> Either2 h j g

(Functor (h f), Functor (j f)) => Functor (Either2 h j f)

Methods

fmap :: (a -> b) -> Either2 h j f a -> Either2 h j f b

(<$) :: a -> Either2 h j f b -> Either2 h j f a

(Eq (h f a), Eq (j f a)) => Eq (Either2 h j f a)

Methods

(==) :: Either2 h j f a -> Either2 h j f a -> Bool

(/=) :: Either2 h j f a -> Either2 h j f a -> Bool

type Rep1 (Either2 h j f :: * -> *)

type Rep1 (Either2 h j f :: * -> *) = D1 (MetaData "Either2" "Data.Binder.Unfix" "unfix-binders-0.1.0-6a1TrK3gzGp6zyFJV1iInG" False) (C1 (MetaCons "Left2" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec1 (h f))) :+: C1 (MetaCons "Right2" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec1 (j f))))

data Var (f :: * -> *) (a :: *)

Constructors

Var a

Instances

Functor1 Var

Methods

fmap1 :: (Functor f, Functor g) => (f ~> g) -> Var f ~> Var g

Strong1 h => Monad (Mu (Either2 Var h))

Methods

(>>=) :: Mu (Either2 Var h) a -> (a -> Mu (Either2 Var h) b) -> Mu (Either2 Var h) b

(>>) :: Mu (Either2 Var h) a -> Mu (Either2 Var h) b -> Mu (Either2 Var h) b

return :: a -> Mu (Either2 Var h) a

fail :: String -> Mu (Either2 Var h) a

Functor (Var f)

Methods

fmap :: (a -> b) -> Var f a -> Var f b

(<$) :: a -> Var f b -> Var f a

Strong1 h => Applicative (Mu (Either2 Var h))

Methods

pure :: a -> Mu (Either2 Var h) a

(<*>) :: Mu (Either2 Var h) (a -> b) -> Mu (Either2 Var h) a -> Mu (Either2 Var h) b

liftA2 :: (a -> b -> c) -> Mu (Either2 Var h) a -> Mu (Either2 Var h) b -> Mu (Either2 Var h) c

(*>) :: Mu (Either2 Var h) a -> Mu (Either2 Var h) b -> Mu (Either2 Var h) b

(<*) :: Mu (Either2 Var h) a -> Mu (Either2 Var h) b -> Mu (Either2 Var h) a

Generic1 (Var f :: * -> *)

Associated Types

type Rep1 (Var f) :: k -> *

Methods

from1 :: Var f a -> Rep1 (Var f) a

to1 :: Rep1 (Var f) a -> Var f a

Eq a => Eq (Var f a)

Methods

(==) :: Var f a -> Var f a -> Bool

(/=) :: Var f a -> Var f a -> Bool

type Rep1 (Var f :: * -> *)

type Rep1 (Var f :: * -> *) = D1 (MetaData "Var" "Data.Binder.Unfix" "unfix-binders-0.1.0-6a1TrK3gzGp6zyFJV1iInG" False) (C1 (MetaCons "Var" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) Par1))

newtype Assigned (r :: *) (v :: *) (a :: *)

Assigned r v a represent the computation of a result r parametrised by an assignment of values of type v to each element of a. It is a functor (in a).

Its usefulness derives from the fact that given a Functor1 F, an algebra of F on Assigned R V yields, via catamorphism (see cata1) an algebra of the monad Mu F. That is a compositional interpreter for Mu F in the type R. This is used a lot.

You may have noticed that Assigned r r is a monad (the continuation monad Cont r, in fact). As a matter of fact Assigned is an indexed monad (up, possibly, to the order of its arguments) which is related to delimited continuation. Neither of this fact are useful for our purposes

Constructors

Assigned ((a -> v) -> r)

Instances

Functor (Assigned r v)

Methods

fmap :: (a -> b) -> Assigned r v a -> Assigned r v b

(<$) :: a -> Assigned r v b -> Assigned r v a

Parametric functors

class forall f p. forall q. Functor (f q) => Functor (h f p) => PFunctor1 (h :: (k -> * -> *) -> k -> * -> *)

Minimal complete definition

pfmap1

Non-uniform fixed point

Simple fixed point

newtype Mu (h :: (* -> *) -> * -> *) (a :: *)

Constructors

Roll

Fields

• unroll :: h (Mu h) a

Instances

Strong1 h => Monad (Mu (Either2 Var h))

Methods

(>>=) :: Mu (Either2 Var h) a -> (a -> Mu (Either2 Var h) b) -> Mu (Either2 Var h) b

(>>) :: Mu (Either2 Var h) a -> Mu (Either2 Var h) b -> Mu (Either2 Var h) b

return :: a -> Mu (Either2 Var h) a

fail :: String -> Mu (Either2 Var h) a

Functor1 h => Functor (Mu h)

Methods

fmap :: (a -> b) -> Mu h a -> Mu h b

(<$) :: a -> Mu h b -> Mu h a

Strong1 h => Applicative (Mu (Either2 Var h))

Methods

pure :: a -> Mu (Either2 Var h) a

(<*>) :: Mu (Either2 Var h) (a -> b) -> Mu (Either2 Var h) a -> Mu (Either2 Var h) b

liftA2 :: (a -> b -> c) -> Mu (Either2 Var h) a -> Mu (Either2 Var h) b -> Mu (Either2 Var h) c

(*>) :: Mu (Either2 Var h) a -> Mu (Either2 Var h) b -> Mu (Either2 Var h) b

(<*) :: Mu (Either2 Var h) a -> Mu (Either2 Var h) b -> Mu (Either2 Var h) a

(Eq a, forall b (f :: * -> *). (Eq b, forall c. Eq c => Eq (f c)) => Eq (h f b)) => Eq (Mu h a)

Methods

(==) :: Mu h a -> Mu h a -> Bool

(/=) :: Mu h a -> Mu h a -> Bool

cata1 :: (Functor1 h, Functor f) => (h f ~> f) -> Mu h ~> f

Mutually recursive fixed point

data MMu (h :: (k -> * -> *) -> k -> * -> *) (p :: k) (a :: *)

Instances

PFunctor1 h => Functor (MMu h p)

Methods

fmap :: (a -> b) -> MMu h p a -> MMu h p b

(<$) :: a -> MMu h p b -> MMu h p a

pcata1 :: (PFunctor1 h, forall q. Functor (f q)) => (forall q. h f q ~> f q) -> MMu h p ~> f p

Deriving instances

Deriving Functor1

class GFunctor1 (h :: * -> *) (j :: * -> *) (f :: * -> *) (g :: * -> *)

A class for deriving Functor1 instances generic types. We would really need a Generic2 framework (because our types have two arguments). Instead we use an encoding trick, related to the way lenses are defined in the lens library. This trick is due to Csongor Kiss, and documented in this blog post.

The intuition is that the first two argument h and j of the type class, are stand-ins for h' f and h' g.

Minimal complete definition

gfmap1

Instances

GFunctor1 Par1 Par1 f g

Methods

gfmap1 :: (f ~> g) -> Par1 ~> Par1

GFunctor1 f g f g

Methods

gfmap1 :: (f ~> g) -> f ~> g

GFunctor1 (V1 :: * -> *) (V1 :: * -> *) f g

Methods

gfmap1 :: (f ~> g) -> V1 ~> V1

GFunctor1 (U1 :: * -> *) (U1 :: * -> *) f g

Methods

gfmap1 :: (f ~> g) -> U1 ~> U1

(Functor1 h, Functor f, Functor g) => GFunctor1 (Rec1 (h f)) (Rec1 (h g)) f g

Methods

gfmap1 :: (f ~> g) -> Rec1 (h f) ~> Rec1 (h g)

GFunctor1 (Rec1 i) (Rec1 i) f g

Methods

gfmap1 :: (f ~> g) -> Rec1 i ~> Rec1 i

GFunctor1 (Rec1 f) (Rec1 g) f g

Methods

gfmap1 :: (f ~> g) -> Rec1 f ~> Rec1 g

GFunctor1 (K1 i c :: * -> *) (K1 i c :: * -> *) g f

Methods

gfmap1 :: (g ~> f) -> K1 i c ~> K1 i c

(GFunctor1 h1 j1 f g, GFunctor1 h2 j2 f g) => GFunctor1 (h1 :+: h2) (j1 :+: j2) f g

Methods

gfmap1 :: (f ~> g) -> (h1 :+: h2) ~> (j1 :+: j2)

(GFunctor1 h1 j1 f g, GFunctor1 h2 j2 f g) => GFunctor1 (h1 :*: h2) (j1 :*: j2) f g

Methods

gfmap1 :: (f ~> g) -> (h1 :*: h2) ~> (j1 :*: j2)

GFunctor1 h j f g => GFunctor1 (M1 i c h) (M1 i c j) f g

Methods

gfmap1 :: (f ~> g) -> M1 i c h ~> M1 i c j

(GFunctor1 h1 j1 f g, GFunctor1 h2 j2 f g, Functor h1) => GFunctor1 (h1 :.: h2) (j1 :.: j2) f g

Methods

gfmap1 :: (f ~> g) -> (h1 :.: h2) ~> (j1 :.: j2)

Deriving Strong1

class GStrong1 (h :: * -> *) (j :: * -> *) (f :: * -> *) (g :: * -> *) (i :: * -> *)

A class for deriving Strong1 instances generic types. See the documentation of Functor1 for details on the encoding. You should read h and j below as being h' f and h' i, respectively.

Minimal complete definition

gstrength1

Instances

GStrong1 f i f g i

Methods

gstrength1 :: f (g a) -> (forall b. f (g b) -> i b) -> i a

GStrong1 (V1 :: * -> *) (V1 :: * -> *) f g i

Methods

gstrength1 :: V1 (g a) -> (forall b. f (g b) -> i b) -> V1 a

GStrong1 (U1 :: * -> *) (U1 :: * -> *) f g i

Methods

gstrength1 :: U1 (g a) -> (forall b. f (g b) -> i b) -> U1 a

GStrong1 (Rec1 f) (Rec1 i) f g i

Methods

gstrength1 :: Rec1 f (g a) -> (forall b. f (g b) -> i b) -> Rec1 i a

(Strong1 h, Functor f, Applicative g, Functor i) => GStrong1 (Rec1 (h f)) (Rec1 (h i)) f g i

Methods

gstrength1 :: Rec1 (h f) (g a) -> (forall b. f (g b) -> i b) -> Rec1 (h i) a

GStrong1 (K1 m c :: * -> *) (K1 m c :: * -> *) g f i

Methods

gstrength1 :: K1 m c (f a) -> (forall b. g (f b) -> i b) -> K1 m c a

(GStrong1 h1 j1 f g i, GStrong1 h2 j2 f g i) => GStrong1 (h1 :+: h2) (j1 :+: j2) f g i

Methods

gstrength1 :: (h1 :+: h2) (g a) -> (forall b. f (g b) -> i b) -> (j1 :+: j2) a

(GStrong1 h1 j1 f g i, GStrong1 h2 j2 f g i) => GStrong1 (h1 :*: h2) (j1 :*: j2) f g i

Methods

gstrength1 :: (h1 :*: h2) (g a) -> (forall b. f (g b) -> i b) -> (j1 :*: j2) a

GStrong1 h j f g i => GStrong1 (M1 m c h) (M1 m c j) f g i

Methods

gstrength1 :: M1 m c h (g a) -> (forall b. f (g b) -> i b) -> M1 m c j a

(GStrong1 h1 j1 f g i, Traversable t, Functor h1, Traversable t, Applicative g) => GStrong1 (h1 :.: t) (j1 :.: t) f g i

Methods

gstrength1 :: (h1 :.: t) (g a) -> (forall b. f (g b) -> i b) -> (j1 :.: t) a