kind-generics 0.1.0.0 → 0.1.1.0

raw patch · 5 files changed

+60/−6 lines, 5 filesPVP ok

version bump matches the API change (PVP)

API changes (from Hackage documentation)

+ Generics.Kind: [ERefl] :: forall (t :: k) d (f :: LoT (k -> d) -> *) (x :: LoT d). Typeable t => f (t :&&: x) -> ERefl f x

+ Generics.Kind: data ERefl (f :: LoT (k -> d) -> *) (x :: LoT d)

+ Generics.Kind.Derive.Eq: instance forall k1 k2 (f :: Data.PolyKinded.LoT (k1 -> k2) -> *) (tys :: Data.PolyKinded.LoT k2). (forall (t :: k1). (Generics.Kind.Derive.Eq.GEq f (t 'Data.PolyKinded.:&&: tys), Data.Typeable.Internal.Typeable t)) => Generics.Kind.Derive.Eq.GEq (Generics.Kind.E f) tys

+ Generics.Kind.Derive.Eq: instance forall k1 k2 (f :: Data.PolyKinded.LoT (k1 -> k2) -> *) (tys :: Data.PolyKinded.LoT k2). (forall (t :: k1). Generics.Kind.Derive.Eq.GEq f (t 'Data.PolyKinded.:&&: tys)) => Generics.Kind.Derive.Eq.GEq (Generics.Kind.ERefl f) tys

+ Generics.Kind.Derive.Functor: instance forall k (f :: Data.PolyKinded.LoT (* -> k) -> *) (v :: Data.PolyKinded.Functor.Variances) (as :: Data.PolyKinded.LoT k) (bs :: Data.PolyKinded.LoT k). (forall t. Generics.Kind.Derive.Functor.GFunctor f ('Data.PolyKinded.Functor.Co : v) (t 'Data.PolyKinded.:&&: as) (t 'Data.PolyKinded.:&&: bs)) => Generics.Kind.Derive.Functor.GFunctor (Generics.Kind.ERefl f) v as bs

+ Generics.Kind.Examples: [WeirdBranchR] :: WeirdTreeR a -> WeirdTreeR a -> WeirdTreeR a

+ Generics.Kind.Examples: [WeirdLeafR] :: (Show a, Typeable t, Eq t) => t -> a -> WeirdTreeR a

+ Generics.Kind.Examples: data WeirdTreeR a

+ Generics.Kind.Examples: instance Data.PolyKinded.Split (Generics.Kind.Examples.WeirdTreeR a) Generics.Kind.Examples.WeirdTreeR (a 'Data.PolyKinded.:&&: 'Data.PolyKinded.LoT0)

+ Generics.Kind.Examples: instance GHC.Classes.Eq a => GHC.Classes.Eq (Generics.Kind.Examples.WeirdTreeR a)

+ Generics.Kind.Examples: instance Generics.Kind.GenericK Generics.Kind.Examples.WeirdTreeR (a 'Data.PolyKinded.:&&: 'Data.PolyKinded.LoT0)

Files

kind-generics.cabal +1/−1
src/Generics/Kind.hs +14/−1
src/Generics/Kind/Derive/Eq.hs +12/−4
src/Generics/Kind/Derive/Functor.hs +5/−0
src/Generics/Kind/Examples.hs +28/−0

kind-generics.cabal view

@@ -1,6 +1,6 @@ cabal-version:       >=1.10 name:                kind-generics-version:             0.1.0.0+version:             0.1.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:

src/Generics/Kind.hs view

@@ -22,7 +22,7 @@ , module Data.PolyKinded.Atom   -- * Generic representation types , (:+:)(..), (:*:)(..), U1(..), M1(..)-, F(..), (:=>:)(..), E(..)+, F(..), (:=>:)(..), E(..), ERefl(..)   -- * Generic type classes , GenericK(..) , GenericF, fromF, toF@@ -37,6 +37,7 @@ import Data.Kind import GHC.Generics.Extra hiding ((:=>:)) import qualified GHC.Generics.Extra as GG+import Type.Reflection  -- | Fields: used to represent each of the (visible) arguments to a constructor. -- Replaces the 'K1' type from "GHC.Generics". The type of the field is@@ -69,6 +70,18 @@ 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  -- THE TYPE CLASS

src/Generics/Kind/Derive/Eq.hs view

@@ -14,6 +14,7 @@ module Generics.Kind.Derive.Eq where  import Generics.Kind+import Type.Reflection  geq' :: forall t f x. (GenericS t f x, GEq (RepK f) x)      => t -> t -> Bool@@ -42,7 +43,14 @@ instance (Ty c tys => GEq f tys) => GEq (c :=>: f) tys where   geq (C x) (C y) = geq x y -{- We cannot check whether the two existentials have the same type-instance (forall t. GEq f (t :&&: tys)) => GEq (E f) tys where-  geq (E x) (E y) = geq x y--}+instance (forall t. (GEq f (t :&&: tys), Typeable t)) => GEq (E f) tys where+  geq (E (x :: f (t1 :&&: tys))) (E (y :: f (t2 :&&: tys)))+    = case eqTypeRep (typeRep @t1) (typeRep @t2) of+        Nothing    -> False+        Just HRefl -> geq x y++instance (forall t. GEq f (t :&&: tys)) => GEq (ERefl f) tys where+  geq (ERefl (x :: f (t1 :&&: tys))) (ERefl (y :: f (t2 :&&: tys)))+    = case eqTypeRep (typeRep @t1) (typeRep @t2) of+        Nothing    -> False+        Just HRefl -> geq x y

src/Generics/Kind/Derive/Functor.hs view

@@ -58,6 +58,11 @@          => GFunctor (E f) v as bs where   gfmap v (E (x :: f (t ':&&: x))) = E (gfmap ((id :^: v) :: Mappings ('Co ': v) (t ':&&: as) (t ':&&: bs)) x) +instance forall f v as bs.+         (forall (t :: *). GFunctor f ('Co ': v) (t ':&&: as) (t ':&&: bs))+         => GFunctor (ERefl f) v as bs where+  gfmap v (ERefl (x :: f (t ':&&: x))) = ERefl (gfmap ((id :^: v) :: Mappings ('Co ': v) (t ':&&: as) (t ':&&: bs)) x)+ class GFunctorArg (t :: Atom d (*))                   (v :: Variances) (intended :: Variance)                   (as :: LoT d) (bs :: LoT d) where

src/Generics/Kind/Examples.hs view

@@ -6,10 +6,12 @@ {-# language FlexibleInstances     #-} {-# language GADTs                 #-} {-# language DeriveGeneric         #-}+{-# language QuantifiedConstraints #-} module Generics.Kind.Examples where  import Data.PolyKinded.Functor import GHC.Generics (Generic)+import Type.Reflection  import Generics.Kind import Generics.Kind.Derive.Eq@@ -62,3 +64,29 @@  instance Show b => KFunctor WeirdTree '[ 'Co ] (a ':&&: 'LoT0) (b ':&&: 'LoT0) where   kfmap = kfmapDefault++-- Hand-written instance with reflection++data WeirdTreeR a where+  WeirdBranchR :: WeirdTreeR a -> WeirdTreeR a -> WeirdTreeR a +  WeirdLeafR   :: (Show a, Typeable t, Eq 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)))++  fromK (WeirdBranchR l r) = L1 $                 F l :*: F r+  fromK (WeirdLeafR   a x) = R1 $ ERefl $ C $ 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++instance (Eq a) => Eq (WeirdTreeR a) where+  (==) = geq'++{-+instance Show b => KFunctor WeirdTreeR '[ 'Co ] (a ':&&: 'LoT0) (b ':&&: 'LoT0) where+  kfmap = kfmapDefault+-}