Safe Haskell	Safe-Inferred
Language	GHC2021

Data.HTree.Existential

Contents

existential data types
existential type synonyms
working with existential HTrees/HLists functions
useful functors to work with existential type-level structures
- working with Has

Description

Existential types and helpers to work with existentials HLists and HTrees

Synopsis

data Some g where
- MkSome :: g k -> Some g
data Some2 g f where
- MkSome2 :: g f k -> Some2 g f
type ETree = Some2 HTree
type EList = Some2 HList
with :: forall {l} (g :: l -> Type) r. Some g -> (forall m. g m -> r) -> r
with2 :: forall {k} {l} (g :: k -> l -> Type) (f :: k) r. Some2 g f -> (forall m. g f m -> r) -> r
withSomeHTree :: ETree f -> (forall t. HTree f t -> r) -> r
withSomeHList :: EList f -> (forall xs. HList f xs -> r) -> r
hcFoldEHList :: forall c f y. (forall x. c x => f x -> y -> y) -> y -> EList (Has c f) -> y
hcFoldMapEHTree :: forall c f y. Semigroup y => (forall a. c a => f a -> y) -> ETree (Has c f) -> y
data Has c f k where
- Proves :: c k => f k -> Has c f k
type HasTypeable = Has Typeable
type HasIs k = Has ((~) k)
withProves :: Some (Has c f) -> (forall a. c a => f a -> r) -> r
prodHas :: forall c1 c2 f. Some (Has c1 (Has c2 f)) -> Some (Has (Both c1 c2) f)
flipHas :: forall c1 c2 f. Some (Has c1 (Has c2 f)) -> Some (Has c2 (Has c1 f))

existential data types

data Some g where Source #

a Some type that takes an arity one type constructor, this is for completeness

Constructors

MkSome :: g k -> Some g

Instances

Instances details

Typeable f => Show (Some (Has (Typeable :: l -> Constraint) f)) Source #
Instance details Defined in Data.HTree.Existential Methods showsPrec :: Int -> Some (Has Typeable f) -> ShowS # show :: Some (Has Typeable f) -> String # showList :: [Some (Has Typeable f)] -> ShowS #
(forall (k :: l). Show (g k)) => Show (Some g) Source #
Instance details Defined in Data.HTree.Existential Methods showsPrec :: Int -> Some g -> ShowS # show :: Some g -> String # showList :: [Some g] -> ShowS #
(forall x. Eq x => Eq (f x), Typeable f) => Eq (Some (Has (Typeable :: Type -> Constraint) (Has Eq f))) Source #
Instance details Defined in Data.HTree.Existential Methods (==) :: Some (Has Typeable (Has Eq f)) -> Some (Has Typeable (Has Eq f)) -> Bool # (/=) :: Some (Has Typeable (Has Eq f)) -> Some (Has Typeable (Has Eq f)) -> Bool #
(forall x. Ord x => Ord (f x), Typeable f, Eq (Some (Has (Typeable :: Type -> Constraint) (Has Ord f)))) => Ord (Some (Has (Typeable :: Type -> Constraint) (Has Ord f))) Source #
Instance details Defined in Data.HTree.Existential Methods compare :: Some (Has Typeable (Has Ord f)) -> Some (Has Typeable (Has Ord f)) -> Ordering # (<) :: Some (Has Typeable (Has Ord f)) -> Some (Has Typeable (Has Ord f)) -> Bool # (<=) :: Some (Has Typeable (Has Ord f)) -> Some (Has Typeable (Has Ord f)) -> Bool # (>) :: Some (Has Typeable (Has Ord f)) -> Some (Has Typeable (Has Ord f)) -> Bool # (>=) :: Some (Has Typeable (Has Ord f)) -> Some (Has Typeable (Has Ord f)) -> Bool # max :: Some (Has Typeable (Has Ord f)) -> Some (Has Typeable (Has Ord f)) -> Some (Has Typeable (Has Ord f)) # min :: Some (Has Typeable (Has Ord f)) -> Some (Has Typeable (Has Ord f)) -> Some (Has Typeable (Has Ord f)) #

