kind-generics 0.2.0 → 0.2.1.0

raw patch · 3 files changed

+120/−36 lines, 3 filesdep ~kind-applyPVP: major bump suggested

API removals or changes: PVP suggests a major version bump

Dependency ranges changed: kind-apply

API changes (from Hackage documentation)

Files

• kind-generics.cabal +2/−2
• src/Generics/Kind.hs +60/−25
• src/Generics/Kind/Examples.hs +58/−9

@@ -1,6 +1,6 @@ cabal-version:       >=1.10 name:                kind-generics-version:             0.2.0+version:             0.2.1.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 gound in GADTs. -- bug-reports:@@ -22,7 +22,7 @@                        Generics.Kind.Examples   -- other-modules:   -- other-extensions:-  build-depends:       base >=4.12 && <5, kind-apply+  build-depends:       base >=4.12 && <5, kind-apply >= 0.2   hs-source-dirs:      src   default-language:    Haskell2010   ghc-options:         -Wall

@@ -22,12 +22,13 @@ , module Data.PolyKinded.Atom   -- * Generic representation types , (:+:)(..), (:*:)(..), U1(..), M1(..)-, F(..), (:=>:)(..), E(..), ERefl(..)+, F(..), (:=>:)(..), E(..)   -- * Generic type classes , GenericK(..) , GenericF, fromF, toF , GenericN, fromN, toN-, GenericS, fromS, toS+  -- * Getting more instances almost for free+, fromRepK, toRepK, SubstRep   -- * Bridging with "GHC.Generics" , Conv(..) ) where@@ -57,6 +58,7 @@ -- >   type RepK Showable = (Show :$: a) :=>: (F V0) data (:=>:) (c :: Atom d Constraint) (f :: LoT d -> *) (x :: LoT d) where   C :: Ty c x => f x -> (c :=>: f) x+deriving instance (Ty c x => Show (f x)) => Show ((c :=>: f) x)  -- | Existentials: a representation of the form @E f@ describes -- a constructor whose inner type is represented by @f@, and where@@ -70,18 +72,7 @@ data E (f :: LoT (k -> d) -> *) (x :: LoT d) where   E :: forall (t :: k) d (f :: LoT (k -> d) -> *) (x :: LoT d)      . f (t ':&&: x) -> E f x---- | Existentials with reflection: similar to 'E',---   but in addition we remember the type of the existential variable.------ > data Exists where--- >  E :: Typeable t => t -> Exists--- >--- > instance GenericK Exists LoT0 where--- >   type RepK Exists = ERefl (F V0)-data ERefl (f :: LoT (k -> d) -> *) (x :: LoT d) where-  ERefl :: forall (t :: k) d (f :: LoT (k -> d) -> *) (x :: LoT d)-         . Typeable t => f (t ':&&: x) -> ERefl f x+deriving instance (forall t. Show (f (t ':&&: x))) => Show (E f x)  -- THE TYPE CLASS @@ -121,17 +112,61 @@ toN :: forall n t f x. GenericN n t f x => RepK f x -> t toN = toK @_ @f --- | @GenericS t f x@ states that the ground type @t@ is split by--- default as the constructor @f@ and a list of types @x$, and that--- a 'GenericK' instance exists for that constructor.------ This constraint provides an external interface similar to that--- provided by 'Generic' in "GHC.Generics".-type GenericS t f x = (Split t f x, GenericK f x)-fromS :: forall t f x. GenericS t f x => t -> RepK f x-fromS = fromF @f-toS :: forall t f x. GenericS t f x => RepK f x -> t-toS = toF @f+-- CONVERSION BETWEEN FEWER AND MORE ARGUMENTS++fromRepK :: forall f x xs. (GenericK f (x ':&&: xs), SubstRep' (RepK f) x xs)+         => f x :@@: xs -> SubstRep (RepK f) x xs+fromRepK = substRep . fromK @_ @f @(x ':&&: xs)++toRepK :: forall f x xs. (GenericK f (x ':&&: xs), SubstRep' (RepK f) x xs)+       => SubstRep (RepK f) x xs -> f x :@@: xs+toRepK = toK @_ @f @(x ':&&: xs) . unsubstRep++class SubstRep' (f :: LoT (t -> k) -> *) (x :: t) (xs :: LoT k) where+  type family SubstRep f x :: LoT k -> *+  substRep   :: f (x ':&&: xs) -> SubstRep f x xs+  unsubstRep :: SubstRep f x xs -> f (x ':&&: xs)++instance SubstRep' U1 x xs where+  type SubstRep U1 x = U1+  substRep   U1 = U1+  unsubstRep U1 = U1++instance (SubstRep' f x xs, SubstRep' g x xs) => SubstRep' (f :+: g) x xs where+  type SubstRep (f :+: g)  x = (SubstRep f x) :+: (SubstRep g x)+  substRep   (L1 x) = L1 (substRep   x)+  substRep   (R1 x) = R1 (substRep   x)+  unsubstRep (L1 x) = L1 (unsubstRep x)+  unsubstRep (R1 x) = R1 (unsubstRep x)++instance (SubstRep' f x xs, SubstRep' g x xs) => SubstRep' (f :*: g) x xs where+  type SubstRep (f :*: g) x = (SubstRep f x) :*: (SubstRep g x)+  substRep   (x :*: y) = substRep   x :*: substRep   y+  unsubstRep (x :*: y) = unsubstRep x :*: unsubstRep y++instance SubstRep' f x xs => SubstRep' (M1 i c f) x xs where+  type SubstRep (M1 i c f) x = M1 i c (SubstRep f x)+  substRep   (M1 x) = M1 (substRep   x)+  unsubstRep (M1 x) = M1 (unsubstRep x)++instance (Ty (SubstAtom c x) xs, Ty c (x ':&&: xs), SubstRep' f x xs)+         => SubstRep' (c :=>: f) x xs where+  type SubstRep (c :=>: f) x = (SubstAtom c x) :=>: (SubstRep f x)+  substRep   (C x) = C (substRep   x)+  unsubstRep (C x) = C (unsubstRep x)++instance (Ty (SubstAtom t x) xs ~ Ty t (x ':&&: xs))+         => SubstRep' (F t) x xs where+  type SubstRep (F t) x = F (SubstAtom t x)+  substRep   (F x) = F x+  unsubstRep (F x) = F x++type family SubstAtom (f :: Atom (t -> k) d) (x :: t) :: Atom k d where+  SubstAtom ('Var 'VZ)     x = 'Kon x+  SubstAtom ('Var ('VS v)) x = 'Var v+  SubstAtom ('Kon t)       x = 'Kon t+  SubstAtom (t1 ':@: t2)   x = (SubstAtom t1 x) ':@: (SubstAtom t2 x)+  SubstAtom (t1 ':&: t2)   x = (SubstAtom t1 x) ':&: (SubstAtom t2 x)  -- CONVERSION BETWEEN GHC.GENERICS AND KIND-GENERICS 

@@ -7,36 +7,75 @@ {-# language GADTs                 #-} {-# language DeriveGeneric         #-} {-# language QuantifiedConstraints #-}+{-# language UndecidableInstances  #-} module Generics.Kind.Examples where  import Data.PolyKinded.Functor import GHC.Generics (Generic)+import GHC.TypeLits import Type.Reflection  import Generics.Kind  -- Obtained from Generic -instance Split (Maybe a) Maybe (a ':&&: 'LoT0) instance GenericK Maybe (a ':&&: 'LoT0) where   type RepK Maybe = U1 :+: F V0+instance GenericK (Maybe a) LoT0 where+  type RepK (Maybe a) = SubstRep (RepK Maybe) a+  fromK = fromRepK+  toK   = toRepK +instance GenericK Either (a ':&&: b ':&&: LoT0) where+  type RepK Either = F V0 :+: F V1+instance GenericK (Either a) (b ':&&: LoT0) where+  type RepK (Either a) = SubstRep (RepK Either) a+  fromK = fromRepK+  toK   = toRepK+instance GenericK (Either a b) LoT0 where+  type RepK (Either a b) = SubstRep (RepK (Either a)) b+  fromK = fromRepK+  toK   = toRepK+ -- From the docs  data Tree a = Branch (Tree a) (Tree a) | Leaf a             deriving Generic -instance Split (Tree a) Tree (a ':&&: 'LoT0) instance GenericK Tree (a ':&&: 'LoT0) where   type RepK Tree = F (Tree :$: V0) :*: F (Tree :$: V0) :+: F V0+instance GenericK (Tree a) LoT0 where+  type RepK (Tree a) = SubstRep (RepK Tree) a+  fromK = fromRepK+  toK   = toRepK +-- Data family++data family HappyFamily t+data instance HappyFamily (Maybe a) = HFM Bool+data instance HappyFamily [a]       = HFL a++instance GenericK HappyFamily (a ':&&: 'LoT0) where+  type RepK HappyFamily = TypeError (Text "Cannot describe this family uniformly")+  fromK = undefined+  toK   = undefined++instance GenericK (HappyFamily (Maybe a)) 'LoT0 where+  type RepK (HappyFamily (Maybe a)) = F (Kon Bool)+  fromK (HFM x) = F   x+  toK   (F   x) = HFM x++instance GenericK (HappyFamily [a]) 'LoT0 where+  type RepK (HappyFamily [a]) = F (Kon a)+  fromK (HFL x) = F   x+  toK   (F   x) = HFL x+ -- Hand-written instance  data WeirdTree a where   WeirdBranch :: WeirdTree a -> WeirdTree a -> WeirdTree a    WeirdLeaf   :: Show a => t -> a -> WeirdTree a -instance Split (WeirdTree a) WeirdTree (a ':&&: 'LoT0) instance GenericK WeirdTree (a ':&&: 'LoT0) where   type RepK WeirdTree     = F (WeirdTree :$: V0) :*: F (WeirdTree :$: V0)@@ -52,16 +91,26 @@  data WeirdTreeR a where   WeirdBranchR :: WeirdTreeR a -> WeirdTreeR a -> WeirdTreeR a -  WeirdLeafR   :: (Show a, Typeable t, Eq t) => t -> a -> WeirdTreeR a+  WeirdLeafR   :: (Show a, Eq t, Typeable t) => t -> a -> WeirdTreeR a -instance Split (WeirdTreeR a) WeirdTreeR (a ':&&: 'LoT0) instance GenericK WeirdTreeR (a ':&&: 'LoT0) where   type RepK WeirdTreeR     = F (WeirdTreeR :$: V0) :*: F (WeirdTreeR :$: V0)-      :+: ERefl ((Show :$: V1) :=>: ((Eq :$: V0) :=>: (F V0 :*: F V1)))+      :+: E (((Show :$: V1) :&: (Eq :$: V0) :&: (Typeable :$: V0)) :=>: (F V0 :*: F V1)) -  fromK (WeirdBranchR l r) = L1 $                 F l :*: F r-  fromK (WeirdLeafR   a x) = R1 $ ERefl $ C $ C $ F a :*: F x+  fromK (WeirdBranchR l r) = L1 $         F l :*: F r+  fromK (WeirdLeafR   a x) = R1 $ E $ C $ F a :*: F x    toK (L1 (F l :*: F r)) = WeirdBranchR l r-  toK (R1 (ERefl (C (C (F a :*: F x))))) = WeirdLeafR a x+  toK (R1 (E (C (F a :*: F x)))) = WeirdLeafR a x++instance GenericK (WeirdTreeR a) 'LoT0 where+  type RepK (WeirdTreeR a)+    = F (Kon (WeirdTreeR a)) :*: F (Kon (WeirdTreeR a))+    :+: E ((Kon (Show a) :&: (Eq :$: V0) :&: (Typeable :$: V0)) :=>: ((F V0 :*: F (Kon a))))++  fromK (WeirdBranchR l r) = L1 $         F l :*: F r+  fromK (WeirdLeafR   a x) = R1 $ E $ C $ F a :*: F x++  toK (L1 (F l :*: F r)) = WeirdBranchR l r+  toK (R1 (E (C (F a :*: F x)))) = WeirdLeafR a x