verifiable-expressions-0.5.0: An intermediate language for Hoare logic style verification.

Safe HaskellSafe
LanguageHaskell2010

Language.Expression

Description

Implements higher-ranked equivalents of Functor, Monad, Foldable and Traversable.

Synopsis

Documentation

class HFunctor (h :: (u -> *) -> u -> *) where Source #

Higher-ranked analogue of Functor.

Minimal complete definition

Nothing

Methods

hmap :: (forall b. t b -> t' b) -> h t a -> h t' a Source #

Higher-ranked analogue of fmap. Has a default implementation in terms of htraverse for HTraversable h.

hmap :: HTraversable h => (forall b. t b -> t' b) -> h t a -> h t' a Source #

Higher-ranked analogue of fmap. Has a default implementation in terms of htraverse for HTraversable h.

Instances
HFunctor (Reverse :: (u -> Type) -> u -> Type) Source # 
Instance details

Defined in Language.Expression

Methods

hmap :: (forall (b :: u0). t b -> t' b) -> Reverse t a -> Reverse t' a Source #

HFunctor (ReaderT r :: (u -> Type) -> u -> Type) Source # 
Instance details

Defined in Language.Expression

Methods

hmap :: (forall (b :: u0). t b -> t' b) -> ReaderT r t a -> ReaderT r t' a Source #

HFunctor (Sum f :: (u -> Type) -> u -> Type) Source # 
Instance details

Defined in Language.Expression

Methods

hmap :: (forall (b :: u0). t b -> t' b) -> Sum f t a -> Sum f t' a Source #

HFunctor (Product f :: (u -> Type) -> u -> Type) Source # 
Instance details

Defined in Language.Expression

Methods

hmap :: (forall (b :: u0). t b -> t' b) -> Product f t a -> Product f t' a Source #

HFunctor h => HFunctor (HFree h :: (u -> Type) -> u -> Type) Source # 
Instance details

Defined in Language.Expression

Methods

hmap :: (forall (b :: u0). t b -> t' b) -> HFree h t a -> HFree h t' a Source #

HFunctor (BV g :: (u -> Type) -> u -> Type) Source # 
Instance details

Defined in Language.Expression.Scope

Methods

hmap :: (forall (b :: u0). t b -> t' b) -> BV g t a -> BV g t' a Source #

HDuofunctor h => HFunctor (SFree h :: (u -> Type) -> u -> Type) Source # 
Instance details

Defined in Language.Expression.Scope

Methods

hmap :: (forall (b :: u0). t b -> t' b) -> SFree h t a -> SFree h t' a Source #

Functor f => HFunctor (Compose f :: (u -> Type) -> u -> Type) Source # 
Instance details

Defined in Language.Expression

Methods

hmap :: (forall (b :: u0). t b -> t' b) -> Compose f t a -> Compose f t' a Source #

HFunctor h => HFunctor (Scope g h :: (u -> Type) -> u -> Type) Source # 
Instance details

Defined in Language.Expression.Scope

Methods

hmap :: (forall (b :: u0). t b -> t' b) -> Scope g h t a -> Scope g h t' a Source #

HFunctor h => HFunctor (Scoped h f :: (u -> Type) -> u -> Type) Source # 
Instance details

Defined in Language.Expression.Scope

Methods

hmap :: (forall (b :: u0). t b -> t' b) -> Scoped h f t a -> Scoped h f t' a Source #

HFunctor (GeneralOp op :: (u -> Type) -> u -> Type) Source # 
Instance details

Defined in Language.Expression.GeneralOp

Methods

hmap :: (forall (b :: u0). t b -> t' b) -> GeneralOp op t a -> GeneralOp op t' a Source #

HFunctor SimpleOp Source # 
Instance details

Defined in Language.Expression.Example

Methods

hmap :: (forall (b :: u). t b -> t' b) -> SimpleOp t a -> SimpleOp t' a Source #

HFunctor LogicOp Source # 
Instance details

Defined in Language.Expression.Prop

Methods

hmap :: (forall (b :: u). t b -> t' b) -> LogicOp t a -> LogicOp t' a Source #

HFunctor (ExceptT e :: (Type -> Type) -> Type -> Type) Source # 
Instance details

Defined in Language.Expression

Methods

hmap :: (forall (b :: u). t b -> t' b) -> ExceptT e t a -> ExceptT e t' a Source #

HFunctor (StateT s :: (Type -> Type) -> Type -> Type) Source # 
Instance details

Defined in Language.Expression

Methods

hmap :: (forall (b :: u). t b -> t' b) -> StateT s t a -> StateT s t' a Source #

HFunctor (StateT s :: (Type -> Type) -> Type -> Type) Source # 
Instance details

Defined in Language.Expression

Methods

hmap :: (forall (b :: u). t b -> t' b) -> StateT s t a -> StateT s t' a Source #

HFunctor (WriterT w :: (Type -> Type) -> Type -> Type) Source # 
Instance details

Defined in Language.Expression

Methods

hmap :: (forall (b :: u). t b -> t' b) -> WriterT w t a -> WriterT w t' a Source #

HFunctor (WriterT w :: (Type -> Type) -> Type -> Type) Source # 
Instance details

Defined in Language.Expression

Methods

hmap :: (forall (b :: u). t b -> t' b) -> WriterT w t a -> WriterT w t' a Source #

(HFunctor op, HFunctor (OpChoice ops)) => HFunctor (OpChoice (op ': ops) :: (Type -> Type) -> Type -> Type) Source # 
Instance details

Defined in Language.Expression.Choice

Methods

hmap :: (forall (b :: u). t b -> t' b) -> OpChoice (op ': ops) t a -> OpChoice (op ': ops) t' a Source #

HFunctor (OpChoice ([] :: [(Type -> Type) -> Type -> Type])) Source # 
Instance details

Defined in Language.Expression.Choice

Methods

hmap :: (forall (b :: u). t b -> t' b) -> OpChoice [] t a -> OpChoice [] t' a Source #

HFunctor (OpChoice ops) => HFunctor (HFree' ops :: (Type -> Type) -> Type -> Type) Source # 
Instance details

Defined in Language.Expression.Choice

Methods

hmap :: (forall (b :: u). t b -> t' b) -> HFree' ops t a -> HFree' ops t' a Source #

class HPointed h where Source #

Half of the higher-ranked analogue of Monad.

Methods

hpure :: t a -> h t a Source #

Higher-ranked analogue of pure or return.

Instances
HPointed (Reverse :: (k -> Type) -> k -> Type) Source # 
Instance details

Defined in Language.Expression

Methods

hpure :: t a -> Reverse t a Source #

HPointed (ReaderT r :: (k -> Type) -> k -> Type) Source # 
Instance details

Defined in Language.Expression

Methods

hpure :: t a -> ReaderT r t a Source #

HPointed (Sum f :: (k -> Type) -> k -> Type) Source # 
Instance details

Defined in Language.Expression

Methods

hpure :: t a -> Sum f t a Source #

HPointed (HFree h :: (k -> Type) -> k -> Type) Source # 
Instance details

Defined in Language.Expression

Methods

hpure :: t a -> HFree h t a Source #

HPointed (BV g :: (k -> Type) -> k -> Type) Source # 
Instance details

Defined in Language.Expression.Scope

Methods

hpure :: t a -> BV g t a Source #

HPointed (SFree h :: (k -> Type) -> k -> Type) Source # 
Instance details

Defined in Language.Expression.Scope

Methods

hpure :: t a -> SFree h t a Source #

Applicative f => HPointed (Compose f :: (k -> Type) -> k -> Type) Source # 
Instance details

Defined in Language.Expression

Methods

hpure :: t a -> Compose f t a Source #

HPointed h => HPointed (Scope g h :: (k -> Type) -> k -> Type) Source # 
Instance details

Defined in Language.Expression.Scope

Methods

hpure :: t a -> Scope g h t a Source #

HPointed (HFree' ops :: (Type -> Type) -> Type -> Type) Source # 
Instance details

Defined in Language.Expression.Choice

Methods

hpure :: t a -> HFree' ops t a Source #

class HBind h where Source #

Half of the higher-ranked analogue of Monad.

Methods

(^>>=) :: h t a -> (forall b. t b -> h t' b) -> h t' a infixr 1 Source #

Higher-ranked analogue of >>=.

Instances
HBind (Reverse :: (k -> Type) -> k -> Type) Source # 
Instance details

Defined in Language.Expression

Methods

(^>>=) :: Reverse t a -> (forall (b :: k0). t b -> Reverse t' b) -> Reverse t' a Source #

HBind (ReaderT r :: (k -> Type) -> k -> Type) Source # 
Instance details

Defined in Language.Expression

Methods

(^>>=) :: ReaderT r t a -> (forall (b :: k0). t b -> ReaderT r t' b) -> ReaderT r t' a Source #

HBind (Sum f :: (k -> Type) -> k -> Type) Source # 
Instance details

Defined in Language.Expression

Methods

(^>>=) :: Sum f t a -> (forall (b :: k0). t b -> Sum f t' b) -> Sum f t' a Source #

HFunctor h => HBind (HFree h :: (k -> Type) -> k -> Type) Source # 
Instance details

Defined in Language.Expression

Methods

(^>>=) :: HFree h t a -> (forall (b :: k0). t b -> HFree h t' b) -> HFree h t' a Source #

HBind (BV g :: (k -> Type) -> k -> Type) Source # 
Instance details

Defined in Language.Expression.Scope

Methods

(^>>=) :: BV g t a -> (forall (b :: k0). t b -> BV g t' b) -> BV g t' a Source #

HDuofunctor h => HBind (SFree h :: (k -> Type) -> k -> Type) Source # 
Instance details

Defined in Language.Expression.Scope

Methods

(^>>=) :: SFree h t a -> (forall (b :: k0). t b -> SFree h t' b) -> SFree h t' a Source #

Monad f => HBind (Compose f :: (k -> Type) -> k -> Type) Source # 
Instance details

Defined in Language.Expression

Methods

(^>>=) :: Compose f t a -> (forall (b :: k0). t b -> Compose f t' b) -> Compose f t' a Source #

HFunctor (OpChoice ops) => HBind (HFree' ops :: (Type -> Type) -> Type -> Type) Source # 
Instance details

Defined in Language.Expression.Choice

Methods

(^>>=) :: HFree' ops t a -> (forall (b :: k). t b -> HFree' ops t' b) -> HFree' ops t' a Source #

class (HFunctor h, HPointed h, HBind h) => HMonad h Source #

Higher-ranked analogue of Monad.

NB there's no such thing as HApplicative for a reason. Consider f :: h t a -> h t' a -> h (Product t t') a, i.e. the higher-ranked analogue of liftA2 (,) :: f a -> f b -> f (a, b). Unfortunately f can't exist, because Product pairs up values of the same type, and in our constructions, h potentially contains values of many types; a just happens to be the one at the top level. There's no guarantee that the two structures will have the same types inside to pair together.

Instances
HMonad (Reverse :: (k -> Type) -> k -> Type) Source # 
Instance details

Defined in Language.Expression

HMonad (ReaderT r :: (k -> Type) -> k -> Type) Source # 
Instance details

Defined in Language.Expression

HMonad (Sum f :: (k -> Type) -> k -> Type) Source # 
Instance details

Defined in Language.Expression

HFunctor h => HMonad (HFree h :: (k -> Type) -> k -> Type) Source # 
Instance details

Defined in Language.Expression

HMonad (BV g :: (k -> Type) -> k -> Type) Source # 
Instance details

Defined in Language.Expression.Scope

HDuofunctor h => HMonad (SFree h :: (k -> Type) -> k -> Type) Source # 
Instance details

Defined in Language.Expression.Scope

HFunctor (OpChoice ops) => HMonad (HFree' ops :: (Type -> Type) -> Type -> Type) Source # 
Instance details

Defined in Language.Expression.Choice

hliftM :: (HPointed h, HBind h) => (forall b. t b -> t' b) -> h t a -> h t' a Source #

Implements hmap from just an HPointed and HBind instance. Can be used to implement HFunctor for your HMonads that aren't HTraversable.

hjoin :: HBind h => h (h t) a -> h t a Source #

Higher-ranked analogue of join.

class HFunctor h => HTraversable h where Source #

Higher-ranked analogue of Traversable.

Minimal complete definition

htraverse | hsequence

Methods

htraverse :: Applicative f => (forall b. t b -> f (t' b)) -> h t a -> f (h t' a) Source #

Higher-ranked analogue of traverse.

hsequence :: Applicative f => h (Compose f t) a -> f (h t a) Source #

Higher-ranked analogue of sequenceA.

Instances
HTraversable (Reverse :: (u -> Type) -> u -> Type) Source # 
Instance details

Defined in Language.Expression

Methods

htraverse :: Applicative f => (forall (b :: u0). t b -> f (t' b)) -> Reverse t a -> f (Reverse t' a) Source #

hsequence :: Applicative f => Reverse (Compose f t) a -> f (Reverse t a) Source #

HTraversable (Sum f :: (u -> Type) -> u -> Type) Source # 
Instance details

Defined in Language.Expression

Methods

htraverse :: Applicative f0 => (forall (b :: u0). t b -> f0 (t' b)) -> Sum f t a -> f0 (Sum f t' a) Source #

hsequence :: Applicative f0 => Sum f (Compose f0 t) a -> f0 (Sum f t a) Source #

HTraversable (Product f :: (u -> Type) -> u -> Type) Source # 
Instance details

Defined in Language.Expression

Methods

htraverse :: Applicative f0 => (forall (b :: u0). t b -> f0 (t' b)) -> Product f t a -> f0 (Product f t' a) Source #

hsequence :: Applicative f0 => Product f (Compose f0 t) a -> f0 (Product f t a) Source #

HTraversable h => HTraversable (HFree h :: (u -> Type) -> u -> Type) Source # 
Instance details

Defined in Language.Expression

Methods

htraverse :: Applicative f => (forall (b :: u0). t b -> f (t' b)) -> HFree h t a -> f (HFree h t' a) Source #

hsequence :: Applicative f => HFree h (Compose f t) a -> f (HFree h t a) Source #

HTraversable (BV g :: (u -> Type) -> u -> Type) Source # 
Instance details

Defined in Language.Expression.Scope

Methods

htraverse :: Applicative f => (forall (b :: u0). t b -> f (t' b)) -> BV g t a -> f (BV g t' a) Source #

hsequence :: Applicative f => BV g (Compose f t) a -> f (BV g t a) Source #

HDuotraversable h => HTraversable (SFree h :: (u -> Type) -> u -> Type) Source # 
Instance details

Defined in Language.Expression.Scope

Methods

htraverse :: Applicative f => (forall (b :: u0). t b -> f (t' b)) -> SFree h t a -> f (SFree h t' a) Source #

hsequence :: Applicative f => SFree h (Compose f t) a -> f (SFree h t a) Source #

Traversable f => HTraversable (Compose f :: (u -> Type) -> u -> Type) Source # 
Instance details

Defined in Language.Expression

Methods

htraverse :: Applicative f0 => (forall (b :: u0). t b -> f0 (t' b)) -> Compose f t a -> f0 (Compose f t' a) Source #

hsequence :: Applicative f0 => Compose f (Compose f0 t) a -> f0 (Compose f t a) Source #

HTraversable h => HTraversable (Scope g h :: (u -> Type) -> u -> Type) Source # 
Instance details

Defined in Language.Expression.Scope

Methods

htraverse :: Applicative f => (forall (b :: u0). t b -> f (t' b)) -> Scope g h t a -> f (Scope g h t' a) Source #

hsequence :: Applicative f => Scope g h (Compose f t) a -> f (Scope g h t a) Source #

HTraversable h => HTraversable (Scoped h f :: (u -> Type) -> u -> Type) Source # 
Instance details

Defined in Language.Expression.Scope

Methods

htraverse :: Applicative f0 => (forall (b :: u0). t b -> f0 (t' b)) -> Scoped h f t a -> f0 (Scoped h f t' a) Source #

hsequence :: Applicative f0 => Scoped h f (Compose f0 t) a -> f0 (Scoped h f t a) Source #

HTraversable (GeneralOp op :: (u -> Type) -> u -> Type) Source # 
Instance details

Defined in Language.Expression.GeneralOp

Methods

htraverse :: Applicative f => (forall (b :: u0). t b -> f (t' b)) -> GeneralOp op t a -> f (GeneralOp op t' a) Source #

hsequence :: Applicative f => GeneralOp op (Compose f t) a -> f (GeneralOp op t a) Source #

HTraversable SimpleOp Source # 
Instance details

Defined in Language.Expression.Example

Methods

htraverse :: Applicative f => (forall (b :: u). t b -> f (t' b)) -> SimpleOp t a -> f (SimpleOp t' a) Source #

hsequence :: Applicative f => SimpleOp (Compose f t) a -> f (SimpleOp t a) Source #

HTraversable LogicOp Source # 
Instance details

Defined in Language.Expression.Prop

Methods

htraverse :: Applicative f => (forall (b :: u). t b -> f (t' b)) -> LogicOp t a -> f (LogicOp t' a) Source #

hsequence :: Applicative f => LogicOp (Compose f t) a -> f (LogicOp t a) Source #

(HTraversable op, HTraversable (OpChoice ops)) => HTraversable (OpChoice (op ': ops) :: (Type -> Type) -> Type -> Type) Source # 
Instance details

Defined in Language.Expression.Choice

Methods

htraverse :: Applicative f => (forall (b :: u). t b -> f (t' b)) -> OpChoice (op ': ops) t a -> f (OpChoice (op ': ops) t' a) Source #

hsequence :: Applicative f => OpChoice (op ': ops) (Compose f t) a -> f (OpChoice (op ': ops) t a) Source #

HTraversable (OpChoice ([] :: [(Type -> Type) -> Type -> Type])) Source # 
Instance details

Defined in Language.Expression.Choice

Methods

htraverse :: Applicative f => (forall (b :: u). t b -> f (t' b)) -> OpChoice [] t a -> f (OpChoice [] t' a) Source #

hsequence :: Applicative f => OpChoice [] (Compose f t) a -> f (OpChoice [] t a) Source #

HTraversable (OpChoice ops) => HTraversable (HFree' ops :: (Type -> Type) -> Type -> Type) Source # 
Instance details

Defined in Language.Expression.Choice

Methods

htraverse :: Applicative f => (forall (b :: u). t b -> f (t' b)) -> HFree' ops t a -> f (HFree' ops t' a) Source #

hsequence :: Applicative f => HFree' ops (Compose f t) a -> f (HFree' ops t a) Source #

hfoldMapMonoid :: (HTraversable h, Monoid m) => (forall b. t b -> m) -> h t a -> m Source #

An HTraversable instance lets you do something similar to foldMap. For a more flexible operation, see hfoldMap.

hbindTraverse :: (HTraversable h, HMonad h, Applicative f) => (forall b. t b -> f (h t' b)) -> h t a -> f (h t' a) Source #

class HBifunctor (h :: (k -> *) -> (k -> *) -> k -> *) where Source #

Higher-ranked analogue of Bifunctor.

Minimal complete definition

Nothing

Methods

hbimap :: (forall b. s b -> s' b) -> (forall b. t b -> t' b) -> h s t a -> h s' t' a Source #

Higher-ranked analogue of bimap.

hfirst :: (forall b. s b -> s' b) -> h s t a -> h s' t a Source #

hsecond :: (forall b. t b -> t' b) -> h s t a -> h s t' a Source #

hbimap :: HBitraversable h => (forall b. s b -> s' b) -> (forall b. t b -> t' b) -> h s t a -> h s' t' a Source #

Higher-ranked analogue of bimap.

Instances
HBifunctor (Sum :: (k -> Type) -> (k -> Type) -> k -> Type) Source # 
Instance details

Defined in Language.Expression

Methods

hbimap :: (forall (b :: k0). s b -> s' b) -> (forall (b :: k0). t b -> t' b) -> Sum s t a -> Sum s' t' a Source #

hfirst :: (forall (b :: k0). s b -> s' b) -> Sum s t a -> Sum s' t a Source #

hsecond :: (forall (b :: k0). t b -> t' b) -> Sum s t a -> Sum s t' a Source #

HBifunctor (Product :: (k -> Type) -> (k -> Type) -> k -> Type) Source # 
Instance details

Defined in Language.Expression

Methods

hbimap :: (forall (b :: k0). s b -> s' b) -> (forall (b :: k0). t b -> t' b) -> Product s t a -> Product s' t' a Source #

hfirst :: (forall (b :: k0). s b -> s' b) -> Product s t a -> Product s' t a Source #

hsecond :: (forall (b :: k0). t b -> t' b) -> Product s t a -> Product s t' a Source #

HBifunctor (BV :: (k -> Type) -> (k -> Type) -> k -> Type) Source # 
Instance details

Defined in Language.Expression.Scope

Methods

hbimap :: (forall (b :: k0). s b -> s' b) -> (forall (b :: k0). t b -> t' b) -> BV s t a -> BV s' t' a Source #

hfirst :: (forall (b :: k0). s b -> s' b) -> BV s t a -> BV s' t a Source #

hsecond :: (forall (b :: k0). t b -> t' b) -> BV s t a -> BV s t' a Source #

HFunctor h => HBifunctor (Scoped h :: (k -> Type) -> (k -> Type) -> k -> Type) Source # 
Instance details

Defined in Language.Expression.Scope

Methods

hbimap :: (forall (b :: k0). s b -> s' b) -> (forall (b :: k0). t b -> t' b) -> Scoped h s t a -> Scoped h s' t' a Source #

hfirst :: (forall (b :: k0). s b -> s' b) -> Scoped h s t a -> Scoped h s' t a Source #

hsecond :: (forall (b :: k0). t b -> t' b) -> Scoped h s t a -> Scoped h s t' a Source #

class HBifunctor h => HBitraversable h where Source #

Methods

hbitraverse :: Applicative f => (forall b. s b -> f (s' b)) -> (forall b. t b -> f (t' b)) -> h s t a -> f (h s' t' a) Source #

Instances
HBitraversable (Sum :: (k -> Type) -> (k -> Type) -> k -> Type) Source # 
Instance details

Defined in Language.Expression

Methods

hbitraverse :: Applicative f => (forall (b :: k0). s b -> f (s' b)) -> (forall (b :: k0). t b -> f (t' b)) -> Sum s t a -> f (Sum s' t' a) Source #

HBitraversable (Product :: (k -> Type) -> (k -> Type) -> k -> Type) Source # 
Instance details

Defined in Language.Expression

Methods

hbitraverse :: Applicative f => (forall (b :: k0). s b -> f (s' b)) -> (forall (b :: k0). t b -> f (t' b)) -> Product s t a -> f (Product s' t' a) Source #

HBitraversable (BV :: (k -> Type) -> (k -> Type) -> k -> Type) Source # 
Instance details

Defined in Language.Expression.Scope

Methods

hbitraverse :: Applicative f => (forall (b :: k0). s b -> f (s' b)) -> (forall (b :: k0). t b -> f (t' b)) -> BV s t a -> f (BV s' t' a) Source #

HTraversable h => HBitraversable (Scoped h :: (k -> Type) -> (k -> Type) -> k -> Type) Source # 
Instance details

Defined in Language.Expression.Scope

Methods

hbitraverse :: Applicative f => (forall (b :: k0). s b -> f (s' b)) -> (forall (b :: k0). t b -> f (t' b)) -> Scoped h s t a -> f (Scoped h s' t' a) Source #

hbifoldMapMonoid :: (Monoid m, HBitraversable h) => (forall b. s b -> m) -> (forall b. t b -> m) -> h s t a -> m Source #

class HDuofunctor (h :: ((u -> *) -> u -> *) -> (u -> *) -> u -> *) where Source #

Minimal complete definition

Nothing

Methods

hduomap :: (forall g g' b. (forall c. g c -> g' c) -> s g b -> s' g' b) -> (forall b. t b -> t' b) -> h s t a -> h s' t' a Source #

hduomap :: HDuotraversable h => (forall g g' b. (forall c. g c -> g' c) -> s g b -> s' g' b) -> (forall b. t b -> t' b) -> h s t a -> h s' t' a Source #

Instances
HDuofunctor (HFree :: ((u -> Type) -> u -> Type) -> (u -> Type) -> u -> Type) Source # 
Instance details

Defined in Language.Expression

Methods

hduomap :: (forall (g :: u0 -> Type) (g' :: u0 -> Type) (b :: u0). (forall (c :: u0). g c -> g' c) -> s g b -> s' g' b) -> (forall (b :: u0). t b -> t' b) -> HFree s t a -> HFree s' t' a Source #

HDuofunctor (Scope g :: ((u -> Type) -> u -> Type) -> (u -> Type) -> u -> Type) Source # 
Instance details

Defined in Language.Expression.Scope

Methods

hduomap :: (forall (g0 :: u0 -> Type) (g' :: u0 -> Type) (b :: u0). (forall (c :: u0). g0 c -> g' c) -> s g0 b -> s' g' b) -> (forall (b :: u0). t b -> t' b) -> Scope g s t a -> Scope g s' t' a Source #

hduomapFirst :: HDuofunctor h => (forall g g' b. (forall c. g c -> g' c) -> s g b -> s' g' b) -> h s t a -> h s' t a Source #

hduomapFirst' :: (HDuofunctor h, HFunctor s) => (forall g b. s g b -> s' g b) -> h s t a -> h s' t a Source #

hduomapSecond :: (HDuofunctor h, HFunctor s) => (forall b. t b -> t' b) -> h s t a -> h s t' a Source #

class HDuofunctor h => HDuotraversable h where Source #

Methods

hduotraverse :: Applicative f => (forall g g' b. (forall c. g c -> f (g' c)) -> s g b -> f (s' g' b)) -> (forall b. t b -> f (t' b)) -> h s t a -> f (h s' t' a) Source #

Instances
HDuotraversable (HFree :: ((u -> Type) -> u -> Type) -> (u -> Type) -> u -> Type) Source # 
Instance details

Defined in Language.Expression

Methods

hduotraverse :: Applicative f => (forall (g :: u0 -> Type) (g' :: u0 -> Type) (b :: u0). (forall (c :: u0). g c -> f (g' c)) -> s g b -> f (s' g' b)) -> (forall (b :: u0). t b -> f (t' b)) -> HFree s t a -> f (HFree s' t' a) Source #

HDuotraversable (Scope g :: ((u -> Type) -> u -> Type) -> (u -> Type) -> u -> Type) Source # 
Instance details

Defined in Language.Expression.Scope

Methods

hduotraverse :: Applicative f => (forall (g0 :: u0 -> Type) (g' :: u0 -> Type) (b :: u0). (forall (c :: u0). g0 c -> f (g' c)) -> s g0 b -> f (s' g' b)) -> (forall (b :: u0). t b -> f (t' b)) -> Scope g s t a -> f (Scope g s' t' a) Source #

hduotraverseFirst :: (HDuotraversable h, Applicative f) => (forall g g' b. (forall c. g c -> f (g' c)) -> s g b -> f (s' g' b)) -> h s t a -> f (h s' t a) Source #

hduotraverseFirst' :: (HDuotraversable h, HTraversable s, Monad f) => (forall g b. s g b -> f (s' g b)) -> h s t a -> f (h s' t a) Source #

hduotraverseSecond :: (HDuotraversable h, HTraversable s, Applicative f) => (forall b. t b -> f (t' b)) -> h s t a -> f (h s t' a) Source #

class HFoldableAt k h where Source #

This is a more flexible, higher-ranked version of Foldable. While Foldable only allows you to fold into a Monoid, HFoldable allows you to fold into some arbitrary type constructor k. This means that the instance can take advantage of additional structure inside k and h, to combine internal results in different ways, rather than just the mappend available to foldMap.

Notice that if you have

instance (Monoid m) => HFoldableAt (Const m) h

then hfoldMap behaves very much like regular foldMap.

Methods

hfoldMap :: (forall b. t b -> k b) -> h t a -> k a Source #

Instances
HFoldableAt (k2 :: k1 -> Type) (Reverse :: (k1 -> Type) -> k1 -> Type) Source # 
Instance details

Defined in Language.Expression

Methods

hfoldMap :: (forall (b :: k). t b -> k2 b) -> Reverse t a -> k2 a Source #

HFoldableAt (k2 :: k1 -> Type) (Sum k2 :: (k1 -> Type) -> k1 -> Type) Source # 
Instance details

Defined in Language.Expression

Methods

hfoldMap :: (forall (b :: k). t b -> k2 b) -> Sum k2 t a -> k2 a Source #

HFoldableAt k2 h => HFoldableAt (k2 :: k1 -> Type) (HFree h :: (k1 -> Type) -> k1 -> Type) Source # 
Instance details

Defined in Language.Expression

Methods

hfoldMap :: (forall (b :: k). t b -> k2 b) -> HFree h t a -> k2 a Source #

(HDuotraversable h, HDuofoldableAt k2 h) => HFoldableAt (k2 :: k1 -> Type) (SFree h :: (k1 -> Type) -> k1 -> Type) Source # 
Instance details

Defined in Language.Expression.Scope

Methods

hfoldMap :: (forall (b :: k). t b -> k2 b) -> SFree h t a -> k2 a Source #

EvalOpAt k2 op => HFoldableAt (k2 :: k1 -> Type) (GeneralOp op :: (k1 -> Type) -> k1 -> Type) Source # 
Instance details

Defined in Language.Expression.GeneralOp

Methods

hfoldMap :: (forall (b :: k). t b -> k2 b) -> GeneralOp op t a -> k2 a Source #

HFoldableAt Identity SimpleOp Source # 
Instance details

Defined in Language.Expression.Example

Methods

hfoldMap :: (forall (b :: k). t b -> Identity b) -> SimpleOp t a -> Identity a Source #

HFoldableAt Identity LogicOp Source # 
Instance details

Defined in Language.Expression.Prop

Methods

hfoldMap :: (forall (b :: k). t b -> Identity b) -> LogicOp t a -> Identity a Source #

HFoldableAt SBV SimpleOp Source # 
Instance details

Defined in Language.Expression.Example

Methods

hfoldMap :: (forall (b :: k). t b -> SBV b) -> SimpleOp t a -> SBV a Source #

HFoldableAt SBV LogicOp Source # 
Instance details

Defined in Language.Expression.Prop

Methods

hfoldMap :: (forall (b :: k). t b -> SBV b) -> LogicOp t a -> SBV a Source #

(HFoldableAt k op, HFoldableAt k (OpChoice ops)) => HFoldableAt (k :: Type -> Type) (OpChoice (op ': ops) :: (Type -> Type) -> Type -> Type) Source # 
Instance details

Defined in Language.Expression.Choice

Methods

hfoldMap :: (forall (b :: k0). t b -> k b) -> OpChoice (op ': ops) t a -> k a Source #

HFoldableAt (k :: Type -> Type) (OpChoice ([] :: [(Type -> Type) -> Type -> Type])) Source # 
Instance details

Defined in Language.Expression.Choice

Methods

hfoldMap :: (forall (b :: k0). t b -> k b) -> OpChoice [] t a -> k a Source #

(HFoldableAt k (OpChoice ops), HFunctor (OpChoice ops)) => HFoldableAt (k :: Type -> Type) (HFree' ops :: (Type -> Type) -> Type -> Type) Source # 
Instance details

Defined in Language.Expression.Choice

Methods

hfoldMap :: (forall (b :: k0). t b -> k b) -> HFree' ops t a -> k a Source #

Alternative k => HFoldableAt (k :: Type -> Type) (Product k :: (Type -> Type) -> Type -> Type) Source # 
Instance details

Defined in Language.Expression

Methods

hfoldMap :: (forall (b :: k0). t b -> k b) -> Product k t a -> k a Source #

(Alternative g, Foldable f) => HFoldableAt (g :: Type -> Type) (Compose f :: (Type -> Type) -> Type -> Type) Source #

e.g. (Monoid m, Foldable f) => HFoldableAt (Const m) (Compose f)

Instance details

Defined in Language.Expression

Methods

hfoldMap :: (forall (b :: k). t b -> g b) -> Compose f t a -> g a Source #

implHfoldMap :: HFunctor h => (h k a -> k a) -> (forall b. t b -> k b) -> h t a -> k a Source #

For HFunctors, provides an implementation of hfoldMap in terms of a simple hfold-like function.

implHfoldMapCompose :: (HTraversable h, Monad m) => (h k a -> m (k a)) -> (forall b. t b -> Compose m k b) -> h t a -> Compose m k a Source #

A helper function for implementing instances with the general form Monad m => HFoldableAt (Compose m t) h. I.e. folding that requires a monadic context of some kind.

hfold :: HFoldableAt t h => h t a -> t a Source #

Higher-ranked equivalent of fold.

hfoldA :: (HFoldableAt (Compose f t) h, Applicative f) => h t a -> f (t a) Source #

Fold in an applicative context.

hfoldMapA :: (HFoldableAt (Compose f k) h, Applicative f) => (forall b. t b -> f (k b)) -> h t a -> f (k a) Source #

Fold in an applicative context.

hfoldTraverse :: (HFoldableAt k h, HTraversable h, Applicative f) => (forall b. t b -> f (k b)) -> h t a -> f (k a) Source #

class HBifoldableAt k h where Source #

Methods

hbifoldMap :: (forall b. f b -> k b) -> (forall b. g b -> k b) -> h f g a -> k a Source #

Instances
HBifoldableAt (k2 :: k1 -> Type) (Sum :: (k1 -> Type) -> (k1 -> Type) -> k1 -> Type) Source # 
Instance details

Defined in Language.Expression

Methods

hbifoldMap :: (forall (b :: k). f b -> k2 b) -> (forall (b :: k). g b -> k2 b) -> Sum f g a -> k2 a Source #

HBifoldableAt (k2 :: k1 -> Type) (BV :: (k1 -> Type) -> (k1 -> Type) -> k1 -> Type) Source # 
Instance details

Defined in Language.Expression.Scope

Methods

hbifoldMap :: (forall (b :: k). f b -> k2 b) -> (forall (b :: k). g b -> k2 b) -> BV f g a -> k2 a Source #

(HFunctor h, HFoldableAt k2 h) => HBifoldableAt (k2 :: k1 -> Type) (Scoped h :: (k1 -> Type) -> (k1 -> Type) -> k1 -> Type) Source # 
Instance details

Defined in Language.Expression.Scope

Methods

hbifoldMap :: (forall (b :: k). f b -> k2 b) -> (forall (b :: k). g b -> k2 b) -> Scoped h f g a -> k2 a Source #

Alternative k => HBifoldableAt (k :: Type -> Type) (Product :: (Type -> Type) -> (Type -> Type) -> Type -> Type) Source # 
Instance details

Defined in Language.Expression

Methods

hbifoldMap :: (forall (b :: k0). f b -> k b) -> (forall (b :: k0). g b -> k b) -> Product f g a -> k a Source #

hbifold :: HBifoldableAt k h => h k k a -> k a Source #

class HDuofoldableAt k h where Source #

Methods

hduofoldMap :: HTraversable s => (forall g b. (forall c. g c -> k c) -> s g b -> k b) -> (forall b. t b -> k b) -> h s t a -> k a Source #

Instances
HDuofoldableAt (k2 :: k1 -> Type) (HFree :: ((k1 -> Type) -> k1 -> Type) -> (k1 -> Type) -> k1 -> Type) Source # 
Instance details

Defined in Language.Expression

Methods

hduofoldMap :: HTraversable s => (forall (g :: k -> Type) (b :: k). (forall (c :: k). g c -> k2 c) -> s g b -> k2 b) -> (forall (b :: k). t b -> k2 b) -> HFree s t a -> k2 a Source #

HDuofoldableAt (k2 :: k1 -> Type) (Scope k2 :: ((k1 -> Type) -> k1 -> Type) -> (k1 -> Type) -> k1 -> Type) Source # 
Instance details

Defined in Language.Expression.Scope

Methods

hduofoldMap :: HTraversable s => (forall (g :: k -> Type) (b :: k). (forall (c :: k). g c -> k2 c) -> s g b -> k2 b) -> (forall (b :: k). t b -> k2 b) -> Scope k2 s t a -> k2 a Source #

implHduofoldMap :: (HDuofunctor h, HFunctor s) => ((forall g b. (forall c. g c -> k c) -> s g b -> k b) -> h s k a -> k a) -> (forall g b. (forall c. g c -> k c) -> s g b -> k b) -> (forall b. t b -> k b) -> h s t a -> k a Source #

implHduofoldMapCompose :: (HDuotraversable h, HTraversable s, Monad m) => ((forall g b. (forall c. g c -> m (k c)) -> s g b -> m (k b)) -> h s k a -> m (k a)) -> (forall g b. (forall c. g c -> Compose m k c) -> s g b -> Compose m k b) -> (forall b. t b -> Compose m k b) -> h s t a -> Compose m k a Source #

data HFree h t a Source #

HFree h is a higher-ranked free monad over the higher-ranked functor h. That means that given HFunctor h, we get HMonad (HFree h) for free.

Constructors

HPure (t a) 
HWrap (h (HFree h t) a) 
Instances
HDuofoldableAt (k2 :: k1 -> Type) (HFree :: ((k1 -> Type) -> k1 -> Type) -> (k1 -> Type) -> k1 -> Type) Source # 
Instance details

Defined in Language.Expression

Methods

hduofoldMap :: HTraversable s => (forall (g :: k -> Type) (b :: k). (forall (c :: k). g c -> k2 c) -> s g b -> k2 b) -> (forall (b :: k). t b -> k2 b) -> HFree s t a -> k2 a Source #

HFoldableAt k2 h => HFoldableAt (k2 :: k1 -> Type) (HFree h :: (k1 -> Type) -> k1 -> Type) Source # 
Instance details

Defined in Language.Expression

Methods

hfoldMap :: (forall (b :: k). t b -> k2 b) -> HFree h t a -> k2 a Source #

Pretty2 op => Pretty2 (HFree op :: (k -> Type) -> k -> Type) Source # 
Instance details

Defined in Language.Expression.Pretty

Methods

pretty2 :: Pretty1 t => HFree op t a -> String Source #

prettys2Prec :: Pretty1 t => Int -> HFree op t a -> ShowS Source #

HDuotraversable (HFree :: ((u -> Type) -> u -> Type) -> (u -> Type) -> u -> Type) Source # 
Instance details

Defined in Language.Expression

Methods

hduotraverse :: Applicative f => (forall (g :: u0 -> Type) (g' :: u0 -> Type) (b :: u0). (forall (c :: u0). g c -> f (g' c)) -> s g b -> f (s' g' b)) -> (forall (b :: u0). t b -> f (t' b)) -> HFree s t a -> f (HFree s' t' a) Source #

HDuofunctor (HFree :: ((u -> Type) -> u -> Type) -> (u -> Type) -> u -> Type) Source # 
Instance details

Defined in Language.Expression

Methods

hduomap :: (forall (g :: u0 -> Type) (g' :: u0 -> Type) (b :: u0). (forall (c :: u0). g c -> g' c) -> s g b -> s' g' b) -> (forall (b :: u0). t b -> t' b) -> HFree s t a -> HFree s' t' a Source #

HTraversable h => HTraversable (HFree h :: (u -> Type) -> u -> Type) Source # 
Instance details

Defined in Language.Expression

Methods

htraverse :: Applicative f => (forall (b :: u0). t b -> f (t' b)) -> HFree h t a -> f (HFree h t' a) Source #

hsequence :: Applicative f => HFree h (Compose f t) a -> f (HFree h t a) Source #

HFunctor h => HMonad (HFree h :: (k -> Type) -> k -> Type) Source # 
Instance details

Defined in Language.Expression

HFunctor h => HBind (HFree h :: (k -> Type) -> k -> Type) Source # 
Instance details

Defined in Language.Expression

Methods

(^>>=) :: HFree h t a -> (forall (b :: k0). t b -> HFree h t' b) -> HFree h t' a Source #

HPointed (HFree h :: (k -> Type) -> k -> Type) Source # 
Instance details

Defined in Language.Expression

Methods

hpure :: t a -> HFree h t a Source #

HFunctor h => HFunctor (HFree h :: (u -> Type) -> u -> Type) Source # 
Instance details

Defined in Language.Expression

Methods

hmap :: (forall (b :: u0). t b -> t' b) -> HFree h t a -> HFree h t' a Source #

Num (WhileExpr l AlgReal) Source # 
Instance details

Defined in Language.While.Syntax

IsString s => IsString (WhileExpr s AlgReal) Source # 
Instance details

Defined in Language.While.Syntax