| Safe Haskell | None |
|---|---|
| Language | GHC2021 |
Data.HTree.Existential
Synopsis
- data Some (g :: l -> Type) where
- data Some2 (g :: k -> l -> Type) (f :: k) where
- type ETree = Some2 (HTree :: (k -> Type) -> TyTree k -> Type)
- type EList = Some2 (HList :: (k -> Type) -> [k] -> Type)
- with :: Some g -> (forall (m :: l). g m -> r) -> r
- with2 :: forall {k} {l} g (f :: k) r. Some2 g f -> (forall (m :: l). g f m -> r) -> r
- withSomeHTree :: forall {k} (f :: k -> Type) r. ETree f -> (forall (t :: TyTree k). HTree f t -> r) -> r
- withSomeHList :: forall {k} (f :: k -> Type) r. EList f -> (forall (xs :: [k]). HList f xs -> r) -> r
- hcFoldEHList :: (forall (x :: k). c x => f x -> y -> y) -> y -> EList (Has c f) -> y
- hcFoldMapEHTree :: forall {k} c f y. Semigroup y => (forall (a :: k). c a => f a -> y) -> ETree (Has c f) -> y
- data Has (c :: k -> Constraint) (f :: k -> Type) (k1 :: k) where
- Proves :: forall {k} (c :: k -> Constraint) (k1 :: k) (f :: k -> Type). c k1 => f k1 -> Has c f k1
- type HasTypeable = Has (Typeable :: k -> Constraint)
- type HasIs (k1 :: k) = Has (k ~ k1)
- withProves :: Some (Has c f) -> (forall (a :: l). c a => f a -> r) -> r
- prodHas :: forall {l} (c1 :: l -> Constraint) (c2 :: l -> Constraint) (f :: l -> Type). Some (Has c1 (Has c2 f)) -> Some (Has (Both c1 c2) f)
- flipHas :: forall {l} (c1 :: l -> Constraint) (c2 :: l -> Constraint) (f :: l -> Type). Some (Has c1 (Has c2 f)) -> Some (Has c2 (Has c1 f))
existential data types
data Some (g :: l -> Type) where Source #
a Some type that takes an arity one type constructor, this is for completeness
Instances
data Some2 (g :: k -> l -> Type) (f :: k) 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
Instances
| (forall x. Eq x => Eq (f x), Typeable f) => Eq (EList (Has (Both (Typeable :: Type -> Constraint) Eq) f)) Source # | |
Defined in Data.HTree.Existential | |
| Eq (f k2) => Eq (EList (HasIs k2 f)) Source # | |
| (forall x. Eq x => Eq (f x), Typeable f) => Eq (ETree (Has (Both (Typeable :: Type -> Constraint) Eq) f)) Source # | |
Defined in Data.HTree.Existential | |
| (forall (k1 :: l). Show (g f k1)) => Show (Some2 g f) Source # | |
existential type synonyms
type ETree = Some2 (HTree :: (k -> Type) -> TyTree k -> Type) Source #
HTree but the type level tree is existential
type EList = Some2 (HList :: (k -> Type) -> [k] -> Type) Source #
HList but the type level list is existential
working with existential HTrees/HLists functions
with :: Some g -> (forall (m :: l). 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 (f :: k) r. Some2 g f -> (forall (m :: l). 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 :: forall {k} (f :: k -> Type) r. ETree f -> (forall (t :: TyTree k). HTree f t -> r) -> r Source #
withSomeHList :: forall {k} (f :: k -> Type) r. EList f -> (forall (xs :: [k]). HList f xs -> r) -> r Source #
hcFoldEHList :: (forall (x :: k). c x => f x -> y -> y) -> y -> EList (Has c f) -> y Source #
fold over existential hlists
hcFoldMapEHTree :: forall {k} c f y. Semigroup y => (forall (a :: k). 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 :: k -> Constraint) (f :: k -> Type) (k1 :: 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 :: forall {k} (c :: k -> Constraint) (k1 :: k) (f :: k -> Type). c k1 => f k1 -> Has c f k1 |
Instances
type HasTypeable = Has (Typeable :: k -> Constraint) Source #
type HasIs (k1 :: k) = Has (k ~ k1) 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 :: l). c a => f a -> r) -> r Source #