Safe Haskell | Safe-Inferred |
---|---|
Language | GHC2021 |
Synopsis
- data Some g where
- data Some2 g f where
- 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
- 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
a Some type that takes an arity one type constructor, this is for completeness
Instances
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 # | |
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 # | |
(forall (k1 :: l). Show (g f k1)) => Show (Some2 g f) Source # | |
existential type synonyms
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
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
a functor useful for proving a constraint for some type
>>>
import Data.Functor.Identity
>>>
Proves @Eq (Identity (5 :: Int))
Proves (Identity 5)
Instances
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 #