kind-generics-deriving (empty) → 0.3.0.0
raw patch · 11 files changed
+809/−0 lines, 11 filesdep +aesondep +basedep +first-class-familiessetup-changed
Dependencies added: aeson, base, first-class-families, kind-apply, kind-generics
Files
- LICENSE +30/−0
- Setup.hs +2/−0
- kind-generics-deriving.cabal +37/−0
- src/Generics/Kind/Derive/Eq.hs +58/−0
- src/Generics/Kind/Derive/EqTwoParams.hs +57/−0
- src/Generics/Kind/Derive/Examples.hs +75/−0
- src/Generics/Kind/Derive/FunctorOne.hs +101/−0
- src/Generics/Kind/Derive/FunctorPosition.hs +130/−0
- src/Generics/Kind/Derive/Json.hs +105/−0
- src/Generics/Kind/Derive/KFunctor.hs +115/−0
- src/Generics/Kind/Derive/Traversable.hs +99/−0
+ LICENSE view
@@ -0,0 +1,30 @@+Copyright (c) 2018, Alejandro Serrano++All rights reserved.++Redistribution and use in source and binary forms, with or without+modification, are permitted provided that the following conditions are met:++ * Redistributions of source code must retain the above copyright+ notice, this list of conditions and the following disclaimer.++ * Redistributions in binary form must reproduce the above+ copyright notice, this list of conditions and the following+ disclaimer in the documentation and/or other materials provided+ with the distribution.++ * Neither the name of Alejandro Serrano nor the names of other+ contributors may be used to endorse or promote products derived+ from this software without specific prior written permission.++THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS+"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT+LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR+A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT+OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,+SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT+LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,+DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY+THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT+(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE+OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+ Setup.hs view
@@ -0,0 +1,2 @@+import Distribution.Simple+main = defaultMain
+ kind-generics-deriving.cabal view
@@ -0,0 +1,37 @@+cabal-version: >=1.10+name: kind-generics-deriving+version: 0.3.0.0+synopsis: Generic programming in GHC style for arbitrary kinds and GADTs.+description: This package provides automatic derivation for a wide range of classes using `kind-generics`.+-- bug-reports:+license: BSD3+license-file: LICENSE+author: Alejandro Serrano+maintainer: trupill@gmail.com+-- copyright:+category: Data+build-type: Simple++source-repository head+ type: git+ location: https://gitlab.com/trupill/kind-generics.git++library+ exposed-modules: Generics.Kind.Derive.Eq,+ Generics.Kind.Derive.EqTwoParams,+ Generics.Kind.Derive.FunctorPosition,+ Generics.Kind.Derive.FunctorOne,+ Generics.Kind.Derive.Traversable,+ Generics.Kind.Derive.KFunctor,+ Generics.Kind.Derive.Json,+ Generics.Kind.Derive.Examples+ -- other-modules:+ -- other-extensions:+ build-depends: base >= 4.12 && < 5+ , kind-apply+ , kind-generics >= 0.5+ , first-class-families >= 0.8 && < 0.9+ , aeson+ hs-source-dirs: src+ default-language: Haskell2010+ ghc-options: -Wall -fprint-explicit-kinds
+ src/Generics/Kind/Derive/Eq.hs view
@@ -0,0 +1,58 @@+{-# language AllowAmbiguousTypes #-}+{-# language ConstraintKinds #-}+{-# language DataKinds #-}+{-# language FlexibleContexts #-}+{-# language FlexibleInstances #-}+{-# language MultiParamTypeClasses #-}+{-# language PolyKinds #-}+{-# language QuantifiedConstraints #-}+{-# language ScopedTypeVariables #-}+{-# language TypeApplications #-}+{-# language TypeFamilies #-}+{-# language TypeOperators #-}+{-# language UndecidableInstances #-}+module Generics.Kind.Derive.Eq where++import Data.Kind+import GHC.TypeLits+import Generics.Kind++geq' :: forall t. (GenericK t, GEq (RepK t), ReqsEq (RepK t) 'LoT0)+ => t -> t -> Bool+geq' x y = geq (fromK @_ @t @'LoT0 x) (fromK @_ @t @'LoT0 y)++class GEq (f :: LoT k -> Type) where+ type family ReqsEq f (tys :: LoT k) :: Constraint+ geq :: ReqsEq f tys => f tys -> f tys -> Bool++instance GEq U1 where+ type ReqsEq U1 tys = ()+ geq U1 U1 = True++instance GEq f => GEq (M1 i c f) where+ type ReqsEq (M1 i c f) tys = ReqsEq f tys+ geq (M1 x) (M1 y) = geq x y++instance (GEq f, GEq g) => GEq (f :+: g) where+ type ReqsEq (f :+: g) tys = (ReqsEq f tys, ReqsEq g tys)+ geq (L1 x) (L1 y) = geq x y+ geq (R1 x) (R1 y) = geq x y+ geq _ _ = False++instance (GEq f, GEq g) => GEq (f :*: g) where+ type ReqsEq (f :*: g) tys = (ReqsEq f tys, ReqsEq g tys)+ geq (x1 :*: x2) (y1 :*: y2) = geq x1 y1 && geq x2 y2++instance GEq (Field t) where+ type ReqsEq (Field t) tys = Eq (Interpret t tys)+ geq (Field x) (Field y) = x == y++instance GEq f => GEq (c :=>: f) where+ type ReqsEq (c :=>: f) tys = ReqsEq f tys+ -- really we want = Interpret c tys => GEq f tys+ geq (SuchThat x) (SuchThat y) = geq x y++instance TypeError ('Text "Existentials are not supported")+ => GEq (Exists k f) where+ type ReqsEq (Exists k f) tys = TypeError ('Text "Existentials are not supported")+ geq = undefined
+ src/Generics/Kind/Derive/EqTwoParams.hs view
@@ -0,0 +1,57 @@+{-# language AllowAmbiguousTypes #-}+{-# language DataKinds #-}+{-# language FlexibleContexts #-}+{-# language FlexibleInstances #-}+{-# language MultiParamTypeClasses #-}+{-# language PolyKinds #-}+{-# language QuantifiedConstraints #-}+{-# language ScopedTypeVariables #-}+{-# language TypeApplications #-}+{-# language TypeFamilies #-}+{-# language TypeOperators #-}+{-# language UndecidableInstances #-}+module Generics.Kind.Derive.EqTwoParams where++import Data.Kind+import Generics.Kind++geq2' :: forall t. (GenericK t, GEq2 (RepK t) 'LoT0 'LoT0)+ => t -> t -> Bool+geq2' x y = geq2 (fromK @_ @t @'LoT0 x) (fromK @_ @t @'LoT0 y)++class GEq2 (f :: LoT k -> Type) (xs :: LoT k) (ys :: LoT k) where+ geq2 :: f xs -> f ys -> Bool++instance GEq2 U1 xs ys where+ geq2 U1 U1 = True++instance (GEq2 f xs ys) => GEq2 (M1 i c f) xs ys where+ geq2 (M1 x) (M1 y) = geq2 x y++instance (GEq2 f xs ys, GEq2 g xs ys) => GEq2 (f :+: g) xs ys where+ geq2 (L1 x) (L1 y) = geq2 x y+ geq2 (R1 x) (R1 y) = geq2 x y+ geq2 _ _ = False++instance (GEq2 f xs ys, GEq2 g xs ys) => GEq2 (f :*: g) xs ys where+ geq2 (x1 :*: x2) (y1 :*: y2) = geq2 x1 y1 && geq2 x2 y2++instance (Interpret t xs ~ Interpret t ys, Eq (Interpret t xs)) => GEq2 (Field t) xs ys where+ geq2 (Field x) (Field y) = x == y++instance ((Interpret c xs, Interpret c ys) => GEq2 f xs ys)+ => GEq2 (c :=>: f) xs ys where+ geq2 (SuchThat x) (SuchThat y) = geq2 x y++instance (forall x y. GEq2 f (x ':&&: xs) (y ':&&: ys))+ => GEq2 (Exists k f) xs ys where+ geq2 (Exists x) (Exists y) = geq2 x y++{-+instance (forall x y. GEq2 f (x ':&&: xs) (y ':&&: ys))+ => GEq2 (ERefl f) xs ys where+ geq2 (ERefl (x :: f (x :&&: xs))) (ERefl (y :: f (y :&&: ys)))+ = case eqTypeRep (typeRep @x) (typeRep @y) of+ Nothing -> False+ Just HRefl -> geq2 x y+-}
+ src/Generics/Kind/Derive/Examples.hs view
@@ -0,0 +1,75 @@+{-# OPTIONS_GHC -fno-warn-orphans #-}+{-# language DataKinds #-}+{-# language FlexibleInstances #-}+{-# language MultiParamTypeClasses #-}+{-# language ScopedTypeVariables #-}+{-# language TypeOperators #-}+module Generics.Kind.Derive.Examples where++import Data.Aeson (FromJSON (..), ToJSON (..))+import Data.PolyKinded.Functor+import Data.Traversable (foldMapDefault)++import Generics.Kind+import Generics.Kind.Derive.Eq+import Generics.Kind.Derive.FunctorOne+import Generics.Kind.Derive.FunctorPosition+import Generics.Kind.Derive.Json+import Generics.Kind.Derive.KFunctor+import Generics.Kind.Derive.Traversable+import Generics.Kind.Examples++-- Maybe+instance KFunctor Maybe '[ 'Co ] (a ':&&: 'LoT0) (b ':&&: 'LoT0) where+ kfmap = kfmapDefault++-- Tree+instance Eq a => Eq (Tree a) where+ (==) = geq'+instance ToJSON a => ToJSON (Tree a) where+ toJSON = gtoJSON'+instance FromJSON a => FromJSON (Tree a) where+ parseJSON = gfromJSON'+instance KFunctor Tree '[ 'Co ] (a ':&&: 'LoT0) (b ':&&: 'LoT0) where+ kfmap = kfmapDefault+instance Functor Tree where+ -- fmap = fmapDefault+ fmap = fmapDefaultOne+instance Foldable Tree where+ foldMap = foldMapDefault+instance Traversable Tree where+ traverse = traverseDefault++-- TTY (from https://gitlab.com/trupill/kind-generics/issues/3)+instance Eq (TTY m a) where+ (==) = geq'+instance ToJSON (TTY m a) where+ toJSON = gtoJSON'+{-+instance FromJSON (TTY m a) where+ parseJSON = gfromJSON'++Fails with:+• Couldn't match type ‘a’ with ‘()’ arising from a use of ‘gfromJSON'’+-}++fmapEither :: (a -> b) -> Either e a -> Either e b+fmapEither = fmapDefault'++-- WeirdTree+instance Show b => KFunctor WeirdTree '[ 'Co ] (a ':&&: 'LoT0) (b ':&&: 'LoT0) where+ kfmap = kfmapDefault++-- WeirdTree with reflected existentials+-- instance (Eq a) => Eq (WeirdTreeR a) where+ -- (==) = geq'++instance Functor (SimpleIndex a) where+ fmap = fmapDefault+instance Foldable (SimpleIndex a) where+ foldMap = foldMapDefault+instance Traversable (SimpleIndex a) where+ traverse = traverseDefault++instance EFunctor f => Functor (Hkd f) where+ fmap = fmapDefaultOne
+ src/Generics/Kind/Derive/FunctorOne.hs view
@@ -0,0 +1,101 @@+{-# language AllowAmbiguousTypes #-}+{-# language ConstraintKinds #-}+{-# language DataKinds #-}+{-# language FlexibleContexts #-}+{-# language FlexibleInstances #-}+{-# language MultiParamTypeClasses #-}+{-# language PolyKinds #-}+{-# language QuantifiedConstraints #-}+{-# language ScopedTypeVariables #-}+{-# language TemplateHaskell #-}+{-# language TypeApplications #-}+{-# language TypeFamilies #-}+{-# language TypeOperators #-}+{-# language UndecidableInstances #-}+module Generics.Kind.Derive.FunctorOne where++import Data.Kind+import Data.Proxy+import Generics.Kind+import qualified Fcf.Core as Fcf+import Fcf.Combinators (Pure, Pure1, type (<=<))++fmapDefaultOne :: (GenericK f,+ GenericK f,+ GFunctorOne (RepK f),+ Reqs (RepK f) a b)+ => (a -> b) -> f a -> f b+fmapDefaultOne f = toK . gfmapo f . fromK++class GFunctorOne (f :: LoT (Type -> Type) -> Type) where+ type family Reqs f a b :: Constraint+ gfmapo :: Reqs f a b => (a -> b) -> f (LoT1 a) -> f (LoT1 b)++gfmapo' :: forall a b f. (GFunctorOne f, Reqs f a b)+ => (a -> b) -> f (LoT1 a) -> f (LoT1 b)+gfmapo' = gfmapo+++instance GFunctorOne U1 where+ type Reqs U1 a b = ()+ gfmapo _ U1 = U1++instance GFunctorOne f => GFunctorOne (M1 i c f) where+ type Reqs (M1 i c f) a b = Reqs f a b+ gfmapo v (M1 x) = M1 (gfmapo v x)++instance (GFunctorOne f, GFunctorOne g)+ => GFunctorOne (f :+: g) where+ type Reqs (f :+: g) a b = (Reqs f a b, Reqs g a b)+ gfmapo v (L1 x) = L1 (gfmapo v x)+ gfmapo v (R1 x) = R1 (gfmapo v x)++instance (GFunctorOne f, GFunctorOne g)+ => GFunctorOne (f :*: g) where+ type Reqs (f :*: g) a b = (Reqs f a b, Reqs g a b)+ gfmapo v (x :*: y) = gfmapo v x :*: gfmapo v y++instance GFunctorOne f => GFunctorOne (c :=>: f) where+ type Reqs (c :=>: f) a b = (Interpret c (LoT1 b), Reqs f a b)+ -- actually you want = Interpret c (LoT1 a) => (Interpret c (LoT1 b), Reqs f a b)+ gfmapo v (SuchThat x) = SuchThat (gfmapo v x)++class GFunctorOneArg (t :: Atom (Type -> Type) Type) where+ gfmapof :: Proxy t -> (a -> b)+ -> Interpret t (LoT1 a) -> Interpret t (LoT1 b)++instance GFunctorOneArg t => GFunctorOne (Field t) where+ type Reqs (Field t) a b = (() :: Constraint)+ gfmapo v (Field x) = Field (gfmapof (Proxy @t) v x)++-- A constant+instance GFunctorOneArg ('Kon t) where+ gfmapof _ _ x = x+-- The type variable itself+instance GFunctorOneArg Var0 where+ gfmapof _ f x = f x+-- Going through functor+instance forall f x.+ (Functor f, GFunctorOneArg x)+ => GFunctorOneArg (f :$: x) where+ gfmapof _ f x = fmap (gfmapof (Proxy @x) f) x++-- Support for Hkd, defunctionalized variant, simplfiied GenericK instance.+instance EFunctor f => GFunctorOneArg (Eval (Kon f :@: Var0)) where+ gfmapof _ f x = emap @f f x++-- Unary first-class family as a functor.+class EFunctor (f :: Type -> Fcf.Exp Type) where+ emap :: (a -> b) -> Fcf.Eval (f a) -> Fcf.Eval (f b)++-- The functor "x" (identity functor).+instance EFunctor Pure where+ emap = id++-- The functor "f x", for any Functor f+instance Functor f => EFunctor (Pure1 f) where+ emap = fmap++-- Composition of functors+instance (EFunctor t, EFunctor u) => EFunctor (t <=< u) where+ emap = emap @t . emap @u
+ src/Generics/Kind/Derive/FunctorPosition.hs view
@@ -0,0 +1,130 @@+{-# language AllowAmbiguousTypes #-}+{-# language DataKinds #-}+{-# language FlexibleContexts #-}+{-# language FlexibleInstances #-}+{-# language MultiParamTypeClasses #-}+{-# language PolyKinds #-}+{-# language QuantifiedConstraints #-}+{-# language ScopedTypeVariables #-}+{-# language TypeApplications #-}+{-# language TypeFamilies #-}+{-# language TypeOperators #-}+{-# language UndecidableInstances #-}+module Generics.Kind.Derive.FunctorPosition where++import Data.Kind+import GHC.TypeLits+import Generics.Kind++fmapDefaultPos :: forall v f as bs.+ (GenericK f, GenericK f,+ GFunctorPos (RepK f) v as bs)+ => (Interpret ('Var v) as -> Interpret ('Var v) bs)+ -> f :@@: as -> f :@@: bs+fmapDefaultPos f = toK @_ @f @bs . gfmapp @_ @(RepK f) @v @as @bs f . fromK @_ @f @as++fmapDefault :: forall f a b. (GenericK f, GenericK f,+ GFunctorPos (RepK f) 'VZ (LoT1 a) (LoT1 b))+ => (a -> b) -> f a -> f b+fmapDefault = fmapDefaultPos @'VZ @f @(LoT1 a) @(LoT1 b)++bimapDefault :: forall f a c b d.+ (GenericK f, GenericK f, GenericK f,+ GFunctorPos (RepK f) 'VZ (LoT2 a d) (LoT2 c d),+ GFunctorPos (RepK f) ('VS 'VZ) (LoT2 a b) (LoT2 a d))+ => (a -> c) -> (b -> d) -> f a b -> f c d+bimapDefault f g = fmapDefaultPos @'VZ @f @(LoT2 a d) @(LoT2 c d) f+ . fmapDefaultPos @('VS 'VZ) @f @(LoT2 a b) @(LoT2 a d) g++class GFunctorPos (f :: LoT k -> Type) (v :: TyVar k Type)+ (as :: LoT k) (bs :: LoT k) where+ gfmapp :: (Interpret ('Var v) as -> Interpret ('Var v) bs)+ -> f as -> f bs++instance GFunctorPos U1 v as bs where+ gfmapp _ U1 = U1++instance forall f v as bs i c. GFunctorPos f v as bs+ => GFunctorPos (M1 i c f) v as bs where+ gfmapp v (M1 x) = M1 (gfmapp @_ @f @v @as @bs v x)++instance forall f g v as bs. (GFunctorPos f v as bs, GFunctorPos g v as bs)+ => GFunctorPos (f :+: g) v as bs where+ gfmapp v (L1 x) = L1 (gfmapp @_ @f @v @as @bs v x)+ gfmapp v (R1 x) = R1 (gfmapp @_ @g @v @as @bs v x)++instance forall f g v as bs. (GFunctorPos f v as bs, GFunctorPos g v as bs)+ => GFunctorPos (f :*: g) v as bs where+ gfmapp v (x :*: y) = gfmapp @_ @f @v @as @bs v x :*: gfmapp @_ @g @v @as @bs v y++instance forall c f v as bs z.+ (Interpret c as => GFunctorPos f v as bs, z ~ Interpret c bs, Interpret c as => z)+ => GFunctorPos (c :=>: f) v as bs where+ gfmapp v (SuchThat x) = SuchThat (gfmapp @_ @f @v @as @bs v x)++instance forall k f v as bs.+ (forall (t :: k). GFunctorPos f ('VS v) (t ':&&: as) (t ':&&: bs))+ => GFunctorPos (Exists k f) v as bs where+ gfmapp v (Exists (x :: f (t ':&&: x)))+ = Exists (gfmapp @_ @f @('VS v) @(t ':&&: x) @(t ':&&: _) v x)++instance forall t v as bs. GFunctorArgPos t v as bs (ContainsTyVar v t)+ => GFunctorPos (Field t) v as bs where+ gfmapp v (Field x) = Field (gfmappf @_ @t @v @as @bs @(ContainsTyVar v t) v x)++class GFunctorArgPos (t :: Atom d Type) (v :: TyVar d Type)+ (as :: LoT d) (bs :: LoT d)+ (p :: Bool) where+ gfmappf :: (Interpret ('Var v) as -> Interpret ('Var v) bs)+ -> Interpret t as -> Interpret t bs++instance (Interpret t as ~ Interpret t bs) => GFunctorArgPos t v as bs 'False where+ gfmappf _ = id++instance TypeError ('Text "Should never get here")+ => GFunctorArgPos ('Kon t) v as bs whatever where+ gfmappf _ = id++instance ( Functor (Interpret f as), Interpret f as ~ Interpret f bs+ , GFunctorArgPos x v as bs (ContainsTyVar v x) )+ => GFunctorArgPos (f ':@: x) v as bs 'True where+ gfmappf f x = fmap (gfmappf @_ @x @v @as @bs @(ContainsTyVar v x) f) x++-- We found the same variable+instance GFunctorArgPos ('Var 'VZ) 'VZ (a ':&&: as) (b ':&&: bs) 'True where+ gfmappf f x = f x+-- We need to keep looking+instance forall d (v :: TyVar d Type) n r as s bs isthere.+ GFunctorArgPos ('Var v) n as bs isthere+ => GFunctorArgPos ('Var ('VS v)) ('VS n) (r ':&&: as) (s ':&&: bs) isthere where+ gfmappf f x = gfmappf @d @('Var v) @n @as @bs @isthere f x+-- If we arrive to another we do not want, keep it as it is+instance TypeError ('Text "Should never get here")+ => GFunctorArgPos ('Var 'VZ) ('VS n) (r ':&&: as) (r ':&&: bs) 'True where+ gfmappf _ = id+instance TypeError ('Text "Should never get here")+ => GFunctorArgPos ('Var ('VS n)) 'VZ (r ':&&: 'LoT0) (r ':&&: 'LoT0) 'True where+ gfmappf _ = id++-- Alternative implementation+{-+type family EqualTyVar (v :: TyVar d Type) (w :: TyVar d Type) :: Bool where+ EqualTyVar v v = True+ EqualTyVar v w = False++class GFunctorVarPos (v :: TyVar d Type) (w :: TyVar d Type)+ (as :: LoT d) (bs :: LoT d)+ (equal :: Bool) where+ gfmappv :: (Interpret (Var w) as -> Interpret (Var w) bs)+ -> Interpret (Var v) as -> Interpret (Var v) bs++instance v ~ w => GFunctorVarPos v w as bs True where+ gfmappv f = f+instance (Interpret (Var v) as ~ Interpret (Var v) bs)+ => GFunctorVarPos v w as bs False where+ gfmappv _ = id++instance forall v w as bs. GFunctorVarPos v w as bs (EqualTyVar v w)+ => GFunctorArgPos (Var v) w as bs True where+ gfmappf = gfmappv @_ @v @w @as @bs @(EqualTyVar v w)+-}
+ src/Generics/Kind/Derive/Json.hs view
@@ -0,0 +1,105 @@+{-# language DataKinds #-}+{-# language FlexibleContexts #-}+{-# language FlexibleInstances #-}+{-# language GADTs #-}+{-# language MultiParamTypeClasses #-}+{-# language PartialTypeSignatures #-}+{-# language PolyKinds #-}+{-# language QuantifiedConstraints #-}+{-# language ScopedTypeVariables #-}+{-# language TypeApplications #-}+{-# language TypeFamilies #-}+{-# language TypeOperators #-}+{-# language UndecidableInstances #-}+module Generics.Kind.Derive.Json where++import Control.Applicative+import Control.Monad+import Data.Aeson+import Data.Aeson.Types+import Data.Kind+import Data.Proxy+import GHC.Generics (Meta (..))+import GHC.TypeLits+import Generics.Kind++gtoJSON' :: forall t. (GenericK t, GToJSONK (RepK t) 'LoT0)+ => t -> Value+gtoJSON' x = gtoJSON (fromK @_ @t @'LoT0 x)++gfromJSON' :: forall t. (GenericK t, GFromJSONK (RepK t) 'LoT0)+ => Value -> Parser t+gfromJSON' v = fmap (toK @_ @t @'LoT0) (gfromJSON v)++class GToJSONK (f :: LoT k -> Type) (x :: LoT k) where+ gtoJSON :: f x -> Value+class GFromJSONK (f :: LoT k -> Type) (x :: LoT k) where+ gfromJSON :: Value -> Parser (f x)++instance ToJSON (Interpret t x)+ => GToJSONK (Field t) x where+ gtoJSON (Field t) = toJSON t+instance FromJSON (Interpret t x)+ => GFromJSONK (Field t) x where+ gfromJSON = fmap Field . parseJSON++instance GToJSONK U1 x where+ gtoJSON U1 = Null+instance GFromJSONK U1 x where+ gfromJSON Null = pure U1+ gfromJSON _ = empty++instance (GToJSONK f x, GToJSONK g x)+ => GToJSONK (f :+: g) x where+ gtoJSON (L1 f) = gtoJSON f+ gtoJSON (R1 g) = gtoJSON g+instance (GFromJSONK f x, GFromJSONK g x)+ => GFromJSONK (f :+: g) x where+ gfromJSON v = (L1 <$> gfromJSON v) <|> (R1 <$> gfromJSON v)++instance (GToJSONK f x, GToJSONK g x)+ => GToJSONK (f :*: g) x where+ gtoJSON (f :*: g) = toJSON (gtoJSON f, gtoJSON g)+instance (GFromJSONK f x, GFromJSONK g x)+ => GFromJSONK (f :*: g) x where+ gfromJSON v = do (f, g) <- parseJSON v+ (:*:) <$> gfromJSON f <*> gfromJSON g++instance forall name f x i fx st.+ (GToJSONK f x, KnownSymbol name)+ => GToJSONK (M1 i ('MetaCons name fx st) f) x where+ gtoJSON (M1 f) = toJSON (symbolVal $ Proxy @name, gtoJSON f)+instance forall name f x i fx st.+ (GFromJSONK f x, KnownSymbol name)+ => GFromJSONK (M1 i ('MetaCons name fx st) f) x where+ gfromJSON v = do (name, f) <- parseJSON v+ guard $ name == symbolVal (Proxy @name)+ M1 <$> gfromJSON f++instance GToJSONK f x+ => GToJSONK (M1 i ('MetaData _1 _2 _3 _4) f) x where+ gtoJSON (M1 f) = gtoJSON f+instance GFromJSONK f x+ => GFromJSONK (M1 i ('MetaData _1 _2 _3 _4) f) x where+ gfromJSON = fmap M1 . gfromJSON++instance GToJSONK f x+ => GToJSONK (M1 i ('MetaSel _1 _2 _3 _4) f) x where+ gtoJSON (M1 f) = gtoJSON f+instance GFromJSONK f x+ => GFromJSONK (M1 i ('MetaSel _1 _2 _3 _4) f) x where+ gfromJSON = fmap M1 . gfromJSON++instance (Interpret c x => GToJSONK f x)+ => GToJSONK (c :=>: f) x where+ gtoJSON (SuchThat f) = gtoJSON f+instance (Interpret c x, GFromJSONK f x)+ => GFromJSONK (c :=>: f) x where+ gfromJSON = fmap SuchThat . gfromJSON++instance (forall t. GToJSONK f (t ':&&: x))+ => GToJSONK (Exists k f) x where+ gtoJSON (Exists x) = gtoJSON x+instance (forall t. GFromJSONK f (t ':&&: x))+ => GFromJSONK (Exists k f) x where+ gfromJSON = fmap Exists . gfromJSON
+ src/Generics/Kind/Derive/KFunctor.hs view
@@ -0,0 +1,115 @@+{-# language AllowAmbiguousTypes #-}+{-# language DataKinds #-}+{-# language FlexibleContexts #-}+{-# language FlexibleInstances #-}+{-# language GADTs #-}+{-# language MultiParamTypeClasses #-}+{-# language PolyKinds #-}+{-# language QuantifiedConstraints #-}+{-# language RankNTypes #-}+{-# language ScopedTypeVariables #-}+{-# language TypeApplications #-}+{-# language TypeFamilies #-}+{-# language TypeOperators #-}+{-# language UndecidableInstances #-}+module Generics.Kind.Derive.KFunctor where++import Data.Kind+import Data.PolyKinded.Functor+import Data.Proxy++import Generics.Kind++kfmapDefault :: forall k (f :: k) v as bs. (GenericK f, GenericK f, GFunctor (RepK f) v as bs)+ => Mappings v as bs -> f :@@: as -> f :@@: bs+kfmapDefault v = toK @k @f @bs . gfmap v . fromK @k @f @as++fmapDefault' :: forall (f :: Type -> Type) a b.+ (GenericK f, GenericK f,+ GFunctor (RepK f) '[ 'Co ] (a ':&&: 'LoT0) (b ':&&: 'LoT0))+ => (a -> b) -> f a -> f b+fmapDefault' f = kfmapDefault (f :^: M0 :: Mappings '[ 'Co ] (a ':&&: 'LoT0) (b ':&&: 'LoT0))++class GFunctor (f :: LoT k -> Type) (v :: Variances) (as :: LoT k) (bs :: LoT k) where+ gfmap :: Mappings v as bs -> f as -> f bs++instance GFunctor U1 v as bs where+ gfmap _ U1 = U1++instance GFunctor f v as bs => GFunctor (M1 i c f) v as bs where+ gfmap v (M1 x) = M1 (gfmap v x)++instance (GFunctor f v as bs, GFunctor g v as bs)+ => GFunctor (f :+: g) v as bs where+ gfmap v (L1 x) = L1 (gfmap v x)+ gfmap v (R1 x) = R1 (gfmap v x)++instance (GFunctor f v as bs, GFunctor g v as bs)+ => GFunctor (f :*: g) v as bs where+ gfmap v (x :*: y) = gfmap v x :*: gfmap v y++instance (Interpret c as => GFunctor f v as bs, {- Ty c as => -} Interpret c bs)+ => GFunctor (c :=>: f) v as bs where+ gfmap v (SuchThat x) = SuchThat (gfmap v x)++instance forall f v as bs.+ (forall (t :: Type). GFunctor f ('Co ': v) (t ':&&: as) (t ':&&: bs))+ => GFunctor (Exists Type f) v as bs where+ gfmap v (Exists (x :: f (t ':&&: x)))+ = Exists (gfmap ((id :^: v) :: Mappings ('Co ': v) (t ':&&: as) (t ':&&: bs)) x)++class GFunctorArg (t :: Atom d Type)+ (v :: Variances) (intended :: Variance)+ (as :: LoT d) (bs :: LoT d) where+ gfmapf :: Proxy t -> Proxy intended+ -> Mappings v as bs+ -> Mapping intended (Interpret t as) (Interpret t bs)++instance forall t v as bs. GFunctorArg t v 'Co as bs+ => GFunctor (Field t) v as bs where+ gfmap v (Field x) = Field (gfmapf (Proxy @t) (Proxy @'Co) v x)++instance GFunctorArg ('Kon t) v 'Co as bs where+ gfmapf _ _ _ = id+instance GFunctorArg ('Kon t) v 'Contra as bs where+ gfmapf _ _ _ = id++instance forall d (f :: Atom (Type -> d) Type) v (as :: LoT d) (bs :: LoT d).+ (forall (t :: Type). GFunctorArg f ('Co ': v) 'Co (t ':&&: as) (t ':&&: bs))+ => GFunctorArg ('ForAll f) v 'Co as bs where+ gfmapf _ _ v x = fromWrappedI $ go $ toWrappedI x+ where+ go :: forall (t :: Type). WrappedI f (t ':&&: as) -> WrappedI f (t ':&&: bs)+ go (WrapI p) = WrapI (gfmapf @(Type -> d) @f @('Co ': v) @'Co @(t ':&&: as) @(t ':&&: bs)+ Proxy Proxy (id :^: v) p)++instance GFunctorArg ('Var 'VZ) (r ': v) r (a ':&&: as) (b ':&&: bs) where+ gfmapf _ _ (f :^: _) = f++instance forall vr pre v intended a as b bs.+ GFunctorArg ('Var vr) v intended as bs+ => GFunctorArg ('Var ('VS vr)) (pre ': v) intended (a ':&&: as) (b ':&&: bs) where+ gfmapf _ _ (_ :^: rest) = gfmapf (Proxy @('Var vr)) (Proxy @intended) rest++instance forall f x v v1 as bs.+ (KFunctor f '[v1] (Interpret x as ':&&: 'LoT0) (Interpret x bs ':&&: 'LoT0),+ GFunctorArg x v v1 as bs)+ => GFunctorArg (f :$: x) v 'Co as bs where+ gfmapf _ _ v = kfmap (gfmapf (Proxy @x) (Proxy @v1) v :^: M0)++instance forall f x y v v1 v2 as bs.+ (KFunctor f '[v1, v2] (Interpret x as ':&&: Interpret y as ':&&: 'LoT0)+ (Interpret x bs ':&&: Interpret y bs ':&&: 'LoT0),+ GFunctorArg x v v1 as bs, GFunctorArg y v v2 as bs)+ => GFunctorArg (f :$: x ':@: y) v 'Co as bs where+ gfmapf _ _ v = kfmap (gfmapf (Proxy @x) (Proxy @v1) v :^:+ gfmapf (Proxy @y) (Proxy @v2) v :^: M0)++instance forall f x y z v v1 v2 v3 as bs.+ (KFunctor f '[v1, v2, v3] (Interpret x as ':&&: Interpret y as ':&&: Interpret z as ':&&: 'LoT0)+ (Interpret x bs ':&&: Interpret y bs ':&&: Interpret z bs ':&&: 'LoT0),+ GFunctorArg x v v1 as bs, GFunctorArg y v v2 as bs, GFunctorArg z v v3 as bs)+ => GFunctorArg (f :$: x ':@: y ':@: z) v 'Co as bs where+ gfmapf _ _ v = kfmap (gfmapf (Proxy @x) (Proxy @v1) v :^:+ gfmapf (Proxy @y) (Proxy @v2) v :^:+ gfmapf (Proxy @z) (Proxy @v3) v :^: M0)
+ src/Generics/Kind/Derive/Traversable.hs view
@@ -0,0 +1,99 @@+{-# language AllowAmbiguousTypes #-}+{-# language DataKinds #-}+{-# language FlexibleContexts #-}+{-# language FlexibleInstances #-}+{-# language MultiParamTypeClasses #-}+{-# language PolyKinds #-}+{-# language QuantifiedConstraints #-}+{-# language ScopedTypeVariables #-}+{-# language TypeApplications #-}+{-# language TypeFamilies #-}+{-# language TypeOperators #-}+{-# language UndecidableInstances #-}+module Generics.Kind.Derive.Traversable where++import Data.Kind+import GHC.TypeLits+import Generics.Kind++traverseDefaultPos :: forall v f as bs g.+ (GenericK f, GenericK f,+ GTraversable (RepK f) v as bs,+ Applicative g)+ => (Interpret ('Var v) as -> g (Interpret ('Var v) bs))+ -> f :@@: as -> g (f :@@: bs)+traverseDefaultPos f = fmap (toK @_ @f @bs) . gtraverse @_ @(RepK f) @v @as @bs f . fromK @_ @f @as++traverseDefault :: forall f a b g. (GenericK f, GenericK f,+ GTraversable (RepK f) 'VZ (LoT1 a) (LoT1 b), Applicative g)+ => (a -> g b) -> f a -> g (f b)+traverseDefault = traverseDefaultPos @'VZ @f @(LoT1 a) @(LoT1 b)++class GTraversable (f :: LoT k -> Type) (v :: TyVar k Type)+ (as :: LoT k) (bs :: LoT k) where+ gtraverse :: Applicative g+ => (Interpret ('Var v) as -> g (Interpret ('Var v) bs))+ -> f as -> g (f bs)++instance GTraversable U1 v as bs where+ gtraverse _ U1 = pure U1++instance forall f v as bs i c. GTraversable f v as bs+ => GTraversable (M1 i c f) v as bs where+ gtraverse v (M1 x) = M1 <$> gtraverse @_ @f @v @as @bs v x++instance forall f g v as bs. (GTraversable f v as bs, GTraversable g v as bs)+ => GTraversable (f :+: g) v as bs where+ gtraverse v (L1 x) = L1 <$> gtraverse @_ @f @v @as @bs v x+ gtraverse v (R1 x) = R1 <$> gtraverse @_ @g @v @as @bs v x++instance forall f g v as bs. (GTraversable f v as bs, GTraversable g v as bs)+ => GTraversable (f :*: g) v as bs where+ gtraverse v (x :*: y) = (:*:) <$> gtraverse @_ @f @v @as @bs v x+ <*> gtraverse @_ @g @v @as @bs v y++instance forall c f v as bs z.+ (Interpret c as => GTraversable f v as bs, z ~ Interpret c bs, Interpret c as => z)+ => GTraversable (c :=>: f) v as bs where+ gtraverse v (SuchThat x) = SuchThat <$> gtraverse @_ @f @v @as @bs v x++instance forall k f v as bs.+ (forall (t :: k). GTraversable f ('VS v) (t ':&&: as) (t ':&&: bs))+ => GTraversable (Exists k f) v as bs where+ gtraverse v (Exists (x :: f (t ':&&: x)))+ = Exists <$> gtraverse @_ @f @('VS v) @(t ':&&: x) @(t ':&&: _) v x++instance forall t v as bs. GTraversableArg t v as bs (ContainsTyVar v t)+ => GTraversable (Field t) v as bs where+ gtraverse v (Field x) = Field <$> gtraversef @_ @t @v @as @bs @(ContainsTyVar v t) v x++class GTraversableArg (t :: Atom d Type) (v :: TyVar d Type)+ (as :: LoT d) (bs :: LoT d) (p :: Bool) where+ gtraversef :: Applicative g+ => (Interpret ('Var v) as -> g (Interpret ('Var v) bs))+ -> Interpret t as -> g (Interpret t bs)++instance (Interpret t as ~ Interpret t bs) => GTraversableArg t v as bs 'False where+ gtraversef _ = pure++instance TypeError ('Text "Should never get here")+ => GTraversableArg ('Kon t) v as bs whatever where+ gtraversef _ = pure++instance ( Traversable (Interpret f as), Interpret f as ~ Interpret f bs+ , GTraversableArg x v as bs (ContainsTyVar v x))+ => GTraversableArg (f ':@: x) v as bs 'True where+ gtraversef f x = traverse (gtraversef @_ @x @v @as @bs @(ContainsTyVar v x) f) x++-- We found the same variable+instance GTraversableArg ('Var 'VZ) 'VZ (a ':&&: as) (b ':&&: bs) 'True where+ gtraversef f x = f x+-- We need to keep looking+instance forall d (v :: TyVar d Type) n r as s bs isthere.+ GTraversableArg ('Var v) n as bs isthere+ => GTraversableArg ('Var ('VS v)) ('VS n) (r ':&&: as) (s ':&&: bs) isthere where+ gtraversef f x = gtraversef @d @('Var v) @n @as @bs @isthere f x+-- If we arrive to another we do not want, keep it as it is+instance TypeError ('Text "Should never get here")+ => GTraversableArg ('Var 'VZ) ('VS n) (r ':&&: as) (r ':&&: bs) 'True where+ gtraversef _ = pure