generics-mrsop-2.0.0: Generic Programming with Mutually Recursive Sums of Products.

Safe HaskellSafe
LanguageHaskell2010

Generics.MRSOP.Base.NS

Contents

Description

Standard representation of n-ary sums.

Synopsis
  • data NS :: (k -> *) -> [k] -> * where
  • mapNS :: (f :-> g) -> NS f ks -> NS g ks
  • mapNSM :: Monad m => (forall x. f x -> m (g x)) -> NS f ks -> m (NS g ks)
  • elimNS :: (forall x. f x -> a) -> NS f ks -> a
  • zipNS :: MonadPlus m => NS ki xs -> NS kj xs -> m (NS (ki :*: kj) xs)
  • cataNS :: (forall x xs. f x -> r (x ': xs)) -> (forall x xs. r xs -> r (x ': xs)) -> NS f xs -> r xs
  • eqNS :: (forall x. p x -> p x -> Bool) -> NS p xs -> NS p xs -> Bool

Documentation

data NS :: (k -> *) -> [k] -> * where Source #

Indexed n-ary sums. This is analogous to the Any datatype in Agda. Combinations of Here and Theres are also called injections.

Constructors

There :: NS p xs -> NS p (x ': xs) 
Here :: p x -> NS p (x ': xs) 
Instances
ShowHO phi => ShowHO (NS phi :: [k] -> Type) Source # 
Instance details

Defined in Generics.MRSOP.Base.NS

Methods

showHO :: NS phi k0 -> String Source #

EqHO phi => EqHO (NS phi :: [k] -> Type) Source # 
Instance details

Defined in Generics.MRSOP.Base.NS

Methods

eqHO :: NS phi k0 -> NS phi k0 -> Bool Source #

EqHO phi => Eq (NS phi xs) Source # 
Instance details

Defined in Generics.MRSOP.Base.NS

Methods

(==) :: NS phi xs -> NS phi xs -> Bool #

(/=) :: NS phi xs -> NS phi xs -> Bool #

ShowHO phi => Show (NS phi xs) Source # 
Instance details

Defined in Generics.MRSOP.Base.NS

Methods

showsPrec :: Int -> NS phi xs -> ShowS #

show :: NS phi xs -> String #

showList :: [NS phi xs] -> ShowS #

Map, Zip and Elim

mapNS :: (f :-> g) -> NS f ks -> NS g ks Source #

Maps over a sum

mapNSM :: Monad m => (forall x. f x -> m (g x)) -> NS f ks -> m (NS g ks) Source #

Maps a monadic function over a sum

elimNS :: (forall x. f x -> a) -> NS f ks -> a Source #

Eliminates a sum

zipNS :: MonadPlus m => NS ki xs -> NS kj xs -> m (NS (ki :*: kj) xs) Source #

Combines two sums. Note that we have to fail if they are constructed from different injections.

Catamorphism

cataNS :: (forall x xs. f x -> r (x ': xs)) -> (forall x xs. r xs -> r (x ': xs)) -> NS f xs -> r xs Source #

Consumes a value of type NS

Equality

eqNS :: (forall x. p x -> p x -> Bool) -> NS p xs -> NS p xs -> Bool Source #

Compares two values of type NS using the provided function in case they are made of the same injection.