packages feed

kind-generics 0.4.1.4 → 0.5.0.0

raw patch · 4 files changed

+77/−6 lines, 4 filesdep +first-class-familiesdep ~kind-applyPVP ok

version bump matches the API change (PVP)

Dependencies added: first-class-families

Dependency ranges changed: kind-apply

API changes (from Hackage documentation)

- Generics.Kind: instance forall d (t :: Data.PolyKinded.Atom.Atom d *) (x :: Data.PolyKinded.LoT d). GHC.Show.Show (Data.PolyKinded.Atom.Interpret t x) => GHC.Show.Show (Generics.Kind.Field t x)
- Generics.Kind: instance forall d k (t :: Data.PolyKinded.Atom.Atom d *) (tys :: Data.PolyKinded.LoT d) p. (k GHC.Types.~ Data.PolyKinded.Atom.Interpret t tys) => Generics.Kind.Conv (GHC.Generics.K1 p k) (Generics.Kind.Field t) tys
- Generics.Kind: instance forall t1 k (t2 :: Data.PolyKinded.Atom.Atom (t1 -> k) *) (x :: t1) (xs :: Data.PolyKinded.LoT k). (Data.PolyKinded.Atom.Interpret (Generics.Kind.SubstAtom t2 x) xs GHC.Types.~ Data.PolyKinded.Atom.Interpret t2 (x 'Data.PolyKinded.:&&: xs)) => Generics.Kind.SubstRep' (Generics.Kind.Field t2) x xs
+ Generics.Kind: [Eval] :: forall d k1. Atom d (Exp k1) -> Atom d k1
+ Generics.Kind: instance forall d (c :: Data.PolyKinded.Atom.Atom d GHC.Types.Constraint) (x :: Data.PolyKinded.LoT d) (f :: Data.PolyKinded.LoT d -> *). (Data.PolyKinded.Atom.Interpret c x => GHC.Classes.Eq (f x)) => GHC.Classes.Eq ((Generics.Kind.:=>:) c f x)
+ Generics.Kind: instance forall d (c :: Data.PolyKinded.Atom.Atom d GHC.Types.Constraint) (x :: Data.PolyKinded.LoT d) (f :: Data.PolyKinded.LoT d -> *). (Data.PolyKinded.Atom.Interpret c x => GHC.Classes.Ord (f x)) => GHC.Classes.Ord ((Generics.Kind.:=>:) c f x)
+ Generics.Kind: instance forall d (t :: Data.PolyKinded.Atom.Atom d (*)) (x :: Data.PolyKinded.LoT d). GHC.Base.Monoid (Data.PolyKinded.Atom.Interpret t x) => GHC.Base.Monoid (Generics.Kind.Field t x)
+ Generics.Kind: instance forall d (t :: Data.PolyKinded.Atom.Atom d (*)) (x :: Data.PolyKinded.LoT d). GHC.Base.Semigroup (Data.PolyKinded.Atom.Interpret t x) => GHC.Base.Semigroup (Generics.Kind.Field t x)
+ Generics.Kind: instance forall d (t :: Data.PolyKinded.Atom.Atom d (*)) (x :: Data.PolyKinded.LoT d). GHC.Classes.Eq (Data.PolyKinded.Atom.Interpret t x) => GHC.Classes.Eq (Generics.Kind.Field t x)
+ Generics.Kind: instance forall d (t :: Data.PolyKinded.Atom.Atom d (*)) (x :: Data.PolyKinded.LoT d). GHC.Classes.Ord (Data.PolyKinded.Atom.Interpret t x) => GHC.Classes.Ord (Generics.Kind.Field t x)
+ Generics.Kind: instance forall d (t :: Data.PolyKinded.Atom.Atom d (*)) (x :: Data.PolyKinded.LoT d). GHC.Show.Show (Data.PolyKinded.Atom.Interpret t x) => GHC.Show.Show (Generics.Kind.Field t x)
+ Generics.Kind: instance forall d k (t :: Data.PolyKinded.Atom.Atom d (*)) (tys :: Data.PolyKinded.LoT d) p. (k GHC.Types.~ Data.PolyKinded.Atom.Interpret t tys) => Generics.Kind.Conv (GHC.Generics.K1 p k) (Generics.Kind.Field t) tys
+ Generics.Kind: instance forall t1 k (t2 :: Data.PolyKinded.Atom.Atom (t1 -> k) (*)) (x :: t1) (xs :: Data.PolyKinded.LoT k). (Data.PolyKinded.Atom.Interpret (Generics.Kind.SubstAtom t2 x) xs GHC.Types.~ Data.PolyKinded.Atom.Interpret t2 (x 'Data.PolyKinded.:&&: xs)) => Generics.Kind.SubstRep' (Generics.Kind.Field t2) x xs
+ Generics.Kind: type RepK f :: LoT k -> Type;
+ Generics.Kind: type SubstRep f x :: LoT k -> Type
+ Generics.Kind.Examples: Hkd :: Eval (f a) -> Hkd f a
+ Generics.Kind.Examples: instance Generics.Kind.GenericK Generics.Kind.Examples.Hkd
+ Generics.Kind.Examples: instance forall k (f :: k -> Fcf.Core.Exp (*)) (a :: k). Generics.Kind.GenericK (Generics.Kind.Examples.Hkd f a)
+ Generics.Kind.Examples: instance forall k (f :: k -> Fcf.Core.Exp (*)). Generics.Kind.GenericK (Generics.Kind.Examples.Hkd f)
+ Generics.Kind.Examples: newtype Hkd f a
- Generics.Kind: [Exists] :: forall k (t :: k) d (f :: LoT (k -> d) -> Type) (x :: LoT d). {unExists :: f (t :&&: x)} -> Exists k f x
+ Generics.Kind: [Exists] :: forall k (t :: k) d (f :: LoT (k -> d) -> Type) (x :: LoT d). f (t ':&&: x) -> Exists k f x
- Generics.Kind: [Field] :: {unField :: Interpret t x} -> Field t x
+ Generics.Kind: [Field] :: Interpret t x -> Field t x
- Generics.Kind: [ForAllI] :: forall d1 d (f :: Atom (d1 -> d) Type) (tys :: LoT d). (forall (t :: d1). () => Interpret f (t :&&: tys)) -> ForAllI f tys
+ Generics.Kind: [ForAllI] :: forall {d1} {d} (f :: Atom (d1 -> d) Type) (tys :: LoT d). (forall (t :: d1). () => Interpret f (t ':&&: tys)) -> ForAllI f tys
- Generics.Kind: [SuchThatI] :: forall d (c :: Atom d Constraint) (tys :: LoT d) (f :: Atom d Type). (Interpret c tys => Interpret f tys) -> SuchThatI c f tys
+ Generics.Kind: [SuchThatI] :: forall {d} (c :: Atom d Constraint) (tys :: LoT d) (f :: Atom d Type). (Interpret c tys => Interpret f tys) -> SuchThatI c f tys
- Generics.Kind: data Atom d (k :: TYPE r)
+ Generics.Kind: data () => Atom d (k :: TYPE r)
- Generics.Kind: data LoT k
+ Generics.Kind: data () => LoT k
- Generics.Kind: data TyEnv
+ Generics.Kind: data () => TyEnv
- Generics.Kind: data TyVar d (k :: TYPE r)
+ Generics.Kind: data () => TyVar d (k :: TYPE r)
- Generics.Kind: data U1 (p :: k)
+ Generics.Kind: data () => U1 (p :: k)
- Generics.Kind: data V1 (p :: k)
+ Generics.Kind: data () => V1 (p :: k)
- Generics.Kind: fromWrappedI :: forall d1 d (f :: Atom (d1 -> d) Type) (tys :: LoT d). (forall (t :: d1). () => WrappedI f (t :&&: tys)) -> ForAllI f tys
+ Generics.Kind: fromWrappedI :: forall {d1} {d} (f :: Atom (d1 -> d) Type) (tys :: LoT d). (forall (t :: d1). () => WrappedI f (t ':&&: tys)) -> ForAllI f tys
- Generics.Kind: infixr 5 :&&:
+ Generics.Kind: infixr 5 :+:
- Generics.Kind: newtype ForAllI (f :: Atom d1 -> d Type) (tys :: LoT d)
+ Generics.Kind: newtype () => ForAllI (f :: Atom d1 -> d Type) (tys :: LoT d)
- Generics.Kind: newtype M1 i (c :: Meta) (f :: k -> Type) (p :: k)
+ Generics.Kind: newtype () => M1 i (c :: Meta) (f :: k -> Type) (p :: k)
- Generics.Kind: newtype SuchThatI (c :: Atom d Constraint) (f :: Atom d Type) (tys :: LoT d)
+ Generics.Kind: newtype () => SuchThatI (c :: Atom d Constraint) (f :: Atom d Type) (tys :: LoT d)
- Generics.Kind: newtype WrappedI (f :: Atom d Type) (tys :: LoT d)
+ Generics.Kind: newtype () => WrappedI (f :: Atom d Type) (tys :: LoT d)
- Generics.Kind: toWrappedI :: forall d1 ks (f :: Atom (d1 -> ks) Type) (tys :: LoT ks) (t :: d1). ForAllI f tys -> WrappedI f (t :&&: tys)
+ Generics.Kind: toWrappedI :: forall {d1} {ks} (f :: Atom (d1 -> ks) Type) (tys :: LoT ks) (t :: d1). ForAllI f tys -> WrappedI f (t ':&&: tys)
- Generics.Kind: type (a :: Atom d k1) :~~: (b :: Atom d k2) = 'Kon (~~) :: k1 -> k2 -> Constraint :: Atom d k1 -> k2 -> Constraint :@: a :@: b
+ Generics.Kind: type (a :: Atom d k1) :~~: (b :: Atom d k2) = 'Kon (~~) :: k1 -> k2 -> Constraint :: Atom d k1 -> k2 -> Constraint ':@: a ':@: b
- Generics.Kind: type LoT1 (a :: k) = a :&&: 'LoT0
+ Generics.Kind: type LoT1 (a :: k) = a ':&&: 'LoT0
- Generics.Kind: type LoT2 (a :: k) (b :: k1) = a :&&: b :&&: 'LoT0
+ Generics.Kind: type LoT2 (a :: k) (b :: k1) = a ':&&: b ':&&: 'LoT0

Files

README.md view
@@ -77,7 +77,7 @@  ```haskell class GenericK (f :: k) where-  type RepK f :: LoT k -> *+  type family RepK f :: LoT k -> *   fromK :: f :@@: x -> RepK f x   toK   :: RepK f x -> f :@@: x ```@@ -126,7 +126,7 @@ instance GenericK (Either a b) where ... ``` -Sometimes it is not possible to write all of these instances, due to restrictions in GHC's type system. The most common case is a data type making use of a type family -- we cannot write something like `Fam :$: Var0` because type families cannot be partially applied. The `kind-generics-th` package contains a thorough description of these limitations.+Sometimes it is not possible to write all of these instances, due to restrictions in GHC's type system. The `kind-generics-th` package contains a thorough description of these limitations.  ## Describing fields: the functor `Field` @@ -221,6 +221,44 @@  You just need to apply the `Exists` and `SuchThat` constructors every time there is an existential or constraint, respectively. However, since the additional information required by those types is implicitly added by the compiler, you do not need to write anything else. +## Atoms for families: `Eval`++If a field contains a type family application, it can be represented by+defunctionalization. For example:++```haskell+type family F a++data T a = C (F a)+```++`F` can be defunctionalized as follows, using `Fcf.Eval` from+[`first-class-families`](https://hackage.haskell.org/package/first-class-families).++```haskell+data DF a+type Fcf.Eval (DF a) = F a+```++All type family applications can thus be rewritten as the application of one+common `Fcf.Eval` to a matchable application. This can then be represented by+one `Atom` constructor, also named `Eval`:++```haskell+instance GenericK T where+  type RepK T = Field (Eval (Kon DF :@: Var0))++  fromK (C x) = Field x+  toK (Field x) = C x+```++`kind-generics-th` can generate `GenericK` instances for such types involving+type families. It also takes care of defunctionalizing type families as needed,+following a more sophisticated approach than described above, that avoids+declaring lots of artificial data types. For more details, see+[`fcf-family`](https://hackage.haskell.org/package/fcf-family)+and the documentation of `kind-generics-th`.+ ## Implementing a generic operation with `kind-generics`  The last stop in our journey through `kind-generics` is being able to implement a generic operation. At this point we assume that the reader is comfortable with the definition of generic operations using `GHC.Generics`, so only the differences with that style are pointed out.@@ -266,7 +304,7 @@  ```haskell class GShow (f :: LoT k -> *) where-  type ReqsShow f (x :: LoT k) :: Constraint+  type family ReqsShow f (x :: LoT k) :: Constraint   gshow :: ReqsShow f x => f x -> String  gshow' :: forall t. (GenericK t LoT0
kind-generics.cabal view
@@ -1,6 +1,6 @@ cabal-version:       >=1.10 name:                kind-generics-version:             0.4.1.4+version:             0.5.0.0 synopsis:            Generic programming in GHC style for arbitrary kinds and GADTs. description:         This package provides functionality to extend the data type generic programming functionality in GHC to classes of arbitrary kind, and constructors featuring constraints and existentials, as usually found in GADTs. -- bug-reports:@@ -22,7 +22,9 @@                        Generics.Kind.Examples   -- other-modules:   -- other-extensions:-  build-depends:       base >= 4.12 && < 5, kind-apply >= 0.3+  build-depends:       base >= 4.12 && < 5+                     , kind-apply >= 0.4 && < 0.5+                     , first-class-families >= 0.8 && < 0.9   hs-source-dirs:      src   default-language:    Haskell2010   ghc-options:         -Wall
src/Generics/Kind.hs view
@@ -6,6 +6,7 @@ {-# language FlexibleContexts          #-} {-# language FlexibleInstances         #-} {-# language GADTs                     #-}+{-# language GeneralizedNewtypeDeriving #-} {-# language MultiParamTypeClasses     #-} {-# language PolyKinds                 #-} {-# language QuantifiedConstraints     #-}@@ -61,6 +62,10 @@   -- and https://ghc.haskell.org/trac/ghc/ticket/14917   -- are implemented, we are restricted to the Type kind   Field :: { unField :: Interpret t x } -> Field t x+deriving instance Eq (Interpret t x) => Eq (Field t x)+deriving instance Ord (Interpret t x) => Ord (Field t x)+deriving instance Semigroup (Interpret t x) => Semigroup (Field t x)+deriving instance Monoid (Interpret t x) => Monoid (Field t x) deriving instance Show (Interpret t x) => Show (Field t x)  -- | Constraints: used to represent constraints in a constructor.@@ -72,6 +77,8 @@ -- >   type RepK Showable = (Show :$: a) :=>: (Field Var0) data (:=>:) (c :: Atom d Constraint) (f :: LoT d -> Type) (x :: LoT d) where   SuchThat :: Interpret c x => f x -> (c :=>: f) x+deriving instance (Interpret c x => Eq (f x)) => Eq ((c :=>: f) x)+deriving instance (Interpret c x => Ord (f x)) => Ord ((c :=>: f) x) deriving instance (Interpret c x => Show (f x)) => Show ((c :=>: f) x)  -- | Existentials: a representation of the form @E f@ describes@@ -98,7 +105,7 @@ -- > instance GenericK (Either a) -- > instance GenericK (Either a b) class GenericK (f :: k) where-  type RepK f :: LoT k -> Type+  type family RepK f :: LoT k -> Type    -- | Convert the data type to its representation.   fromK :: f :@@: x -> RepK f x
src/Generics/Kind/Examples.hs view
@@ -18,6 +18,7 @@ import           GHC.TypeLits import           Type.Reflection (Typeable) +import qualified Fcf.Core as Fcf import           Generics.Kind  -- Obtained from Generic@@ -242,3 +243,26 @@   fromK = undefined   toK   = undefined -}++-- Type families++-- HKD pattern, defunctionalized variant+newtype Hkd f a = Hkd (Fcf.Eval (f a))++-- Simplified encoding compared to kind-generics-th.+-- Fcf.Eval in Hkd could be any other type family, so a general+-- implementation would have to defunctionalize it.+instance GenericK Hkd where+  type RepK Hkd = Field (Eval (Var0 :@: Var1))+  fromK (Hkd x) = Field x+  toK (Field x) = Hkd x++instance GenericK (Hkd f) where+  type RepK (Hkd f) = Field (Eval (Kon f :@: Var0))+  fromK (Hkd x) = Field x+  toK (Field x) = Hkd x++instance GenericK (Hkd f a) where+  type RepK (Hkd f a) = Field (Kon (Fcf.Eval (f a)))+  fromK (Hkd x) = Field x+  toK (Field x) = Hkd x