data Some2 g f where Source #

a Some type that take an arity two type constructor, this is necessary so that we avoid using composition on the type level or having visible parameters to the type synonyms

Constructors

MkSome2 :: g f k -> Some2 g f

Instances

Instances details

(forall x. Eq x => Eq (f x), Typeable f) => Eq (EList (Has (Both (Typeable :: Type -> Constraint) Eq) f)) Source #
Instance details Defined in Data.HTree.Existential Methods (==) :: EList (Has (Both Typeable Eq) f) -> EList (Has (Both Typeable Eq) f) -> Bool # (/=) :: EList (Has (Both Typeable Eq) f) -> EList (Has (Both Typeable Eq) f) -> Bool #
Eq (f k2) => Eq (EList (HasIs k2 f)) Source #
Instance details Defined in Data.HTree.Existential Methods (==) :: EList (HasIs k2 f) -> EList (HasIs k2 f) -> Bool # (/=) :: EList (HasIs k2 f) -> EList (HasIs k2 f) -> Bool #
(forall x. Eq x => Eq (f x), Typeable f) => Eq (ETree (Has (Both (Typeable :: Type -> Constraint) Eq) f)) Source #
Instance details Defined in Data.HTree.Existential Methods (==) :: ETree (Has (Both Typeable Eq) f) -> ETree (Has (Both Typeable Eq) f) -> Bool # (/=) :: ETree (Has (Both Typeable Eq) f) -> ETree (Has (Both Typeable Eq) f) -> Bool #
(forall (k1 :: l). Show (g f k1)) => Show (Some2 g f) Source #
Instance details Defined in Data.HTree.Existential Methods showsPrec :: Int -> Some2 g f -> ShowS # show :: Some2 g f -> String # showList :: [Some2 g f] -> ShowS #

existential type synonyms

type ETree = Some2 HTree Source #

HTree but the type level tree is existential

type EList = Some2 HList Source #

HList but the type level list is existential

working with existential HTrees/HLists functions

with :: forall {l} (g :: l -> Type) r. Some g -> (forall m. g m -> r) -> r Source #

take some existentai arity one type constructor and a function that takes the non-existential one and returns some r and return an r

with2 :: forall {k} {l} (g :: k -> l -> Type) (f :: k) r. Some2 g f -> (forall m. g f m -> r) -> r Source #

take some existential arity two type constructor and a function that takes the non-existential one and returns some r and return an r

withSomeHTree :: ETree f -> (forall t. HTree f t -> r) -> r Source #

with2 specialized to HTrees

withSomeHList :: EList f -> (forall xs. HList f xs -> r) -> r Source #

with2 specialized to HLists

hcFoldEHList :: forall c f y. (forall x. c x => f x -> y -> y) -> y -> EList (Has c f) -> y Source #

fold over existential hlists

hcFoldMapEHTree :: forall c f y. Semigroup y => (forall a. c a => f a -> y) -> ETree (Has c f) -> y Source #

fold over existential htrees

useful functors to work with existential type-level structures

data Has c f k where Source #

a functor useful for proving a constraint for some type

>>> import Data.Functor.Identity
>>> Proves @Eq (Identity (5 :: Int))
Proves (Identity 5)

Constructors

Proves :: c k => f k -> Has c f k

Instances

Instances details

