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 +41/−3
- kind-generics.cabal +4/−2
- src/Generics/Kind.hs +8/−1
- src/Generics/Kind/Examples.hs +24/−0
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