| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
Generics.Kind
Description
Main module of kind-generics. Please refer to the README file for documentation on how to use this package.
Synopsis
- data ((f :: k -> Type) :+: (g :: k -> Type)) (p :: k)
- data ((f :: k -> Type) :*: (g :: k -> Type)) (p :: k) = (f p) :*: (g p)
- data V1 (p :: k)
- data U1 (p :: k) = U1
- newtype M1 i (c :: Meta) (f :: k -> Type) (p :: k) = M1 {
- unM1 :: f p
- newtype Field (t :: Atom d Type) (x :: LoT d) where
- data ((c :: Atom d Constraint) :=>: (f :: LoT d -> Type)) (x :: LoT d) where
- data Exists k (f :: LoT (k -> d) -> Type) (x :: LoT d) where
- data Atom d (k :: TYPE r) where
- Var :: forall d k1. TyVar d k1 -> Atom d k1
- Kon :: forall k1 d. k1 -> Atom d k1
- (:@:) :: forall d k1 k2. Atom d (k1 -> k2) -> Atom d k1 -> Atom d k2
- (:&:) :: forall d. Atom d Constraint -> Atom d Constraint -> Atom d Constraint
- ForAll :: forall d1 d. Atom (d1 -> d) Type -> Atom d Type
- (:=>>:) :: forall d. Atom d Constraint -> Atom d Type -> Atom d Type
- Eval :: forall d k1. Atom d (Exp k1) -> Atom d k1
- data TyVar d (k :: TYPE r) where
- type (:$:) (f :: k1 -> k2) (x :: Atom d k1) = ('Kon f :: Atom d (k1 -> k2)) ':@: x
- type (:~:) (a :: Atom d k1) (b :: Atom d k1) = (('Kon ((~) :: k1 -> k1 -> Constraint) :: Atom d (k1 -> k1 -> Constraint)) ':@: a) ':@: b
- type (:~~:) (a :: Atom d k1) (b :: Atom d k2) = (('Kon ((~~) :: k1 -> k2 -> Constraint) :: Atom d (k1 -> k2 -> Constraint)) ':@: a) ':@: b
- type Var0 = 'Var ('VZ :: TyVar (k -> xs) k)
- type Var1 = 'Var ('VS ('VZ :: TyVar (k -> xs) k) :: TyVar (x -> k -> xs) k)
- type Var2 = 'Var ('VS ('VS ('VZ :: TyVar (k -> xs) k) :: TyVar (x1 -> k -> xs) k) :: TyVar (x -> x1 -> k -> xs) k)
- type Var3 = 'Var ('VS ('VS ('VS ('VZ :: TyVar (k -> xs) k) :: TyVar (x2 -> k -> xs) k) :: TyVar (x1 -> x2 -> k -> xs) k) :: TyVar (x -> x1 -> x2 -> k -> xs) k)
- type Var4 = 'Var ('VS ('VS ('VS ('VS ('VZ :: TyVar (k -> xs) k) :: TyVar (x3 -> k -> xs) k) :: TyVar (x2 -> x3 -> k -> xs) k) :: TyVar (x1 -> x2 -> x3 -> k -> xs) k) :: TyVar (x -> x1 -> x2 -> x3 -> k -> xs) k)
- type Var5 = 'Var ('VS ('VS ('VS ('VS ('VS ('VZ :: TyVar (k -> xs) k) :: TyVar (x4 -> k -> xs) k) :: TyVar (x3 -> x4 -> k -> xs) k) :: TyVar (x2 -> x3 -> x4 -> k -> xs) k) :: TyVar (x1 -> x2 -> x3 -> x4 -> k -> xs) k) :: TyVar (x -> x1 -> x2 -> x3 -> x4 -> k -> xs) k)
- type Var6 = 'Var ('VS ('VS ('VS ('VS ('VS ('VS ('VZ :: TyVar (k -> xs) k) :: TyVar (x5 -> k -> xs) k) :: TyVar (x4 -> x5 -> k -> xs) k) :: TyVar (x3 -> x4 -> x5 -> k -> xs) k) :: TyVar (x2 -> x3 -> x4 -> x5 -> k -> xs) k) :: TyVar (x1 -> x2 -> x3 -> x4 -> x5 -> k -> xs) k) :: TyVar (x -> x1 -> x2 -> x3 -> x4 -> x5 -> k -> xs) k)
- type Var7 = 'Var ('VS ('VS ('VS ('VS ('VS ('VS ('VS ('VZ :: TyVar (k -> xs) k) :: TyVar (x6 -> k -> xs) k) :: TyVar (x5 -> x6 -> k -> xs) k) :: TyVar (x4 -> x5 -> x6 -> k -> xs) k) :: TyVar (x3 -> x4 -> x5 -> x6 -> k -> xs) k) :: TyVar (x2 -> x3 -> x4 -> x5 -> x6 -> k -> xs) k) :: TyVar (x1 -> x2 -> x3 -> x4 -> x5 -> x6 -> k -> xs) k) :: TyVar (x -> x1 -> x2 -> x3 -> x4 -> x5 -> x6 -> k -> xs) k)
- type Var8 = 'Var ('VS ('VS ('VS ('VS ('VS ('VS ('VS ('VS ('VZ :: TyVar (k -> xs) k) :: TyVar (x7 -> k -> xs) k) :: TyVar (x6 -> x7 -> k -> xs) k) :: TyVar (x5 -> x6 -> x7 -> k -> xs) k) :: TyVar (x4 -> x5 -> x6 -> x7 -> k -> xs) k) :: TyVar (x3 -> x4 -> x5 -> x6 -> x7 -> k -> xs) k) :: TyVar (x2 -> x3 -> x4 -> x5 -> x6 -> x7 -> k -> xs) k) :: TyVar (x1 -> x2 -> x3 -> x4 -> x5 -> x6 -> x7 -> k -> xs) k) :: TyVar (x -> x1 -> x2 -> x3 -> x4 -> x5 -> x6 -> x7 -> k -> xs) k)
- type Var9 = 'Var ('VS ('VS ('VS ('VS ('VS ('VS ('VS ('VS ('VS ('VZ :: TyVar (k -> xs) k) :: TyVar (x8 -> k -> xs) k) :: TyVar (x7 -> x8 -> k -> xs) k) :: TyVar (x6 -> x7 -> x8 -> k -> xs) k) :: TyVar (x5 -> x6 -> x7 -> x8 -> k -> xs) k) :: TyVar (x4 -> x5 -> x6 -> x7 -> x8 -> k -> xs) k) :: TyVar (x3 -> x4 -> x5 -> x6 -> x7 -> x8 -> k -> xs) k) :: TyVar (x2 -> x3 -> x4 -> x5 -> x6 -> x7 -> x8 -> k -> xs) k) :: TyVar (x1 -> x2 -> x3 -> x4 -> x5 -> x6 -> x7 -> x8 -> k -> xs) k) :: TyVar (x -> x1 -> x2 -> x3 -> x4 -> x5 -> x6 -> x7 -> x8 -> k -> xs) k)
- data LoT k where
- type family (f :: k) :@@: (tys :: LoT k) where ...
- type LoT1 (a :: k) = a ':&&: 'LoT0
- type LoT2 (a :: k) (b :: k1) = a ':&&: (b ':&&: 'LoT0)
- data TyEnv where
- class GenericK (f :: k) where
- type GenericF t (f :: k) (x :: LoT k) = (GenericK f, x ~ SplitF t f, t ~ (f :@@: x))
- fromF :: forall {k} (f :: k) t (x :: LoT k). GenericF t f x => t -> RepK f x
- toF :: forall {k} (f :: k) t (x :: LoT k). GenericF t f x => RepK f x -> t
- type GenericN (n :: Nat) t (f :: k) (x :: LoT k) = (GenericK f, 'TyEnv f x ~ SplitN n t, t ~ (f :@@: x))
- fromN :: forall {k} (n :: Nat) t (f :: k) (x :: LoT k). GenericN n t f x => t -> RepK f x
- toN :: forall {k} (n :: Nat) t (f :: k) (x :: LoT k). GenericN n t f x => RepK f x -> t
- fromRepK :: forall {t} {k} (f :: t -> k) (x :: t) (xs :: LoT k). (GenericK f, SubstRep' (RepK f) x xs) => (f x :@@: xs) -> SubstRep (RepK f) x xs
- toRepK :: forall {t} {k} (f :: t -> k) (x :: t) (xs :: LoT k). (GenericK f, SubstRep' (RepK f) x xs) => SubstRep (RepK f) x xs -> f x :@@: xs
- type family SubstRep (f :: LoT (t -> k) -> Type) (x :: t) :: LoT k -> Type
- class SubstRep' (f :: LoT (t -> k) -> Type) (x :: t) (xs :: LoT k)
- type family SubstAtom (f :: Atom (t -> k) d) (x :: t) :: Atom k d where ...
- class Conv (gg :: Type -> Type) (kg :: LoT d -> Type) (tys :: LoT d) where
- toGhcGenerics :: kg tys -> gg a
- toKindGenerics :: gg a -> kg tys
- type family Interpret (t :: Atom d k) (tys :: LoT d) :: k where ...
- type family InterpretVar (t :: TyVar d k) (tys :: LoT d) :: k where ...
- type family Satisfies (cs :: [Atom d Constraint]) (tys :: LoT d) where ...
- type family ContainsTyVar (v :: TyVar d k) (t :: Atom d p) :: Bool where ...
- newtype ForAllI (f :: Atom (d1 -> d) Type) (tys :: LoT d) where
- newtype SuchThatI (c :: Atom d Constraint) (f :: Atom d Type) (tys :: LoT d) where
- newtype WrappedI (f :: Atom d Type) (tys :: LoT d) = WrapI {}
- toWrappedI :: forall {d1} {ks} (f :: Atom (d1 -> ks) Type) (tys :: LoT ks) (t :: d1). ForAllI f tys -> WrappedI f (t ':&&: tys)
- fromWrappedI :: forall {d1} {d} (f :: Atom (d1 -> d) Type) (tys :: LoT d). (forall (t :: d1). WrappedI f (t ':&&: tys)) -> ForAllI f tys
Generic representation types
data ((f :: k -> Type) :+: (g :: k -> Type)) (p :: k) infixr 5 #
Sums: encode choice between constructors
Instances
| (SubstRep' f x xs, SubstRep' g x xs) => SubstRep' (f :+: g :: LoT (t -> k) -> Type) (x :: t) (xs :: LoT k) Source # | |||||
Defined in Generics.Kind | |||||
| Generic1 (f :+: g :: k -> Type) | |||||
Defined in GHC.Generics Associated Types
| |||||
| (Conv f f' tys, Conv g g' tys) => Conv (f :+: g) (f' :+: g' :: LoT d -> Type) (tys :: LoT d) Source # | |||||
Defined in Generics.Kind Methods toGhcGenerics :: (f' :+: g') tys -> (f :+: g) a Source # toKindGenerics :: (f :+: g) a -> (f' :+: g') tys Source # | |||||
| (Foldable f, Foldable g) => Foldable (f :+: g) | Since: base-4.9.0.0 | ||||
Defined in Data.Foldable Methods fold :: Monoid m => (f :+: g) m -> m # foldMap :: Monoid m => (a -> m) -> (f :+: g) a -> m # foldMap' :: Monoid m => (a -> m) -> (f :+: g) a -> m # foldr :: (a -> b -> b) -> b -> (f :+: g) a -> b # foldr' :: (a -> b -> b) -> b -> (f :+: g) a -> b # foldl :: (b -> a -> b) -> b -> (f :+: g) a -> b # foldl' :: (b -> a -> b) -> b -> (f :+: g) a -> b # foldr1 :: (a -> a -> a) -> (f :+: g) a -> a # foldl1 :: (a -> a -> a) -> (f :+: g) a -> a # toList :: (f :+: g) a -> [a] # length :: (f :+: g) a -> Int # elem :: Eq a => a -> (f :+: g) a -> Bool # maximum :: Ord a => (f :+: g) a -> a # minimum :: Ord a => (f :+: g) a -> a # | |||||
| (Foldable1 f, Foldable1 g) => Foldable1 (f :+: g) | Since: base-4.18.0.0 | ||||
Defined in Data.Foldable1 Methods fold1 :: Semigroup m => (f :+: g) m -> m # foldMap1 :: Semigroup m => (a -> m) -> (f :+: g) a -> m # foldMap1' :: Semigroup m => (a -> m) -> (f :+: g) a -> m # toNonEmpty :: (f :+: g) a -> NonEmpty a # maximum :: Ord a => (f :+: g) a -> a # minimum :: Ord a => (f :+: g) a -> a # foldrMap1 :: (a -> b) -> (a -> b -> b) -> (f :+: g) a -> b # foldlMap1' :: (a -> b) -> (b -> a -> b) -> (f :+: g) a -> b # foldlMap1 :: (a -> b) -> (b -> a -> b) -> (f :+: g) a -> b # foldrMap1' :: (a -> b) -> (a -> b -> b) -> (f :+: g) a -> b # | |||||
| (Contravariant f, Contravariant g) => Contravariant (f :+: g) | |||||
| (Traversable f, Traversable g) => Traversable (f :+: g) | Since: base-4.9.0.0 | ||||
Defined in Data.Traversable | |||||
| (Functor f, Functor g) => Functor (f :+: g) | Since: base-4.9.0.0 | ||||
| (Typeable f, Typeable g, Data p, Data (f p), Data (g p)) => Data ((f :+: g) p) | Since: base-4.9.0.0 | ||||
Defined in Data.Data Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g0. g0 -> c g0) -> (f :+: g) p -> c ((f :+: g) p) # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c ((f :+: g) p) # toConstr :: (f :+: g) p -> Constr # dataTypeOf :: (f :+: g) p -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c ((f :+: g) p)) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c ((f :+: g) p)) # gmapT :: (forall b. Data b => b -> b) -> (f :+: g) p -> (f :+: g) p # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> (f :+: g) p -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> (f :+: g) p -> r # gmapQ :: (forall d. Data d => d -> u) -> (f :+: g) p -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> (f :+: g) p -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> (f :+: g) p -> m ((f :+: g) p) # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> (f :+: g) p -> m ((f :+: g) p) # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> (f :+: g) p -> m ((f :+: g) p) # | |||||
| Generic ((f :+: g) p) | |||||
Defined in GHC.Generics Associated Types
| |||||
| (Read (f p), Read (g p)) => Read ((f :+: g) p) | Since: base-4.7.0.0 | ||||
| (Show (f p), Show (g p)) => Show ((f :+: g) p) | Since: base-4.7.0.0 | ||||
| (Eq (f p), Eq (g p)) => Eq ((f :+: g) p) | Since: base-4.7.0.0 | ||||
| (Ord (f p), Ord (g p)) => Ord ((f :+: g) p) | Since: base-4.7.0.0 | ||||
Defined in GHC.Generics | |||||
| type SubstRep (f :+: g :: LoT (t -> k) -> Type) (x :: t) Source # | |||||
| type Rep1 (f :+: g :: k -> Type) | Since: base-4.9.0.0 | ||||
Defined in GHC.Generics type Rep1 (f :+: g :: k -> Type) = D1 ('MetaData ":+:" "GHC.Generics" "base" 'False) (C1 ('MetaCons "L1" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec1 f)) :+: C1 ('MetaCons "R1" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec1 g))) | |||||
| type Rep ((f :+: g) p) | Since: base-4.7.0.0 | ||||
Defined in GHC.Generics type Rep ((f :+: g) p) = D1 ('MetaData ":+:" "GHC.Generics" "base" 'False) (C1 ('MetaCons "L1" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (f p))) :+: C1 ('MetaCons "R1" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (g p)))) | |||||
data ((f :: k -> Type) :*: (g :: k -> Type)) (p :: k) infixr 6 #
Products: encode multiple arguments to constructors
Constructors
| (f p) :*: (g p) infixr 6 |
Instances
| (SubstRep' f x xs, SubstRep' g x xs) => SubstRep' (f :*: g :: LoT (t -> k) -> Type) (x :: t) (xs :: LoT k) Source # | |||||
Defined in Generics.Kind | |||||
| Generic1 (f :*: g :: k -> Type) | |||||
Defined in GHC.Generics Associated Types
| |||||
| (Conv f f' tys, Conv g g' tys) => Conv (f :*: g) (f' :*: g' :: LoT d -> Type) (tys :: LoT d) Source # | |||||
Defined in Generics.Kind Methods toGhcGenerics :: (f' :*: g') tys -> (f :*: g) a Source # toKindGenerics :: (f :*: g) a -> (f' :*: g') tys Source # | |||||
| (MonadFix f, MonadFix g) => MonadFix (f :*: g) | Since: base-4.9.0.0 | ||||
Defined in Control.Monad.Fix | |||||
| (MonadZip f, MonadZip g) => MonadZip (f :*: g) | Since: base-4.9.0.0 | ||||
| (Foldable f, Foldable g) => Foldable (f :*: g) | Since: base-4.9.0.0 | ||||
Defined in Data.Foldable Methods fold :: Monoid m => (f :*: g) m -> m # foldMap :: Monoid m => (a -> m) -> (f :*: g) a -> m # foldMap' :: Monoid m => (a -> m) -> (f :*: g) a -> m # foldr :: (a -> b -> b) -> b -> (f :*: g) a -> b # foldr' :: (a -> b -> b) -> b -> (f :*: g) a -> b # foldl :: (b -> a -> b) -> b -> (f :*: g) a -> b # foldl' :: (b -> a -> b) -> b -> (f :*: g) a -> b # foldr1 :: (a -> a -> a) -> (f :*: g) a -> a # foldl1 :: (a -> a -> a) -> (f :*: g) a -> a # toList :: (f :*: g) a -> [a] # length :: (f :*: g) a -> Int # elem :: Eq a => a -> (f :*: g) a -> Bool # maximum :: Ord a => (f :*: g) a -> a # minimum :: Ord a => (f :*: g) a -> a # | |||||
| (Foldable1 f, Foldable1 g) => Foldable1 (f :*: g) | Since: base-4.18.0.0 | ||||
Defined in Data.Foldable1 Methods fold1 :: Semigroup m => (f :*: g) m -> m # foldMap1 :: Semigroup m => (a -> m) -> (f :*: g) a -> m # foldMap1' :: Semigroup m => (a -> m) -> (f :*: g) a -> m # toNonEmpty :: (f :*: g) a -> NonEmpty a # maximum :: Ord a => (f :*: g) a -> a # minimum :: Ord a => (f :*: g) a -> a # foldrMap1 :: (a -> b) -> (a -> b -> b) -> (f :*: g) a -> b # foldlMap1' :: (a -> b) -> (b -> a -> b) -> (f :*: g) a -> b # foldlMap1 :: (a -> b) -> (b -> a -> b) -> (f :*: g) a -> b # foldrMap1' :: (a -> b) -> (a -> b -> b) -> (f :*: g) a -> b # | |||||
| (Contravariant f, Contravariant g) => Contravariant (f :*: g) | |||||
| (Traversable f, Traversable g) => Traversable (f :*: g) | Since: base-4.9.0.0 | ||||
Defined in Data.Traversable | |||||
| (Alternative f, Alternative g) => Alternative (f :*: g) | Since: base-4.9.0.0 | ||||
| (Applicative f, Applicative g) => Applicative (f :*: g) | Since: base-4.9.0.0 | ||||
| (Functor f, Functor g) => Functor (f :*: g) | Since: base-4.9.0.0 | ||||
| (Monad f, Monad g) => Monad (f :*: g) | Since: base-4.9.0.0 | ||||
| (MonadPlus f, MonadPlus g) => MonadPlus (f :*: g) | Since: base-4.9.0.0 | ||||
| (Typeable f, Typeable g, Data p, Data (f p), Data (g p)) => Data ((f :*: g) p) | Since: base-4.9.0.0 | ||||
Defined in Data.Data Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g0. g0 -> c g0) -> (f :*: g) p -> c ((f :*: g) p) # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c ((f :*: g) p) # toConstr :: (f :*: g) p -> Constr # dataTypeOf :: (f :*: g) p -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c ((f :*: g) p)) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c ((f :*: g) p)) # gmapT :: (forall b. Data b => b -> b) -> (f :*: g) p -> (f :*: g) p # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> (f :*: g) p -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> (f :*: g) p -> r # gmapQ :: (forall d. Data d => d -> u) -> (f :*: g) p -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> (f :*: g) p -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> (f :*: g) p -> m ((f :*: g) p) # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> (f :*: g) p -> m ((f :*: g) p) # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> (f :*: g) p -> m ((f :*: g) p) # | |||||
| (Monoid (f p), Monoid (g p)) => Monoid ((f :*: g) p) | Since: base-4.12.0.0 | ||||
| (Semigroup (f p), Semigroup (g p)) => Semigroup ((f :*: g) p) | Since: base-4.12.0.0 | ||||
| Generic ((f :*: g) p) | |||||
Defined in GHC.Generics Associated Types
| |||||
| (Read (f p), Read (g p)) => Read ((f :*: g) p) | Since: base-4.7.0.0 | ||||
| (Show (f p), Show (g p)) => Show ((f :*: g) p) | Since: base-4.7.0.0 | ||||
| (Eq (f p), Eq (g p)) => Eq ((f :*: g) p) | Since: base-4.7.0.0 | ||||
| (Ord (f p), Ord (g p)) => Ord ((f :*: g) p) | Since: base-4.7.0.0 | ||||
Defined in GHC.Generics | |||||
| type SubstRep (f :*: g :: LoT (t -> k) -> Type) (x :: t) Source # | |||||
| type Rep1 (f :*: g :: k -> Type) | Since: base-4.9.0.0 | ||||
Defined in GHC.Generics type Rep1 (f :*: g :: k -> Type) = D1 ('MetaData ":*:" "GHC.Generics" "base" 'False) (C1 ('MetaCons ":*:" ('InfixI 'RightAssociative 6) 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec1 f) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec1 g))) | |||||
| type Rep ((f :*: g) p) | Since: base-4.7.0.0 | ||||
Defined in GHC.Generics type Rep ((f :*: g) p) = D1 ('MetaData ":*:" "GHC.Generics" "base" 'False) (C1 ('MetaCons ":*:" ('InfixI 'RightAssociative 6) 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (f p)) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (g p)))) | |||||
Void: used for datatypes without constructors
Instances
| Generic1 (V1 :: k -> Type) | |
Defined in GHC.Generics | |
| Foldable (V1 :: Type -> Type) | Since: base-4.9.0.0 |
Defined in Data.Foldable Methods fold :: Monoid m => V1 m -> m # foldMap :: Monoid m => (a -> m) -> V1 a -> m # foldMap' :: Monoid m => (a -> m) -> V1 a -> m # foldr :: (a -> b -> b) -> b -> V1 a -> b # foldr' :: (a -> b -> b) -> b -> V1 a -> b # foldl :: (b -> a -> b) -> b -> V1 a -> b # foldl' :: (b -> a -> b) -> b -> V1 a -> b # foldr1 :: (a -> a -> a) -> V1 a -> a # foldl1 :: (a -> a -> a) -> V1 a -> a # elem :: Eq a => a -> V1 a -> Bool # maximum :: Ord a => V1 a -> a # | |
| Foldable1 (V1 :: Type -> Type) | Since: base-4.18.0.0 |
Defined in Data.Foldable1 Methods fold1 :: Semigroup m => V1 m -> m # foldMap1 :: Semigroup m => (a -> m) -> V1 a -> m # foldMap1' :: Semigroup m => (a -> m) -> V1 a -> m # toNonEmpty :: V1 a -> NonEmpty a # maximum :: Ord a => V1 a -> a # minimum :: Ord a => V1 a -> a # foldrMap1 :: (a -> b) -> (a -> b -> b) -> V1 a -> b # foldlMap1' :: (a -> b) -> (b -> a -> b) -> V1 a -> b # foldlMap1 :: (a -> b) -> (b -> a -> b) -> V1 a -> b # foldrMap1' :: (a -> b) -> (a -> b -> b) -> V1 a -> b # | |
| Contravariant (V1 :: Type -> Type) | |
| Traversable (V1 :: Type -> Type) | Since: base-4.9.0.0 |
| Functor (V1 :: Type -> Type) | Since: base-4.9.0.0 |
| Data p => Data (V1 p) | Since: base-4.9.0.0 |
Defined in Data.Data Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> V1 p -> c (V1 p) # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (V1 p) # dataTypeOf :: V1 p -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (V1 p)) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (V1 p)) # gmapT :: (forall b. Data b => b -> b) -> V1 p -> V1 p # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> V1 p -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> V1 p -> r # gmapQ :: (forall d. Data d => d -> u) -> V1 p -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> V1 p -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> V1 p -> m (V1 p) # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> V1 p -> m (V1 p) # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> V1 p -> m (V1 p) # | |
| Semigroup (V1 p) | Since: base-4.12.0.0 |
| Generic (V1 p) | |
| Read (V1 p) | Since: base-4.9.0.0 |
| Show (V1 p) | Since: base-4.9.0.0 |
| Eq (V1 p) | Since: base-4.9.0.0 |
| Ord (V1 p) | Since: base-4.9.0.0 |
| type Rep1 (V1 :: k -> Type) | Since: base-4.9.0.0 |
| type Rep (V1 p) | Since: base-4.9.0.0 |
Unit: used for constructors without arguments
Constructors
| U1 |
Instances
| SubstRep' (U1 :: LoT (t -> k) -> Type) (x :: t) (xs :: LoT k) Source # | |
Defined in Generics.Kind | |
| Generic1 (U1 :: k -> Type) | |
Defined in GHC.Generics | |
| Conv (U1 :: Type -> Type) (U1 :: LoT d -> Type) (tys :: LoT d) Source # | |
Defined in Generics.Kind | |
| MonadZip (U1 :: Type -> Type) | Since: base-4.9.0.0 |
| Foldable (U1 :: Type -> Type) | Since: base-4.9.0.0 |
Defined in Data.Foldable Methods fold :: Monoid m => U1 m -> m # foldMap :: Monoid m => (a -> m) -> U1 a -> m # foldMap' :: Monoid m => (a -> m) -> U1 a -> m # foldr :: (a -> b -> b) -> b -> U1 a -> b # foldr' :: (a -> b -> b) -> b -> U1 a -> b # foldl :: (b -> a -> b) -> b -> U1 a -> b # foldl' :: (b -> a -> b) -> b -> U1 a -> b # foldr1 :: (a -> a -> a) -> U1 a -> a # foldl1 :: (a -> a -> a) -> U1 a -> a # elem :: Eq a => a -> U1 a -> Bool # maximum :: Ord a => U1 a -> a # | |
| Contravariant (U1 :: Type -> Type) | |
| Traversable (U1 :: Type -> Type) | Since: base-4.9.0.0 |
| Alternative (U1 :: Type -> Type) | Since: base-4.9.0.0 |
| Applicative (U1 :: Type -> Type) | Since: base-4.9.0.0 |
| Functor (U1 :: Type -> Type) | Since: base-4.9.0.0 |
| Monad (U1 :: Type -> Type) | Since: base-4.9.0.0 |
| MonadPlus (U1 :: Type -> Type) | Since: base-4.9.0.0 |
| Data p => Data (U1 p) | Since: base-4.9.0.0 |
Defined in Data.Data Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> U1 p -> c (U1 p) # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (U1 p) # dataTypeOf :: U1 p -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (U1 p)) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (U1 p)) # gmapT :: (forall b. Data b => b -> b) -> U1 p -> U1 p # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> U1 p -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> U1 p -> r # gmapQ :: (forall d. Data d => d -> u) -> U1 p -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> U1 p -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> U1 p -> m (U1 p) # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> U1 p -> m (U1 p) # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> U1 p -> m (U1 p) # | |
| Monoid (U1 p) | Since: base-4.12.0.0 |
| Semigroup (U1 p) | Since: base-4.12.0.0 |
| Generic (U1 p) | |
| Read (U1 p) | Since: base-4.9.0.0 |
| Show (U1 p) | Since: base-4.9.0.0 |
| Eq (U1 p) | Since: base-4.9.0.0 |
| Ord (U1 p) | Since: base-4.7.0.0 |
| type SubstRep (U1 :: LoT (t -> k) -> Type) (x :: t) Source # | |
| type Rep1 (U1 :: k -> Type) | Since: base-4.9.0.0 |
| type Rep (U1 p) | Since: base-4.7.0.0 |
newtype M1 i (c :: Meta) (f :: k -> Type) (p :: k) #
Meta-information (constructor names, etc.)
Instances
| SubstRep' f x xs => SubstRep' (M1 i c f :: LoT (t -> k) -> Type) (x :: t) (xs :: LoT k) Source # | |||||
Defined in Generics.Kind | |||||
| Generic1 (M1 i c f :: k -> Type) | |||||
Defined in GHC.Generics Associated Types
| |||||
| Conv f f' tys => Conv (M1 i c f) (f' :: LoT d -> Type) (tys :: LoT d) Source # | |||||
Defined in Generics.Kind Methods toGhcGenerics :: f' tys -> M1 i c f a Source # toKindGenerics :: M1 i c f a -> f' tys Source # | |||||
| Conv f f' tys => Conv (M1 i c f) (M1 i c f' :: LoT d -> Type) (tys :: LoT d) Source # | |||||
Defined in Generics.Kind Methods toGhcGenerics :: M1 i c f' tys -> M1 i c f a Source # toKindGenerics :: M1 i c f a -> M1 i c f' tys Source # | |||||
| MonadFix f => MonadFix (M1 i c f) | Since: base-4.9.0.0 | ||||
Defined in Control.Monad.Fix | |||||
| MonadZip f => MonadZip (M1 i c f) | Since: base-4.9.0.0 | ||||
| Foldable f => Foldable (M1 i c f) | Since: base-4.9.0.0 | ||||
Defined in Data.Foldable Methods fold :: Monoid m => M1 i c f m -> m # foldMap :: Monoid m => (a -> m) -> M1 i c f a -> m # foldMap' :: Monoid m => (a -> m) -> M1 i c f a -> m # foldr :: (a -> b -> b) -> b -> M1 i c f a -> b # foldr' :: (a -> b -> b) -> b -> M1 i c f a -> b # foldl :: (b -> a -> b) -> b -> M1 i c f a -> b # foldl' :: (b -> a -> b) -> b -> M1 i c f a -> b # foldr1 :: (a -> a -> a) -> M1 i c f a -> a # foldl1 :: (a -> a -> a) -> M1 i c f a -> a # elem :: Eq a => a -> M1 i c f a -> Bool # maximum :: Ord a => M1 i c f a -> a # minimum :: Ord a => M1 i c f a -> a # | |||||
| Foldable1 f => Foldable1 (M1 i c f) | Since: base-4.18.0.0 | ||||
Defined in Data.Foldable1 Methods fold1 :: Semigroup m => M1 i c f m -> m # foldMap1 :: Semigroup m => (a -> m) -> M1 i c f a -> m # foldMap1' :: Semigroup m => (a -> m) -> M1 i c f a -> m # toNonEmpty :: M1 i c f a -> NonEmpty a # maximum :: Ord a => M1 i c f a -> a # minimum :: Ord a => M1 i c f a -> a # foldrMap1 :: (a -> b) -> (a -> b -> b) -> M1 i c f a -> b # foldlMap1' :: (a -> b) -> (b -> a -> b) -> M1 i c f a -> b # foldlMap1 :: (a -> b) -> (b -> a -> b) -> M1 i c f a -> b # foldrMap1' :: (a -> b) -> (a -> b -> b) -> M1 i c f a -> b # | |||||
| Contravariant f => Contravariant (M1 i c f) | |||||
| Traversable f => Traversable (M1 i c f) | Since: base-4.9.0.0 | ||||
| Alternative f => Alternative (M1 i c f) | Since: base-4.9.0.0 | ||||
| Applicative f => Applicative (M1 i c f) | Since: base-4.9.0.0 | ||||
| Functor f => Functor (M1 i c f) | Since: base-4.9.0.0 | ||||
| Monad f => Monad (M1 i c f) | Since: base-4.9.0.0 | ||||
| MonadPlus f => MonadPlus (M1 i c f) | Since: base-4.9.0.0 | ||||
| (Data p, Data (f p), Typeable c, Typeable i, Typeable f) => Data (M1 i c f p) | Since: base-4.9.0.0 | ||||
Defined in Data.Data Methods gfoldl :: (forall d b. Data d => c0 (d -> b) -> d -> c0 b) -> (forall g. g -> c0 g) -> M1 i c f p -> c0 (M1 i c f p) # gunfold :: (forall b r. Data b => c0 (b -> r) -> c0 r) -> (forall r. r -> c0 r) -> Constr -> c0 (M1 i c f p) # toConstr :: M1 i c f p -> Constr # dataTypeOf :: M1 i c f p -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c0 (t d)) -> Maybe (c0 (M1 i c f p)) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c0 (t d e)) -> Maybe (c0 (M1 i c f p)) # gmapT :: (forall b. Data b => b -> b) -> M1 i c f p -> M1 i c f p # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> M1 i c f p -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> M1 i c f p -> r # gmapQ :: (forall d. Data d => d -> u) -> M1 i c f p -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> M1 i c f p -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> M1 i c f p -> m (M1 i c f p) # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> M1 i c f p -> m (M1 i c f p) # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> M1 i c f p -> m (M1 i c f p) # | |||||
| Monoid (f p) => Monoid (M1 i c f p) | Since: base-4.12.0.0 | ||||
| Semigroup (f p) => Semigroup (M1 i c f p) | Since: base-4.12.0.0 | ||||
| Generic (M1 i c f p) | |||||
Defined in GHC.Generics Associated Types
| |||||
| Read (f p) => Read (M1 i c f p) | Since: base-4.7.0.0 | ||||
| Show (f p) => Show (M1 i c f p) | Since: base-4.7.0.0 | ||||
| Eq (f p) => Eq (M1 i c f p) | Since: base-4.7.0.0 | ||||
| Ord (f p) => Ord (M1 i c f p) | Since: base-4.7.0.0 | ||||
| type SubstRep (M1 i c f :: LoT (t -> k) -> Type) (x :: t) Source # | |||||
| type Rep1 (M1 i c f :: k -> Type) | Since: base-4.9.0.0 | ||||
Defined in GHC.Generics | |||||
| type Rep (M1 i c f p) | Since: base-4.7.0.0 | ||||
Defined in GHC.Generics | |||||
newtype Field (t :: Atom d Type) (x :: LoT d) where Source #
Fields: used to represent each of the (visible) arguments to a constructor.
Replaces the K1 type from Generics. The type of the field is
represented by an Atom from Atom.
instance GenericK [] (a :&&: LoT0) where type RepK [] = Field Var0 :*: Field ([] :$: Var0)
Constructors
| Field | |
Instances
| Interpret (SubstAtom t2 x) xs ~ Interpret t2 (x ':&&: xs) => SubstRep' (Field t2 :: LoT (t1 -> k) -> Type) (x :: t1) (xs :: LoT k) Source # | |
Defined in Generics.Kind | |
| k ~ Interpret t tys => Conv (K1 p k :: Type -> Type) (Field t :: LoT d -> Type) (tys :: LoT d) Source # | |
Defined in Generics.Kind Methods toGhcGenerics :: Field t tys -> K1 p k a Source # toKindGenerics :: K1 p k a -> Field t tys Source # | |
| Monoid (Interpret t x) => Monoid (Field t x) Source # | |
| Semigroup (Interpret t x) => Semigroup (Field t x) Source # | |
| Show (Interpret t x) => Show (Field t x) Source # | |
| Eq (Interpret t x) => Eq (Field t x) Source # | |
| Ord (Interpret t x) => Ord (Field t x) Source # | |
| type SubstRep (Field t2 :: LoT (t1 -> k) -> Type) (x :: t1) Source # | |
data ((c :: Atom d Constraint) :=>: (f :: LoT d -> Type)) (x :: LoT d) where Source #
Constraints: used to represent constraints in a constructor.
Replaces the (:=>:) type from GHC.Generics.Extra.
data Showable a = Show a => a -> X a instance GenericK Showable (a :&&: LoT0) where type RepK Showable = (Show :$: a) :=>: (Field Var0)
Constructors
| SuchThat :: forall {d} (c :: Atom d Constraint) (x :: LoT d) (f :: LoT d -> Type). Interpret c x => f x -> (c :=>: f) x |
Instances
| (Interpret (SubstAtom c x) xs => InterpretCons c x xs, Interpret c (x ':&&: xs) => InterpretSubst c x xs, SubstRep' f x xs) => SubstRep' (c :=>: f :: LoT (t -> k) -> Type) (x :: t) (xs :: LoT k) Source # | |
Defined in Generics.Kind | |
| (k ~ Interpret t tys, Conv f f' tys) => Conv (k :=>: f) (t :=>: f' :: LoT d -> Type) (tys :: LoT d) Source # | |
Defined in Generics.Kind Methods toGhcGenerics :: (t :=>: f') tys -> (k :=>: f) a Source # toKindGenerics :: (k :=>: f) a -> (t :=>: f') tys Source # | |
| (Interpret c x => Show (f x)) => Show ((c :=>: f) x) Source # | |
| (Interpret c x => Eq (f x)) => Eq ((c :=>: f) x) Source # | |
| (Interpret c x => Ord (f x)) => Ord ((c :=>: f) x) Source # | |
Defined in Generics.Kind | |
| type SubstRep (c :=>: f :: LoT (t -> k) -> Type) (x :: t) Source # | |
data Exists k (f :: LoT (k -> d) -> Type) (x :: LoT d) where Source #
Existentials: a representation of the form E f describes
a constructor whose inner type is represented by f, and where
the type variable at index 0, Var0, is existentially quantified.
data E where E :: t -> Exists instance GenericK E LoT0 where type RepK E = Exists Type (Field Var0)
Constructors
| Exists | |
Atoms for Field
data Atom d (k :: TYPE r) where #
Shape of a type, possibly with type variables.
>>>:kind Kon [] :@: Var0 -- the type [a] for unknown aKon [] :@: Var0 :: Atom (* -> xs) *
Representation of type families
Type families are represented using first-class-families.
For example, the type-level n + m :: -- may expand to the following--Nat
n + m -- using(from GHC.TypeNats ~+)Eval(n+m) -- usingEvalfrom Fcf.Core and(from Fcf.Data.Nat+)
which may be encoded as the following Atom (using Var0 for n and Var1 for m):
Eval((Kon(+):@:Var0):@:Var1) --EvalasAtom's constructor ::Atom(Nat -> Nat -> Type) Nat
kind-generics
uses a different, more systematic encoding of type families for GenericK instances;
see fcf-family for more details.
For example, n + m is instead expanded to the following:
n + m ~Eval(NDFamily(MkName"base" "GHC.TypeNats" "+")P0'(n, '(m, '())))
which gets encoded as the following Atom:
Eval(Kon(NDFamily(MkName"base" "GHC.TypeNats" "+")P0):@:((Kon'(,):@:Var0):@:((Kon'(,):@:Var1):@:Kon'()))) ::Atom(Nat -> Nat -> Type) Nat
Constructors
| Var :: forall d k1. TyVar d k1 -> Atom d k1 | Represents a type variable. |
| Kon :: forall k1 d. k1 -> Atom d k1 | Represents a constant type, like |
| (:@:) :: forall d k1 k2. Atom d (k1 -> k2) -> Atom d k1 -> Atom d k2 | Represents type application. |
| (:&:) :: forall d. Atom d Constraint -> Atom d Constraint -> Atom d Constraint infixr 5 | Represents the conjunction of two constraints. |
| ForAll :: forall d1 d. Atom (d1 -> d) Type -> Atom d Type | Represents universal quantification. |
| (:=>>:) :: forall d. Atom d Constraint -> Atom d Type -> Atom d Type infixr 5 | Represents constraint requirement, the "thick arrow" |
| Eval :: forall d k1. Atom d (Exp k1) -> Atom d k1 | Represents a type family application. |
type (:$:) (f :: k1 -> k2) (x :: Atom d k1) = ('Kon f :: Atom d (k1 -> k2)) ':@: x #
Represents an applied constructor.
Instead of Kon [] :: Var0$ you can write @[] :$: Var0$.
type (:~:) (a :: Atom d k1) (b :: Atom d k1) = (('Kon ((~) :: k1 -> k1 -> Constraint) :: Atom d (k1 -> k1 -> Constraint)) ':@: a) ':@: b #
Represents (homogeneous) type equality.
type (:~~:) (a :: Atom d k1) (b :: Atom d k2) = (('Kon ((~~) :: k1 -> k2 -> Constraint) :: Atom d (k1 -> k2 -> Constraint)) ':@: a) ':@: b #
Represents heterogeneous type equality.
type Var2 = 'Var ('VS ('VS ('VZ :: TyVar (k -> xs) k) :: TyVar (x1 -> k -> xs) k) :: TyVar (x -> x1 -> k -> xs) k) #
type Var3 = 'Var ('VS ('VS ('VS ('VZ :: TyVar (k -> xs) k) :: TyVar (x2 -> k -> xs) k) :: TyVar (x1 -> x2 -> k -> xs) k) :: TyVar (x -> x1 -> x2 -> k -> xs) k) #
type Var4 = 'Var ('VS ('VS ('VS ('VS ('VZ :: TyVar (k -> xs) k) :: TyVar (x3 -> k -> xs) k) :: TyVar (x2 -> x3 -> k -> xs) k) :: TyVar (x1 -> x2 -> x3 -> k -> xs) k) :: TyVar (x -> x1 -> x2 -> x3 -> k -> xs) k) #
type Var5 = 'Var ('VS ('VS ('VS ('VS ('VS ('VZ :: TyVar (k -> xs) k) :: TyVar (x4 -> k -> xs) k) :: TyVar (x3 -> x4 -> k -> xs) k) :: TyVar (x2 -> x3 -> x4 -> k -> xs) k) :: TyVar (x1 -> x2 -> x3 -> x4 -> k -> xs) k) :: TyVar (x -> x1 -> x2 -> x3 -> x4 -> k -> xs) k) #
type Var6 = 'Var ('VS ('VS ('VS ('VS ('VS ('VS ('VZ :: TyVar (k -> xs) k) :: TyVar (x5 -> k -> xs) k) :: TyVar (x4 -> x5 -> k -> xs) k) :: TyVar (x3 -> x4 -> x5 -> k -> xs) k) :: TyVar (x2 -> x3 -> x4 -> x5 -> k -> xs) k) :: TyVar (x1 -> x2 -> x3 -> x4 -> x5 -> k -> xs) k) :: TyVar (x -> x1 -> x2 -> x3 -> x4 -> x5 -> k -> xs) k) #
type Var7 = 'Var ('VS ('VS ('VS ('VS ('VS ('VS ('VS ('VZ :: TyVar (k -> xs) k) :: TyVar (x6 -> k -> xs) k) :: TyVar (x5 -> x6 -> k -> xs) k) :: TyVar (x4 -> x5 -> x6 -> k -> xs) k) :: TyVar (x3 -> x4 -> x5 -> x6 -> k -> xs) k) :: TyVar (x2 -> x3 -> x4 -> x5 -> x6 -> k -> xs) k) :: TyVar (x1 -> x2 -> x3 -> x4 -> x5 -> x6 -> k -> xs) k) :: TyVar (x -> x1 -> x2 -> x3 -> x4 -> x5 -> x6 -> k -> xs) k) #
type Var8 = 'Var ('VS ('VS ('VS ('VS ('VS ('VS ('VS ('VS ('VZ :: TyVar (k -> xs) k) :: TyVar (x7 -> k -> xs) k) :: TyVar (x6 -> x7 -> k -> xs) k) :: TyVar (x5 -> x6 -> x7 -> k -> xs) k) :: TyVar (x4 -> x5 -> x6 -> x7 -> k -> xs) k) :: TyVar (x3 -> x4 -> x5 -> x6 -> x7 -> k -> xs) k) :: TyVar (x2 -> x3 -> x4 -> x5 -> x6 -> x7 -> k -> xs) k) :: TyVar (x1 -> x2 -> x3 -> x4 -> x5 -> x6 -> x7 -> k -> xs) k) :: TyVar (x -> x1 -> x2 -> x3 -> x4 -> x5 -> x6 -> x7 -> k -> xs) k) #
type Var9 = 'Var ('VS ('VS ('VS ('VS ('VS ('VS ('VS ('VS ('VS ('VZ :: TyVar (k -> xs) k) :: TyVar (x8 -> k -> xs) k) :: TyVar (x7 -> x8 -> k -> xs) k) :: TyVar (x6 -> x7 -> x8 -> k -> xs) k) :: TyVar (x5 -> x6 -> x7 -> x8 -> k -> xs) k) :: TyVar (x4 -> x5 -> x6 -> x7 -> x8 -> k -> xs) k) :: TyVar (x3 -> x4 -> x5 -> x6 -> x7 -> x8 -> k -> xs) k) :: TyVar (x2 -> x3 -> x4 -> x5 -> x6 -> x7 -> x8 -> k -> xs) k) :: TyVar (x1 -> x2 -> x3 -> x4 -> x5 -> x6 -> x7 -> x8 -> k -> xs) k) :: TyVar (x -> x1 -> x2 -> x3 -> x4 -> x5 -> x6 -> x7 -> x8 -> k -> xs) k) #
Lists of types
LoT k represents a list of types which can be applied
to a data type of kind k.
Constructors
| LoT0 :: LoT Type | Empty list of types. |
| (:&&:) :: forall k1 ks. k1 -> LoT ks -> LoT (k1 -> ks) infixr 5 | Cons a type with a list of types. |
Instances
| SubstRep' (U1 :: LoT (t -> k) -> Type) (x :: t) (xs :: LoT k) Source # | |
Defined in Generics.Kind | |
| (SubstRep' f x xs, SubstRep' g x xs) => SubstRep' (f :*: g :: LoT (t -> k) -> Type) (x :: t) (xs :: LoT k) Source # | |
Defined in Generics.Kind | |
| (SubstRep' f x xs, SubstRep' g x xs) => SubstRep' (f :+: g :: LoT (t -> k) -> Type) (x :: t) (xs :: LoT k) Source # | |
Defined in Generics.Kind | |
| SubstRep' f x xs => SubstRep' (M1 i c f :: LoT (t -> k) -> Type) (x :: t) (xs :: LoT k) Source # | |
Defined in Generics.Kind | |
| Conv (U1 :: Type -> Type) (U1 :: LoT d -> Type) (tys :: LoT d) Source # | |
Defined in Generics.Kind | |
| (Conv f f' tys, Conv g g' tys) => Conv (f :*: g) (f' :*: g' :: LoT d -> Type) (tys :: LoT d) Source # | |
Defined in Generics.Kind Methods toGhcGenerics :: (f' :*: g') tys -> (f :*: g) a Source # toKindGenerics :: (f :*: g) a -> (f' :*: g') tys Source # | |
| (Conv f f' tys, Conv g g' tys) => Conv (f :+: g) (f' :+: g' :: LoT d -> Type) (tys :: LoT d) Source # | |
Defined in Generics.Kind Methods toGhcGenerics :: (f' :+: g') tys -> (f :+: g) a Source # toKindGenerics :: (f :+: g) a -> (f' :+: g') tys Source # | |
| Conv f f' tys => Conv (M1 i c f) (M1 i c f' :: LoT d -> Type) (tys :: LoT d) Source # | |
Defined in Generics.Kind Methods toGhcGenerics :: M1 i c f' tys -> M1 i c f a Source # toKindGenerics :: M1 i c f a -> M1 i c f' tys Source # | |
| type SubstRep (U1 :: LoT (t -> k) -> Type) (x :: t) Source # | |
| type SubstRep (f :*: g :: LoT (t -> k) -> Type) (x :: t) Source # | |
| type SubstRep (f :+: g :: LoT (t -> k) -> Type) (x :: t) Source # | |
| type SubstRep (M1 i c f :: LoT (t -> k) -> Type) (x :: t) Source # | |
type family (f :: k) :@@: (tys :: LoT k) where ... #
Apply a list of types to a type constructor.
>>>:kind! Either :@@: (Int :&&: Bool :&&: LoT0)Either Int Bool :: Type
A type constructor and a list of types that can be applied to it.
Generic type classes
class GenericK (f :: k) where Source #
Representable types of any kind. Examples:
instance GenericK Int instance GenericK [] instance GenericK Either instance GenericK (Either a) instance GenericK (Either a b)
Minimal complete definition
Nothing
Methods
fromK :: forall (x :: LoT k). (f :@@: x) -> RepK f x Source #
Convert the data type to its representation.
default fromK :: forall (x :: LoT k). (Generic (f :@@: x), Conv (Rep (f :@@: x)) (RepK f) x) => (f :@@: x) -> RepK f x Source #
toK :: forall (x :: LoT k). RepK f x -> f :@@: x Source #
Convert from a representation to its corresponding data type.
Instances
type GenericN (n :: Nat) t (f :: k) (x :: LoT k) = (GenericK f, 'TyEnv f x ~ SplitN n t, t ~ (f :@@: x)) Source #
Getting more instances almost for free
fromRepK :: forall {t} {k} (f :: t -> k) (x :: t) (xs :: LoT k). (GenericK f, SubstRep' (RepK f) x xs) => (f x :@@: xs) -> SubstRep (RepK f) x xs Source #
toRepK :: forall {t} {k} (f :: t -> k) (x :: t) (xs :: LoT k). (GenericK f, SubstRep' (RepK f) x xs) => SubstRep (RepK f) x xs -> f x :@@: xs Source #
type family SubstRep (f :: LoT (t -> k) -> Type) (x :: t) :: LoT k -> Type Source #
Instances
| type SubstRep (U1 :: LoT (t -> k) -> Type) (x :: t) Source # | |
| type SubstRep (Field t2 :: LoT (t1 -> k) -> Type) (x :: t1) Source # | |
| type SubstRep (f :*: g :: LoT (t -> k) -> Type) (x :: t) Source # | |
| type SubstRep (f :+: g :: LoT (t -> k) -> Type) (x :: t) Source # | |
| type SubstRep (c :=>: f :: LoT (t -> k) -> Type) (x :: t) Source # | |
| type SubstRep (M1 i c f :: LoT (t -> k) -> Type) (x :: t) Source # | |
class SubstRep' (f :: LoT (t -> k) -> Type) (x :: t) (xs :: LoT k) Source #
Minimal complete definition
substRep, unsubstRep
Instances
| SubstRep' (U1 :: LoT (t -> k) -> Type) (x :: t) (xs :: LoT k) Source # | |
Defined in Generics.Kind | |
| Interpret (SubstAtom t2 x) xs ~ Interpret t2 (x ':&&: xs) => SubstRep' (Field t2 :: LoT (t1 -> k) -> Type) (x :: t1) (xs :: LoT k) Source # | |
Defined in Generics.Kind | |
| (SubstRep' f x xs, SubstRep' g x xs) => SubstRep' (f :*: g :: LoT (t -> k) -> Type) (x :: t) (xs :: LoT k) Source # | |
Defined in Generics.Kind | |
| (SubstRep' f x xs, SubstRep' g x xs) => SubstRep' (f :+: g :: LoT (t -> k) -> Type) (x :: t) (xs :: LoT k) Source # | |
Defined in Generics.Kind | |
| (Interpret (SubstAtom c x) xs => InterpretCons c x xs, Interpret c (x ':&&: xs) => InterpretSubst c x xs, SubstRep' f x xs) => SubstRep' (c :=>: f :: LoT (t -> k) -> Type) (x :: t) (xs :: LoT k) Source # | |
Defined in Generics.Kind | |
| SubstRep' f x xs => SubstRep' (M1 i c f :: LoT (t -> k) -> Type) (x :: t) (xs :: LoT k) Source # | |
Defined in Generics.Kind | |
type family SubstAtom (f :: Atom (t -> k) d) (x :: t) :: Atom k d where ... Source #
Equations
| SubstAtom ('Var ('VZ :: TyVar (k1 -> k) k1) :: Atom (k1 -> k) k1) (x :: k1) = 'Kon x :: Atom k k1 | |
| SubstAtom ('Var ('VS v :: TyVar (t -> d) k1) :: Atom (t -> d) k1) (x :: t) = 'Var v | |
| SubstAtom ('Kon t2 :: Atom (t1 -> k) k1) (x :: t1) = 'Kon t2 :: Atom k k1 | |
| SubstAtom (t1 ':@: t2 :: Atom (t -> k) k2) (x :: t) = SubstAtom t1 x ':@: SubstAtom t2 x | |
| SubstAtom (t1 ':&: t2 :: Atom (t -> k) Constraint) (x :: t) = SubstAtom t1 x ':&: SubstAtom t2 x |
Bridging with GHC.Generics
class Conv (gg :: Type -> Type) (kg :: LoT d -> Type) (tys :: LoT d) where Source #
Bridges a representation of a data type using the combinators
in GHC.Generics with a representation using this module.
You are never expected to manipulate this type class directly,
it is part of the deriving mechanism for GenericK.
Instances
| Conv (U1 :: Type -> Type) (U1 :: LoT d -> Type) (tys :: LoT d) Source # | |
Defined in Generics.Kind | |
| k ~ Interpret t tys => Conv (K1 p k :: Type -> Type) (Field t :: LoT d -> Type) (tys :: LoT d) Source # | |
Defined in Generics.Kind Methods toGhcGenerics :: Field t tys -> K1 p k a Source # toKindGenerics :: K1 p k a -> Field t tys Source # | |
| (Conv f f' tys, Conv g g' tys) => Conv (f :*: g) (f' :*: g' :: LoT d -> Type) (tys :: LoT d) Source # | |
Defined in Generics.Kind Methods toGhcGenerics :: (f' :*: g') tys -> (f :*: g) a Source # toKindGenerics :: (f :*: g) a -> (f' :*: g') tys Source # | |
| (Conv f f' tys, Conv g g' tys) => Conv (f :+: g) (f' :+: g' :: LoT d -> Type) (tys :: LoT d) Source # | |
Defined in Generics.Kind Methods toGhcGenerics :: (f' :+: g') tys -> (f :+: g) a Source # toKindGenerics :: (f :+: g) a -> (f' :+: g') tys Source # | |
| (k ~ Interpret t tys, Conv f f' tys) => Conv (k :=>: f) (t :=>: f' :: LoT d -> Type) (tys :: LoT d) Source # | |
Defined in Generics.Kind Methods toGhcGenerics :: (t :=>: f') tys -> (k :=>: f) a Source # toKindGenerics :: (k :=>: f) a -> (t :=>: f') tys Source # | |
| Conv f f' tys => Conv (M1 i c f) (f' :: LoT d -> Type) (tys :: LoT d) Source # | |
Defined in Generics.Kind Methods toGhcGenerics :: f' tys -> M1 i c f a Source # toKindGenerics :: M1 i c f a -> f' tys Source # | |
| Conv f f' tys => Conv (M1 i c f) (M1 i c f' :: LoT d -> Type) (tys :: LoT d) Source # | |
Defined in Generics.Kind Methods toGhcGenerics :: M1 i c f' tys -> M1 i c f a Source # toKindGenerics :: M1 i c f a -> M1 i c f' tys Source # | |
Re-exported from Atom
Interpretation of atoms
type family Interpret (t :: Atom d k) (tys :: LoT d) :: k where ... #
Replaces the holes in the Atom t by the elements of
the list of types tys. The amount and kind of types in tys
must match statically those required by the Atom.
>>>:kind! Interpret ([] :$: Var0) (LoT1 Int)Interpret ([] :$: Var0) (LoT1 Int) :: * = [Int]
Equations
| Interpret ('Var v :: Atom d k) (tys :: LoT d) = InterpretVar v tys | |
| Interpret ('Kon t :: Atom d k) (tys :: LoT d) = t | |
| Interpret (f ':@: x :: Atom d k2) (tys :: LoT d) = Interpret f tys (Interpret x tys) | |
| Interpret (c ':&: d2 :: Atom d1 Constraint) (tys :: LoT d1) = (Interpret c tys, Interpret d2 tys) | |
| Interpret ('ForAll f :: Atom d Type) (tys :: LoT d) = ForAllI f tys | |
| Interpret (c ':=>>: f :: Atom d Type) (tys :: LoT d) = SuchThatI c f tys | |
| Interpret ('Eval f :: Atom d a) (tys :: LoT d) = Eval (Interpret f tys) |
type family InterpretVar (t :: TyVar d k) (tys :: LoT d) :: k where ... #
Obtains the type in the list tys referenced
by the type variable t.
>>>:kind! Interpret Var0 (LoT2 Int Bool)Interpret Var0 (LoT2 Int Bool) :: * = Int>>>:kind! Interpret Var1 (LoT2 Int Bool)Interpret Var1 (LoT2 Int Bool) :: * = Bool
Equations
| InterpretVar ('VZ :: TyVar (k -> k') k) (tys :: LoT (k -> k')) = HeadLoT tys | |
| InterpretVar ('VS v :: TyVar (k2 -> k') k1) (tys :: LoT (k2 -> k')) = InterpretVar v (TailLoT tys) |
type family Satisfies (cs :: [Atom d Constraint]) (tys :: LoT d) where ... #
Interprets a list of Atom representing constraints
into the actual constraints. This is a specialization of
Interpret for the case of constraints.
>>>:kind! Satisfies '[Eq :$: Var0, Show :$: Var0] (LoT1 Int)Satisfies '[Eq :$: Var0, Show :$: Var0] (LoT1 Int) :: Constraint = (Eq Int, (Show Int, () :: Constraint))
Equations
| Satisfies ('[] :: [Atom d Constraint]) (tys :: LoT d) = () | |
| Satisfies (c ': cs :: [Atom d Constraint]) (tys :: LoT d) = (Interpret c tys, Satisfies cs tys) |
type family ContainsTyVar (v :: TyVar d k) (t :: Atom d p) :: Bool where ... #
Determines whether a given type variable v is used within an Atom t.
If not, we know that the atom is constant with respect to that variable.
Equations
| ContainsTyVar (v :: TyVar d p) ('Var v :: Atom d p) = 'True | |
| ContainsTyVar (v :: TyVar d k) ('Var w :: Atom d p) = 'False | |
| ContainsTyVar (v :: TyVar d k) ('Kon t :: Atom d p) = 'False | |
| ContainsTyVar (v :: TyVar d k) (f ':@: x :: Atom d p2) = Or (ContainsTyVar v f) (ContainsTyVar v x) | |
| ContainsTyVar (v :: TyVar d k) (x ':&: y :: Atom d Constraint) = Or (ContainsTyVar v x) (ContainsTyVar v y) | |
| ContainsTyVar (v :: TyVar d k) (c ':=>>: f :: Atom d Type) = Or (ContainsTyVar v c) (ContainsTyVar v f) | |
| ContainsTyVar (v :: TyVar xs k) ('ForAll f :: Atom xs Type) = ContainsTyVar ('VS v :: TyVar (x -> xs) k) f |
Auxiliary data types for interpretation
newtype ForAllI (f :: Atom (d1 -> d) Type) (tys :: LoT d) where #
newtype SuchThatI (c :: Atom d Constraint) (f :: Atom d Type) (tys :: LoT d) where #
Auxiliary type for interpretation of the (:=>>:) atom.
Required because a type family like Interpret cannot return
a type with constraints.
Constructors
| SuchThatI | |
Fields
| |
newtype WrappedI (f :: Atom d Type) (tys :: LoT d) #
Records a value of type f applied to the list tys.
>>>:t WrapI [1] :: WrappedI ([] :$: Var0) (LoT1 Int)WrapI [1] :: WrappedI ([] :$: Var0) (LoT1 Int)