Typeable f => Show (Some (Has (Typeable :: l -> Constraint) f)) Source #
Instance details Defined in Data.HTree.Existential Methods showsPrec :: Int -> Some (Has Typeable f) -> ShowS # show :: Some (Has Typeable f) -> String # showList :: [Some (Has Typeable f)] -> ShowS #
(forall x. Eq x => Eq (f x), Typeable f) => Eq (EList (Has (Both (Typeable :: Type -> Constraint) Eq) f)) Source #
Instance details Defined in Data.HTree.Existential Methods (==) :: EList (Has (Both Typeable Eq) f) -> EList (Has (Both Typeable Eq) f) -> Bool # (/=) :: EList (Has (Both Typeable Eq) f) -> EList (Has (Both Typeable Eq) f) -> Bool #
Eq (f k2) => Eq (EList (HasIs k2 f)) Source #
Instance details Defined in Data.HTree.Existential Methods (==) :: EList (HasIs k2 f) -> EList (HasIs k2 f) -> Bool # (/=) :: EList (HasIs k2 f) -> EList (HasIs k2 f) -> Bool #
(forall x. Eq x => Eq (f x), Typeable f) => Eq (ETree (Has (Both (Typeable :: Type -> Constraint) Eq) f)) Source #
Instance details Defined in Data.HTree.Existential Methods (==) :: ETree (Has (Both Typeable Eq) f) -> ETree (Has (Both Typeable Eq) f) -> Bool # (/=) :: ETree (Has (Both Typeable Eq) f) -> ETree (Has (Both Typeable Eq) f) -> Bool #
(forall x. Eq x => Eq (f x), Typeable f) => Eq (Some (Has (Typeable :: Type -> Constraint) (Has Eq f))) Source #
Instance details Defined in Data.HTree.Existential Methods (==) :: Some (Has Typeable (Has Eq f)) -> Some (Has Typeable (Has Eq f)) -> Bool # (/=) :: Some (Has Typeable (Has Eq f)) -> Some (Has Typeable (Has Eq f)) -> Bool #
(forall x. Ord x => Ord (f x), Typeable f, Eq (Some (Has (Typeable :: Type -> Constraint) (Has Ord f)))) => Ord (Some (Has (Typeable :: Type -> Constraint) (Has Ord f))) Source #
Instance details Defined in Data.HTree.Existential Methods compare :: Some (Has Typeable (Has Ord f)) -> Some (Has Typeable (Has Ord f)) -> Ordering # (<) :: Some (Has Typeable (Has Ord f)) -> Some (Has Typeable (Has Ord f)) -> Bool # (<=) :: Some (Has Typeable (Has Ord f)) -> Some (Has Typeable (Has Ord f)) -> Bool # (>) :: Some (Has Typeable (Has Ord f)) -> Some (Has Typeable (Has Ord f)) -> Bool # (>=) :: Some (Has Typeable (Has Ord f)) -> Some (Has Typeable (Has Ord f)) -> Bool # max :: Some (Has Typeable (Has Ord f)) -> Some (Has Typeable (Has Ord f)) -> Some (Has Typeable (Has Ord f)) # min :: Some (Has Typeable (Has Ord f)) -> Some (Has Typeable (Has Ord f)) -> Some (Has Typeable (Has Ord f)) #
Show (f k2) => Show (Has c f k2) Source #
Instance details Defined in Data.HTree.Constraint Methods showsPrec :: Int -> Has c f k2 -> ShowS # show :: Has c f k2 -> String # showList :: [Has c f k2] -> ShowS #

type HasTypeable = Has Typeable Source #

Has but specialised to Typeable

type HasIs k = Has ((~) k) Source #

Has but specialised to a constant type, Some (HasIs k f) is isomorphic to f k

working with `Has`

withProves :: Some (Has c f) -> (forall a. c a => f a -> r) -> r Source #

destruct Some, destruct Has

prodHas :: forall c1 c2 f. Some (Has c1 (Has c2 f)) -> Some (Has (Both c1 c2) f) Source #

condens the Has constraints in an existential

flipHas :: forall c1 c2 f. Some (Has c1 (Has c2 f)) -> Some (Has c2 (Has c1 f)) Source #

flip the constraints in an existential

existential data types

Instances

Instances

existential type synonyms

working with existential HTrees/HLists functions

useful functors to work with existential type-level structures

Instances

working with Has

working with `Has`