kind-generics 0.4.1.0 → 0.4.1.1

raw patch · 3 files changed

+63/−66 lines, 3 filesPVP: major bump suggested

API removals or changes: PVP suggests a major version bump

API changes (from Hackage documentation)

- Generics.Kind.Examples: data Ranky

+ Generics.Kind: class SubstRep' (f :: LoT (t -> k) -> *) (x :: t) (xs :: LoT k)

+ Generics.Kind.Examples: newtype Ranky

- Generics.Kind: type GenericF t f x = (GenericK f, x ~ (SplitF t f), t ~ (f :@@: x))

+ Generics.Kind: type GenericF t f x = (GenericK f, x ~ SplitF t f, t ~ (f :@@: x))

- Generics.Kind: type GenericN n t f x = (GenericK f, 'TyEnv f x ~ (SplitN n t), t ~ (f :@@: x))

+ Generics.Kind: type GenericN n t f x = (GenericK f, 'TyEnv f x ~ SplitN n t, t ~ (f :@@: x))

- Generics.Kind: type family SubstRep f x :: LoT k -> *

+ Generics.Kind: type family SubstAtom (f :: Atom (t -> k) d) (x :: t) :: Atom k d

Files

kind-generics.cabal +1/−1
src/Generics/Kind.hs +25/−26
src/Generics/Kind/Examples.hs +37/−39

kind-generics.cabal view

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

src/Generics/Kind.hs view

@@ -1,21 +1,20 @@-{-# language DataKinds                 #-}-{-# language KindSignatures            #-}-{-# language PolyKinds                 #-}-{-# language TypeFamilies              #-}-{-# language GADTs                     #-}+{-# language AllowAmbiguousTypes       #-} {-# language ConstraintKinds           #-}-{-# language TypeOperators             #-}-{-# language StandaloneDeriving        #-}+{-# language DataKinds                 #-}+{-# language DefaultSignatures         #-}+{-# language ExistentialQuantification #-} {-# language FlexibleContexts          #-}-{-# language UndecidableInstances      #-}-{-# language MultiParamTypeClasses     #-} {-# language FlexibleInstances         #-}-{-# language ExistentialQuantification #-}-{-# language DefaultSignatures         #-}+{-# language GADTs                     #-}+{-# language MultiParamTypeClasses     #-}+{-# language PolyKinds                 #-}+{-# language QuantifiedConstraints     #-} {-# language ScopedTypeVariables       #-}+{-# language StandaloneDeriving        #-} {-# language TypeApplications          #-}-{-# language AllowAmbiguousTypes       #-}-{-# language QuantifiedConstraints     #-}+{-# language TypeFamilies              #-}+{-# language TypeOperators             #-}+{-# language UndecidableInstances      #-} -- | Main module of @kind-generics@. Please refer to the @README@ file for documentation on how to use this package. module Generics.Kind (   module Data.PolyKinded@@ -28,16 +27,16 @@ , GenericF, fromF, toF , GenericN, fromN, toN   -- * Getting more instances almost for free-, fromRepK, toRepK, SubstRep+, fromRepK, toRepK, SubstRep, SubstRep', SubstAtom   -- * Bridging with "GHC.Generics" , Conv(..) ) where -import Data.PolyKinded-import Data.PolyKinded.Atom-import Data.Kind-import GHC.Generics.Extra hiding ((:=>:), SuchThat)-import qualified GHC.Generics.Extra as GG+import           Data.Kind+import           Data.PolyKinded+import           Data.PolyKinded.Atom+import           GHC.Generics.Extra   hiding (SuchThat, (:=>:))+import qualified GHC.Generics.Extra   as GG -- import GHC.Exts  -- | Fields: used to represent each of the (visible) arguments to a constructor.@@ -105,13 +104,13 @@         => RepK f x -> f :@@: x   toK = to . toGhcGenerics -type GenericF t f x = (GenericK f, x ~ (SplitF t f), t ~ (f :@@: x))+type GenericF t f x = (GenericK f, x ~ SplitF t f, t ~ (f :@@: x)) fromF :: forall f t x. GenericF t f x => t -> RepK f x fromF = fromK @_ @f toF :: forall f t x. GenericF t f x => RepK f x -> t toF = toK @_ @f -type GenericN n t f x = (GenericK f, 'TyEnv f x ~ (SplitN n t), t ~ (f :@@: x))+type GenericN n t f x = (GenericK f, 'TyEnv f x ~ SplitN n t, t ~ (f :@@: x)) fromN :: forall n t f x. GenericN n t f x => t -> RepK f x fromN = fromK @_ @f toN :: forall n t f x. GenericN n t f x => RepK f x -> t@@ -138,14 +137,14 @@   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)+  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)+  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 @@ -156,7 +155,7 @@  instance (Interpret (SubstAtom c x) xs, Interpret c (x ':&&: xs), SubstRep' f x xs)          => SubstRep' (c :=>: f) x xs where-  type SubstRep (c :=>: f) x = (SubstAtom c x) :=>: (SubstRep f x)+  type SubstRep (c :=>: f) x = SubstAtom c x :=>: SubstRep f x   substRep   (SuchThat x) = SuchThat (substRep   x)   unsubstRep (SuchThat x) = SuchThat (unsubstRep x) @@ -170,8 +169,8 @@   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)+  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

src/Generics/Kind/Examples.hs view

@@ -1,25 +1,23 @@ {-# OPTIONS_GHC -fno-warn-orphans  #-}-{-# language TypeOperators         #-}-{-# language TypeFamilies          #-} {-# language DataKinds             #-}-{-# language PolyKinds             #-}-{-# language MultiParamTypeClasses #-}+{-# language DeriveGeneric         #-} {-# language FlexibleInstances     #-} {-# language GADTs                 #-}-{-# language DeriveGeneric         #-}+{-# language MultiParamTypeClasses #-}+{-# language PolyKinds             #-} {-# language QuantifiedConstraints #-}-{-# language UndecidableInstances  #-} {-# language RankNTypes            #-}+{-# language TypeFamilies          #-}+{-# language TypeOperators         #-} {-# language UnboxedTuples         #-}+{-# language UndecidableInstances  #-} module Generics.Kind.Examples where -import Data.PolyKinded.Functor-import GHC.Generics (Generic)-import GHC.TypeLits-import Type.Reflection (Typeable)-import Data.Proxy+import           GHC.Generics    (Generic)+import           GHC.TypeLits+import           Type.Reflection (Typeable) -import Generics.Kind+import           Generics.Kind  -- Obtained from Generic @@ -67,17 +65,17 @@ data instance HappyFamily [a]       = HFL a  instance GenericK HappyFamily where-  type RepK HappyFamily = TypeError (Text "Cannot describe this family uniformly")+  type RepK HappyFamily = TypeError ('Text "Cannot describe this family uniformly")   fromK = undefined   toK   = undefined  instance GenericK (HappyFamily (Maybe a)) where-  type RepK (HappyFamily (Maybe a)) = Field (Kon Bool)+  type RepK (HappyFamily (Maybe a)) = Field ('Kon Bool)   fromK (HFM   x) = Field x   toK   (Field x) = HFM   x  instance GenericK (HappyFamily [a]) where-  type RepK (HappyFamily [a]) = Field (Kon a)+  type RepK (HappyFamily [a]) = Field ('Kon a)   fromK (HFL   x) = Field x   toK   (Field x) = HFL   x @@ -90,22 +88,22 @@   type RepK SimpleIndex     = Exists (*) ((Var1 :~: ([] :$: Var0)) :=>: Field ([] :$: Var0))   fromK (MkSimpleIndex x) = Exists (SuchThat (Field x))-  toK (Exists (SuchThat (Field x))) = (MkSimpleIndex x)+  toK (Exists (SuchThat (Field x))) = MkSimpleIndex x  instance GenericK (SimpleIndex a) where   type RepK (SimpleIndex a)-    = Exists (*) ((Kon a :~: ([] :$: Var0)) :=>: Field ([] :$: Var0))+    = Exists (*) (('Kon a :~: ([] :$: Var0)) :=>: Field ([] :$: Var0))   fromK (MkSimpleIndex x) = Exists (SuchThat (Field x))-  toK (Exists (SuchThat (Field x))) = (MkSimpleIndex x)+  toK (Exists (SuchThat (Field x))) = MkSimpleIndex x  instance GenericK (SimpleIndex a b) where   type RepK (SimpleIndex a b)-    = Exists (*) ((Kon a :~: ([] :$: Var0)) :=>: Field ([] :$: Var0))+    = Exists (*) (('Kon a :~: ([] :$: Var0)) :=>: Field ([] :$: Var0))   fromK (MkSimpleIndex x) = Exists (SuchThat (Field x))-  toK (Exists (SuchThat (Field x))) = (MkSimpleIndex x)+  toK (Exists (SuchThat (Field x))) = MkSimpleIndex x  data WeirdTree a where-  WeirdBranch :: WeirdTree a -> WeirdTree a -> WeirdTree a +  WeirdBranch :: WeirdTree a -> WeirdTree a -> WeirdTree a   WeirdLeaf   :: Show a => t -> a -> WeirdTree a  instance GenericK WeirdTree where@@ -116,37 +114,37 @@   fromK (WeirdBranch l r) = L1 $                     Field l :*: Field r   fromK (WeirdLeaf   a x) = R1 $ Exists $ SuchThat $ Field a :*: Field x -  toK (L1 (Field l :*: Field r)) = WeirdBranch l r+  toK (L1 (Field l :*: Field r))                     = WeirdBranch l r   toK (R1 (Exists (SuchThat (Field a :*: Field x)))) = WeirdLeaf a x  -- Hand-written instance with reflection  data WeirdTreeR a where-  WeirdBranchR :: WeirdTreeR a -> WeirdTreeR a -> WeirdTreeR a +  WeirdBranchR :: WeirdTreeR a -> WeirdTreeR a -> WeirdTreeR a   WeirdLeafR   :: (Show a, Eq t, Typeable t) => t -> a -> WeirdTreeR a  instance GenericK WeirdTreeR where   type RepK WeirdTreeR     = Field (WeirdTreeR :$: Var0) :*: Field (WeirdTreeR :$: Var0)-      :+: Exists (*) (((Show :$: Var1) :&: (Eq :$: Var0) :&: (Typeable :$: Var0))+      :+: Exists (*) (((Show :$: Var1) ':&: (Eq :$: Var0) ':&: (Typeable :$: Var0))                       :=>: (Field Var0 :*: Field Var1))    fromK (WeirdBranchR l r) = L1 $                     Field l :*: Field r   fromK (WeirdLeafR   a x) = R1 $ Exists $ SuchThat $ Field a :*: Field x -  toK (L1 (Field l :*: Field r)) = WeirdBranchR l r+  toK (L1 (Field l :*: Field r))                     = WeirdBranchR l r   toK (R1 (Exists (SuchThat (Field a :*: Field x)))) = WeirdLeafR a x  instance GenericK (WeirdTreeR a) where   type RepK (WeirdTreeR a)-    = Field (Kon (WeirdTreeR a)) :*: Field (Kon (WeirdTreeR a))-    :+: Exists (*) ((Kon (Show a) :&: (Eq :$: Var0) :&: (Typeable :$: Var0))-                    :=>: ((Field Var0 :*: Field (Kon a))))+    = Field ('Kon (WeirdTreeR a)) :*: Field ('Kon (WeirdTreeR a))+    :+: Exists (*) (('Kon (Show a) ':&: (Eq :$: Var0) ':&: (Typeable :$: Var0))+                    :=>: (Field Var0 :*: Field ('Kon a)))    fromK (WeirdBranchR l r) = L1 $                     Field l :*: Field r   fromK (WeirdLeafR   a x) = R1 $ Exists $ SuchThat $ Field a :*: Field x -  toK (L1 (Field l :*: Field r)) = WeirdBranchR l r+  toK (L1 (Field l :*: Field r))                     = WeirdBranchR l r   toK (R1 (Exists (SuchThat (Field a :*: Field x)))) = WeirdLeafR a x  -- From https://gitlab.com/trupill/kind-generics/issues/3@@ -157,8 +155,8 @@  instance GenericK (TTY m a) where   type RepK (TTY m a)-    =     ((Kon a :~: Kon ()) :=>: Field (Kon String))-      :+: ((Kon a :~: Kon String) :=>: U1)+    =     (('Kon a :~: 'Kon ()) :=>: Field ('Kon String))+      :+: (('Kon a :~: 'Kon String) :=>: U1)    fromK (WriteTTY s) = L1 (SuchThat (Field s))   fromK ReadTTY      = R1 (SuchThat U1)@@ -173,12 +171,12 @@  {- GHC rewrites this to the following Core data T (a :: k) =-  forall (a' :: Type). (k ~ Type, a ~~ a') => MkT (Maybe a') +  forall (a' :: Type). (k ~ Type, a ~~ a') => MkT (Maybe a') -}  instance GenericK (T :: k -> *) where   type RepK (T :: k -> *) =-    Exists (*) ((Kon (k ~ (*)) :&: (Var0 :~~: Var1)) :=>: Field (Maybe :$: Var0))+    Exists (*) (('Kon (k ~ (*)) ':&: (Var0 :~~: Var1)) :=>: Field (Maybe :$: Var0))   fromK (MkT x) = Exists (SuchThat (Field x))   toK (Exists (SuchThat (Field x))) = MkT x @@ -199,28 +197,28 @@   P' :: forall k (a :: k). P' k a  instance GenericK (P' j :: k -> *) where-  type RepK (P' j :: k -> *) = (Kon k :~: Kon j) :=>: U1+  type RepK (P' j :: k -> *) = ('Kon k :~: 'Kon j) :=>: U1   fromK P' = SuchThat U1   toK (SuchThat U1) = P'  instance GenericK (P' :: * -> k -> *) where-  type RepK (P' :: * -> k -> *) = (Kon k :~: Var0) :=>: U1+  type RepK (P' :: * -> k -> *) = ('Kon k :~: Var0) :=>: U1   fromK P' = SuchThat U1   toK (SuchThat U1) = P'  -- Rank-N types -data Ranky = MkRanky (forall a. a -> a)+newtype Ranky = MkRanky (forall a. a -> a)  instance GenericK Ranky where-  type RepK Ranky = Field (ForAll ((->) :$: Var0 :@: Var0))+  type RepK Ranky = Field ('ForAll ((->) :$: Var0 ':@: Var0))   fromK (MkRanky x) = Field (ForAllI x)   toK (Field (ForAllI x)) = MkRanky x  newtype Ranky2 b = MkRanky2 ((forall a. a -> a) -> b)  instance GenericK Ranky2 where-  type RepK Ranky2 = Field ((->) :$: ForAll ((->) :$: Var0 :@: Var0) :@: Var0)+  type RepK Ranky2 = Field ((->) :$: 'ForAll ((->) :$: Var0 ':@: Var0) ':@: Var0)   fromK (MkRanky2 f) = Field (\(ForAllI x) -> f x)   toK (Field f) = MkRanky2 (\x -> f (ForAllI x)) @@ -228,7 +226,7 @@   MkShower :: (Show a => a -> String) -> Shower a  instance GenericK Shower where-  type RepK Shower = Field ((Show :$: Var0) :=>>: ((->) :$: Var0 :@: Kon String))+  type RepK Shower = Field ((Show :$: Var0) ':=>>: ((->) :$: Var0 ':@: 'Kon String))   fromK (MkShower f) = Field (SuchThatI f)   toK (Field (SuchThatI f)) = MkShower f