diff --git a/ChangeLog.md b/ChangeLog.md new file mode 100644 --- /dev/null +++ b/ChangeLog.md @@ -0,0 +1,2 @@ +## generic-lens-core-2.0.0.0 (2020-02-11) +- Initial release diff --git a/LICENSE b/LICENSE new file mode 100644 --- /dev/null +++ b/LICENSE @@ -0,0 +1,30 @@ +Copyright (c) 2020, Csongor Kiss + +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 Csongor Kiss 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. diff --git a/Setup.hs b/Setup.hs new file mode 100644 --- /dev/null +++ b/Setup.hs @@ -0,0 +1,2 @@ +import Distribution.Simple +main = defaultMain diff --git a/generic-lens-core.cabal b/generic-lens-core.cabal new file mode 100644 --- /dev/null +++ b/generic-lens-core.cabal @@ -0,0 +1,70 @@ +name: generic-lens-core +version: 2.0.0.0 +synopsis: Generically derive traversals, lenses and prisms. +description: This library uses GHC.Generics to derive efficient optics (traversals, lenses and prisms) for algebraic data types in a type-directed way, with a focus on good type inference and error messages when possible. + . + This package is the shared internal logic of the + @@ + and + @@ + libraries. + +homepage: https://github.com/kcsongor/generic-lens +license: BSD3 +license-file: LICENSE +author: Csongor Kiss +maintainer: kiss.csongor.kiss@gmail.com +category: Generics, Records, Lens +build-type: Simple +cabal-version: >= 1.10 +Tested-With: GHC == 8.4.1, GHC == 8.4.4, GHC == 8.6.5, GHC == 8.8.1, GHC == 8.10.1 + +extra-source-files: ChangeLog.md + +library + exposed-modules: Data.Generics.Internal.GenericN + + , Data.Generics.Internal.Profunctor.Lens + , Data.Generics.Internal.Profunctor.Prism + , Data.Generics.Internal.Profunctor.Iso + + , Data.Generics.Internal.VL.Traversal + + , Data.GenericLens.Internal + + , Data.Generics.Internal.Families + , Data.Generics.Internal.Families.Changing + , Data.Generics.Internal.Families.Collect + , Data.Generics.Internal.Families.Has + , Data.Generics.Internal.Errors + , Data.Generics.Internal.Void + + , Data.Generics.Internal.Wrapped + + , Data.Generics.Sum.Internal.Constructors + , Data.Generics.Sum.Internal.Typed + , Data.Generics.Sum.Internal.Subtype + + , Data.Generics.Product.Internal.Param + , Data.Generics.Product.Internal.Types + + , Data.Generics.Product.Internal.Fields + , Data.Generics.Product.Internal.Typed + , Data.Generics.Product.Internal.Positions + , Data.Generics.Product.Internal.GLens + , Data.Generics.Product.Internal.Subtype + + , Data.Generics.Product.Internal.HList + + build-depends: base >= 4.11 && < 5 + , text >= 1.2 && < 1.3 + , indexed-profunctors >= 0.1 && < 1.0 + + hs-source-dirs: src + default-language: Haskell2010 + ghc-options: -Wall + +source-repository head + type: git + location: https://github.com/kcsongor/generic-lens + diff --git a/src/Data/GenericLens/Internal.hs b/src/Data/GenericLens/Internal.hs new file mode 100644 --- /dev/null +++ b/src/Data/GenericLens/Internal.hs @@ -0,0 +1,42 @@ +----------------------------------------------------------------------------- +-- | +-- Module : Data.GenericLens.Internal +-- Copyright : (C) 2020 Csongor Kiss +-- License : BSD3 +-- Maintainer : Csongor Kiss +-- Stability : experimental +-- Portability : non-portable +-- +-- The library internals are exposed through this module. Please keep +-- in mind that everything here is subject to change irrespective of +-- the the version numbers. +----------------------------------------------------------------------------- + +module Data.GenericLens.Internal + ( module Data.Generics.Internal.Families + , module Data.Generics.Internal.Families.Changing + , module Data.Generics.Internal.Families.Collect + , module Data.Generics.Internal.Families.Has + , module Data.Generics.Internal.Void + , module Data.Generics.Internal.Errors + + , module Data.Generics.Internal.GenericN + + -- * Profunctor optics + , module Data.Generics.Internal.Profunctor.Iso + , module Data.Generics.Internal.Profunctor.Lens + , module Data.Generics.Internal.Profunctor.Prism + ) where + +import Data.Generics.Internal.Families +import Data.Generics.Internal.Families.Changing +import Data.Generics.Internal.Families.Collect +import Data.Generics.Internal.Families.Has +import Data.Generics.Internal.Void +import Data.Generics.Internal.Errors + +import Data.Generics.Internal.GenericN + +import Data.Generics.Internal.Profunctor.Iso +import Data.Generics.Internal.Profunctor.Lens +import Data.Generics.Internal.Profunctor.Prism diff --git a/src/Data/Generics/Internal/Errors.hs b/src/Data/Generics/Internal/Errors.hs new file mode 100644 --- /dev/null +++ b/src/Data/Generics/Internal/Errors.hs @@ -0,0 +1,59 @@ +{-# LANGUAGE UndecidableInstances #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE KindSignatures #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE KindSignatures #-} + +------------------------------------------------------------------------------- +---- | +---- Module : Data.Generics.Internal.Errors +---- Copyright : (C) 2020 Csongor Kiss +---- License : BSD3 +---- Maintainer : Csongor Kiss +---- Stability : experimental +---- Portability : non-portable +---- +---- Provide more legible type errors as described in +---- (https://kcsongor.github.io/report-stuck-families/)[this blog post]. +------------------------------------------------------------------------------- + +module Data.Generics.Internal.Errors + ( NoGeneric + , Defined + , Defined_list + + , QuoteType + , PrettyError + ) where + +import GHC.Generics +import GHC.TypeLits +import Data.Kind + +type family NoGeneric (a :: Type) (ctxt :: [ErrorMessage]) :: Constraint where + NoGeneric a ctxt = PrettyError ('Text "No instance for " ':<>: QuoteType (Generic a) + ': ctxt) +type family PrettyError (ctxt :: [ErrorMessage]) :: k where + PrettyError '[] = TypeError ('Text "") + PrettyError (c ': cs) = TypeError ('Text "| " ':<>: c ':$$: PrettyLines cs) + +type family PrettyLines (ctxt :: [ErrorMessage]) :: ErrorMessage where + PrettyLines '[] = 'Text "" + PrettyLines (c ': cs) = 'Text "| " ':<>: c ':$$: PrettyLines cs + +type family Defined (break :: Type -> Type) (err :: Constraint) (a :: k) :: k where + Defined Void1 _ _ = Any + Defined _ _ k = k + +type family Defined_list (break :: [*]) (err :: Constraint) (a :: k) :: k where + Defined_list '[Void] _ _ = Any + Defined_list _ _ k = k + +data Void1 a +data Void +type family Any :: k + +type family QuoteType (typ :: k) :: ErrorMessage where + QuoteType typ = 'Text "‘" ':<>: 'ShowType typ ':<>: 'Text "’" diff --git a/src/Data/Generics/Internal/Families.hs b/src/Data/Generics/Internal/Families.hs new file mode 100644 --- /dev/null +++ b/src/Data/Generics/Internal/Families.hs @@ -0,0 +1,34 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE KindSignatures #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE TypeOperators #-} + +----------------------------------------------------------------------------- +-- | +-- Module : Data.Generics.Internal.Families +-- Copyright : (C) 2020 Csongor Kiss +-- License : BSD3 +-- Maintainer : Csongor Kiss +-- Stability : experimental +-- Portability : non-portable +-- +----------------------------------------------------------------------------- +module Data.Generics.Internal.Families + ( module Families + , ShowSymbols + ) where + +import Data.Generics.Internal.Families.Collect as Families +import Data.Generics.Internal.Families.Has as Families +import Data.Generics.Internal.Families.Changing as Families + +import GHC.TypeLits (ErrorMessage (..), Symbol) + +type family ShowSymbols (ctors :: [Symbol]) :: ErrorMessage where + ShowSymbols '[] + = 'Text "" + ShowSymbols (c ': cs) + = 'Text "• " ':<>: 'Text c ':$$: ShowSymbols cs diff --git a/src/Data/Generics/Internal/Families/Changing.hs b/src/Data/Generics/Internal/Families/Changing.hs new file mode 100644 --- /dev/null +++ b/src/Data/Generics/Internal/Families/Changing.hs @@ -0,0 +1,137 @@ +{-# LANGUAGE AllowAmbiguousTypes #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE FunctionalDependencies #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE UndecidableInstances #-} + +module Data.Generics.Internal.Families.Changing + ( Indexed + , Infer + , PTag (..) + , P + , LookupParam + , ArgAt + , ArgCount + , UnifyHead + ) where + +import GHC.TypeLits (Nat, type (-), type (+), TypeError, ErrorMessage (..)) + +{- + Note [Changing type parameters] + ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + + To get good type inference for type-changing lenses, we want to be able + map the field's type back to the type argument it corresponds to. This way, + when the field is changed, we know what the result type of the structure is + going to be. + + However, for a given type @t@, its representation @Rep t@ forgets which types + in the structure came from type variables, and which didn't. An @Int@ that + results from the instantiation of the type paremeter and an @Int@ that was + monomorphically specified in the structure are indistinguishable. + + The solution is to replace the type arguments in the type with unique + proxies, like: @T a b@ -> @T (P 1 a) (P 0 b)@. This way, if looking up + a field's type yields something of shape @P _ _@, we know it came from a type + parameter, and also know which. + + If the field's type is a proxy, then its type is allowed to change, otherwise + not. This also allows us to satisfy the functional dependency @s field b -> t@. + If after doing the conversion on @s@, @field@'s type is @(P _ a), then @t@ is + @s[b/a]@, otherwise @t ~ s@ and @b ~ a@. +-} + +-- `P` can be used in place of any type parameter, which means that it can have +-- any kind, not just *, so a data type won't work. +-- (this caused https://github.com/kcsongor/generic-lens/issues/23) +-- Instead, we use a matchable type family to wrap any `k` - however, we can no longer directly +-- pattern match on `P`, as it's not a type constructor. But we can still take it apart as a polymorphic +-- application form. In order to distinguish between applications of P and other type constructors, we use a tag, `PTag` +-- to fake a type constructor. +data PTag = PTag +type family P :: Nat -> k -> PTag -> k + +type Indexed t = Indexed' t 0 + +type family Indexed' (t :: k) (next :: Nat) :: k where + Indexed' (t (a :: j) :: k) next = (Indexed' t (next + 1)) (P next a 'PTag) + Indexed' t _ = t + +data Sub where + Sub :: Nat -> k -> Sub + +type family Unify (a :: k) (b :: k) :: [Sub] where + Unify (p n _ 'PTag) a' = '[ 'Sub n a'] + Unify (a x) (b y) = Unify x y ++ Unify a b + Unify a a = '[] + Unify a b = TypeError + ( 'Text "Couldn't match type " + ':<>: 'ShowType a + ':<>: 'Text " with " + ':<>: 'ShowType b + ) + +type family (xs :: [k]) ++ (ys :: [k]) :: [k] where + '[] ++ ys = ys + (x ': xs) ++ ys = x ': (xs ++ ys) + +type family Infer (s :: *) (a' :: *) (b :: *) :: * where + Infer (s a) a' b + = ReplaceArgs (s a) (Unify a' b) + Infer s _ _ = s + +-------------------------------------------------------------------------------- + +-- [TODO]: work this out +-- +--type family ArgKind (t :: k) (pos :: Nat) :: * where +-- ArgKind (t (a :: k)) 'Z = k +-- ArgKind (t _) ('S pos) = ArgKind t pos +-- +--type family ReplaceArg (t :: k) (pos :: Nat) (to :: ArgKind t pos) :: k where +-- ReplaceArg (t a) 'Z to = t to +-- ReplaceArg (t a) ('S pos) to = ReplaceArg t pos to a +-- ReplaceArg t _ _ = t + +type family ReplaceArg (t :: k) (pos :: Nat) (to :: j) :: k where + ReplaceArg (t a) 0 to = t to + ReplaceArg (t a) pos to = ReplaceArg t (pos - 1) to a + ReplaceArg t _ _ = t + +type family ReplaceArgs (t :: k) (subs :: [Sub]) :: k where + ReplaceArgs t '[] = t + ReplaceArgs t ('Sub n arg ': ss) = ReplaceArgs (ReplaceArg t n arg) ss + +type family LookupParam (a :: k) (p :: Nat) :: Maybe Nat where + LookupParam (param (n :: Nat)) m = 'Nothing + LookupParam (a (_ (m :: Nat))) n = IfEq m n ('Just 0) (MaybeAdd (LookupParam a n) 1) + LookupParam (a _) n = MaybeAdd (LookupParam a n) 1 + LookupParam a _ = 'Nothing + +type family MaybeAdd (a :: Maybe Nat) (b :: Nat) :: Maybe Nat where + MaybeAdd 'Nothing _ = 'Nothing + MaybeAdd ('Just a) b = 'Just (a + b) + +type family IfEq (a :: k) (b :: k) (t :: l) (f :: l) :: l where + IfEq a a t _ = t + IfEq _ _ _ f = f + +type family ArgCount (t :: k) :: Nat where + ArgCount (f a) = 1 + ArgCount f + ArgCount a = 0 + +type family ArgAt (t :: k) (n :: Nat) :: j where + ArgAt (t a) 0 = a + ArgAt (t a) n = ArgAt t (n - 1) + + +-- | Ensure that the types @a@ and @b@ are both applications of the same +-- constructor. The arguments may be different. +class UnifyHead (a :: k) (b :: k) +instance {-# OVERLAPPING #-} (gb ~ g b, UnifyHead f g) => UnifyHead (f a) gb +instance (a ~ b) => UnifyHead a b diff --git a/src/Data/Generics/Internal/Families/Collect.hs b/src/Data/Generics/Internal/Families/Collect.hs new file mode 100644 --- /dev/null +++ b/src/Data/Generics/Internal/Families/Collect.hs @@ -0,0 +1,133 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE UndecidableInstances #-} + +----------------------------------------------------------------------------- +-- | +-- Module : Data.Generics.Internal.Families.Collect +-- Copyright : (C) 2020 Csongor Kiss +-- License : BSD3 +-- Maintainer : Csongor Kiss +-- Stability : experimental +-- Portability : non-portable +-- +----------------------------------------------------------------------------- +module Data.Generics.Internal.Families.Collect + ( CollectTotalType + , CollectPartialType + , CollectField + , CollectFieldsOrdered + , TypeStat (..) + , type (\\) + ) where + +import Data.Type.Bool (If) +import Data.Type.Equality (type (==)) +import GHC.Generics +import GHC.TypeLits (Symbol, CmpSymbol) + +import Data.Generics.Product.Internal.HList (type (++)) +import Data.Generics.Internal.Families.Has (GTypes) + +data TypeStat + = TypeStat + { _containsNone :: [Symbol] + , _containsMultiple :: [Symbol] + , _containsOne :: [Symbol] + } + +type EmptyStat = 'TypeStat '[] '[] '[] + +type family CollectTotalType t f :: TypeStat where + CollectTotalType t (C1 ('MetaCons ctor _ _) f) + = AddToStat ctor (CountType t f) EmptyStat + CollectTotalType t (M1 _ _ r) + = CollectTotalType t r + CollectTotalType t (l :+: r) + = MergeStat (CollectTotalType t l) (CollectTotalType t r) + +type family CollectField t f :: TypeStat where + CollectField t (C1 ('MetaCons ctor _ _) f) + = AddToStat ctor (CountField t f) EmptyStat + CollectField t (M1 _ _ r) + = CollectField t r + CollectField t (l :+: r) + = MergeStat (CollectField t l) (CollectField t r) + +type family AddToStat (ctor :: Symbol) (count :: Count) (st :: TypeStat) :: TypeStat where + AddToStat ctor 'None ('TypeStat n m o) = 'TypeStat (ctor ': n) m o + AddToStat ctor 'Multiple ('TypeStat n m o) = 'TypeStat n (ctor ': m) o + AddToStat ctor 'One ('TypeStat n m o) = 'TypeStat n m (ctor ': o) + +type family MergeStat (st1 :: TypeStat) (st2 :: TypeStat) :: TypeStat where + MergeStat ('TypeStat n m o) ('TypeStat n' m' o') = 'TypeStat (n ++ n') (m ++ m') (o ++ o') + +type family CountType t f :: Count where + CountType t (S1 _ (Rec0 t)) + = 'One + CountType t (l :*: r) + = CountType t l <|> CountType t r + CountType t _ + = 'None + +type family CountField (field :: Symbol) f :: Count where + CountField field (S1 ('MetaSel ('Just field) _ _ _) _) + = 'One + CountField field (l :*: r) + = CountField field l <|> CountField field r + CountField _ _ + = 'None + +type family CollectPartialType t f :: [Symbol] where + CollectPartialType t (l :+: r) + = CollectPartialType t l ++ CollectPartialType t r + CollectPartialType t (C1 ('MetaCons ctor _ _) f) + = If (t == GTypes f) '[ctor] '[] + CollectPartialType t (D1 _ f) + = CollectPartialType t f + +data Count + = None + | One + | Multiple + +type family (a :: Count) <|> (b :: Count) :: Count where + 'None <|> b = b + a <|> 'None = a + a <|> b = 'Multiple + +type family (a :: Count) <&> (b :: Count) :: Count where + a <&> a = a + _ <&> _ = 'Multiple + +type family CollectFieldsOrdered (r :: * -> *) :: [Symbol] where + CollectFieldsOrdered (l :*: r) + = Merge (CollectFieldsOrdered l) (CollectFieldsOrdered r) + CollectFieldsOrdered (S1 ('MetaSel ('Just name) _ _ _) _) + = '[name] + CollectFieldsOrdered (M1 _ m a) + = CollectFieldsOrdered a + CollectFieldsOrdered _ + = '[] + +type family Merge (xs :: [Symbol]) (ys :: [Symbol]) :: [Symbol] where + Merge xs '[] = xs + Merge '[] ys = ys + Merge (x ': xs) (y ': ys) = Merge' (CmpSymbol x y) x y xs ys + +type family Merge' (ord :: Ordering) (x :: Symbol) (y :: Symbol) (xs :: [Symbol]) (ys :: [Symbol]) :: [Symbol] where + Merge' 'LT x y xs ys = x ': Merge xs (y ': ys) + Merge' _ x y xs ys = y ': Merge (x ': xs) ys + +type family (xs :: [Symbol]) \\ (ys :: [Symbol]) :: [Symbol] where + xs \\ '[] = xs + '[] \\ xs = '[] + (x ': xs) \\ (y ': ys) = Sub' (CmpSymbol x y) x y xs ys + +infixr 5 \\ +type family Sub' (ord :: Ordering) (x :: Symbol) (y :: Symbol) (xs :: [Symbol]) (ys :: [Symbol]) :: [Symbol] where + Sub' 'LT x y xs ys = x ': (xs \\ y ': ys) + Sub' 'GT x _ xs ys = (x ': xs) \\ ys + Sub' 'EQ _ _ xs ys = xs \\ ys diff --git a/src/Data/Generics/Internal/Families/Has.hs b/src/Data/Generics/Internal/Families/Has.hs new file mode 100644 --- /dev/null +++ b/src/Data/Generics/Internal/Families/Has.hs @@ -0,0 +1,134 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE UndecidableInstances #-} + +----------------------------------------------------------------------------- +-- | +-- Module : Data.Generics.Internal.Families.Has +-- Copyright : (C) 2020 Csongor Kiss +-- License : BSD3 +-- Maintainer : Csongor Kiss +-- Stability : experimental +-- Portability : non-portable +-- +----------------------------------------------------------------------------- +module Data.Generics.Internal.Families.Has + ( HasTotalFieldP + , HasTotalTypeP + , HasTotalPositionP + , Pos + , HasPartialTypeP + , HasCtorP + , GTypes + ) where + +import Data.Type.Bool (type (||)) +import Data.Type.Equality (type (==)) +import GHC.Generics +import GHC.TypeLits (Symbol, Nat) +import Data.Kind (Type) + +import Data.Generics.Product.Internal.HList + +-- Note: these could be factored out into a single traversal + +type family Both (m1 :: Maybe a) (m2 :: Maybe a) :: Maybe a where + Both ('Just a) ('Just a) = 'Just a + +type family Alt (m1 :: Maybe a) (m2 :: Maybe a) :: Maybe a where + Alt ('Just a) _ = 'Just a + Alt _ b = b + +type family HasTotalFieldP (field :: Symbol) f :: Maybe Type where + HasTotalFieldP field (S1 ('MetaSel ('Just field) _ _ _) (Rec0 t)) + = 'Just t + HasTotalFieldP field (l :*: r) + = Alt (HasTotalFieldP field l) (HasTotalFieldP field r) + HasTotalFieldP field (l :+: r) + = Both (HasTotalFieldP field l) (HasTotalFieldP field r) + HasTotalFieldP field (S1 _ _) + = 'Nothing + HasTotalFieldP field (C1 _ f) + = HasTotalFieldP field f + HasTotalFieldP field (D1 _ f) + = HasTotalFieldP field f + HasTotalFieldP field (K1 _ _) + = 'Nothing + HasTotalFieldP field U1 + = 'Nothing + HasTotalFieldP field V1 + = 'Nothing + +type family HasTotalTypeP (typ :: Type) f :: Maybe Type where + HasTotalTypeP typ (S1 _ (K1 _ typ)) + = 'Just typ + HasTotalTypeP typ (l :*: r) + = Alt (HasTotalTypeP typ l) (HasTotalTypeP typ r) + HasTotalTypeP typ (l :+: r) + = Both (HasTotalTypeP typ l) (HasTotalTypeP typ r) + HasTotalTypeP typ (S1 _ _) + = 'Nothing + HasTotalTypeP typ (C1 _ f) + = HasTotalTypeP typ f + HasTotalTypeP typ (D1 _ f) + = HasTotalTypeP typ f + HasTotalTypeP typ (K1 _ _) + = 'Nothing + HasTotalTypeP typ U1 + = 'Nothing + HasTotalTypeP typ V1 + = 'Nothing + +data Pos (p :: Nat) + +type family HasTotalPositionP (pos :: Nat) f :: Maybe Type where + HasTotalPositionP pos (S1 _ (K1 (Pos pos) t)) + = 'Just t + HasTotalPositionP pos (l :*: r) + = Alt (HasTotalPositionP pos l) (HasTotalPositionP pos r) + HasTotalPositionP pos (l :+: r) + = Both (HasTotalPositionP pos l) (HasTotalPositionP pos r) + HasTotalPositionP pos (S1 _ _) + = 'Nothing + HasTotalPositionP pos (C1 _ f) + = HasTotalPositionP pos f + HasTotalPositionP pos (D1 _ f) + = HasTotalPositionP pos f + HasTotalPositionP pos (K1 _ _) + = 'Nothing + HasTotalPositionP pos U1 + = 'Nothing + HasTotalPositionP pos V1 + = 'Nothing + +type family HasPartialTypeP a f :: Bool where + HasPartialTypeP t (l :+: r) + = HasPartialTypeP t l || HasPartialTypeP t r + HasPartialTypeP t (C1 m f) + = t == GTypes f + HasPartialTypeP t (M1 _ _ f) + = HasPartialTypeP t f + HasPartialTypeP t _ + = 'False + +type family HasCtorP (ctor :: Symbol) f :: Bool where + HasCtorP ctor (C1 ('MetaCons ctor _ _) _) + = 'True + HasCtorP ctor (f :+: g) + = HasCtorP ctor f || HasCtorP ctor g + HasCtorP ctor (D1 m f) + = HasCtorP ctor f + HasCtorP ctor _ + = 'False + +type family GTypes (rep :: Type -> Type) :: [Type] where + GTypes (l :*: r) + = GTypes l ++ GTypes r + GTypes (K1 _ a) + = '[ a] + GTypes (M1 _ m a) + = GTypes a + GTypes U1 = '[] + diff --git a/src/Data/Generics/Internal/GenericN.hs b/src/Data/Generics/Internal/GenericN.hs new file mode 100644 --- /dev/null +++ b/src/Data/Generics/Internal/GenericN.hs @@ -0,0 +1,66 @@ +{-# OPTIONS_HADDOCK hide #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE InstanceSigs #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE UndecidableInstances #-} + +-------------------------------------------------------------------------------- +-- | +-- Module : Data.Generics.Internal.GenericN +-- Copyright : (C) 2020 Csongor Kiss +-- License : BSD3 +-- Maintainer : Csongor Kiss +-- Stability : experimental +-- Portability : non-portable +-- +-- Generic representation of types with multiple parameters +-- +-------------------------------------------------------------------------------- + +module Data.Generics.Internal.GenericN + ( Param (..) + , Rec (Rec, unRec) + , GenericN (..) + ) where + +import Data.Kind +import GHC.Generics +import GHC.TypeLits +import Data.Coerce + +data family Param :: Nat -> j -> k + +newtype instance Param n (a :: Type) + = StarParam { getStarParam :: a} + +type family Indexed (t :: k) (i :: Nat) :: k where + Indexed (t a) i = Indexed t (i + 1) (Param i a) + Indexed t _ = t + +newtype Rec (p :: Type) a x = Rec { unRec :: K1 R a x } + +class + ( Coercible (Rep a) (RepN a) + , Generic a + ) => GenericN (a :: Type) where + type family RepN (a :: Type) :: Type -> Type + type instance RepN a = Rep (Indexed a 0) + toN :: RepN a x -> a + fromN :: a -> RepN a x + +instance + ( Coercible (Rep a) (RepN a) + , Generic a + ) => GenericN a where + toN :: forall x. RepN a x -> a + toN = coerce (to :: Rep a x -> a) + {-# INLINE toN #-} + + fromN :: forall x. a -> RepN a x + fromN = coerce (from :: a -> Rep a x) + {-# INLINE fromN #-} diff --git a/src/Data/Generics/Internal/Profunctor/Iso.hs b/src/Data/Generics/Internal/Profunctor/Iso.hs new file mode 100644 --- /dev/null +++ b/src/Data/Generics/Internal/Profunctor/Iso.hs @@ -0,0 +1,86 @@ +{-# OPTIONS_HADDOCK hide #-} +{-# LANGUAGE TupleSections #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE NoMonomorphismRestriction #-} +{-# LANGUAGE Rank2Types #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE TypeFamilyDependencies #-} +{-# LANGUAGE TypeOperators #-} + +----------------------------------------------------------------------------- +-- | +-- Module : Data.Generics.Internal.Profunctor.Iso +-- Copyright : (C) 2020 Csongor Kiss +-- License : BSD3 +-- Maintainer : Csongor Kiss +-- Stability : experimental +-- Portability : non-portable +-- +-- Internal lens helpers. Only exported for Haddock +-- +----------------------------------------------------------------------------- +module Data.Generics.Internal.Profunctor.Iso where + +import Data.Profunctor.Indexed +import GHC.Generics ((:*:)(..), (:+:)(..), Generic(..), M1(..), K1(..), Rep) +import Data.Generics.Internal.GenericN (Rec (..)) + +-- import qualified Data.Generics.Internal.VL.Iso as VL + +type Iso s t a b + = forall p i. (Profunctor p) => p i a b -> p i s t + +type Iso' s a = Iso s s a a + +-- | A type and its generic representation are isomorphic +repIso :: (Generic a, Generic b) => Iso a b (Rep a x) (Rep b x) +repIso = iso from to + +-- | 'M1' is just a wrapper around `f p` +--mIso :: Iso' (M1 i c f p) (f p) +mIso :: Iso (M1 i c f p) (M1 i c g p) (f p) (g p) +mIso = iso unM1 M1 +{-# INLINE mIso #-} + +kIso :: Iso (K1 r a p) (K1 r b p) a b +kIso = iso unK1 K1 +{-# INLINE kIso #-} + +recIso :: Iso (Rec r a p) (Rec r b p) a b +recIso = iso (unK1 . unRec) (Rec . K1) +{-# INLINE recIso #-} + +sumIso :: Iso ((a :+: b) x) ((a' :+: b') x) (Either (a x) (b x)) (Either (a' x) (b' x)) +sumIso = iso back forth + where forth (Left l) = L1 l + forth (Right r) = R1 r + back (L1 l) = Left l + back (R1 r) = Right r +{-# INLINE sumIso #-} + +prodIso :: Iso ((a :*: b) x) ((a' :*: b') x) (a x, b x) (a' x, b' x) +prodIso = iso (\(a :*: b) -> (a, b)) (\(a, b) -> (a :*: b)) + +assoc3 :: Iso ((a, b), c) ((a', b'), c') (a, (b, c)) (a', (b', c')) +assoc3 = iso (\((a, b), c) -> (a, (b, c))) (\(a, (b, c)) -> ((a, b), c)) + +-------------------------------------------------------------------------------- +-- Iso stuff + +fromIso :: Iso s t a b -> Iso b a t s +fromIso l = withIso l $ \ sa bt -> iso bt sa +{-# INLINE fromIso #-} + +iso :: (s -> a) -> (b -> t) -> Iso s t a b +iso = dimap +{-# INLINE iso #-} + +withIso :: Iso s t a b -> ((s -> a) -> (b -> t) -> r) -> r +withIso ai k = case ai (Exchange id id) of + Exchange sa bt -> k sa bt + +pairing :: Iso s t a b -> Iso s' t' a' b' -> Iso (s, s') (t, t') (a, a') (b, b') +pairing f g = withIso f $ \ sa bt -> withIso g $ \s'a' b't' -> + iso (bmap sa s'a') (bmap bt b't') + where bmap f' g' (a, b) = (f' a, g' b) diff --git a/src/Data/Generics/Internal/Profunctor/Lens.hs b/src/Data/Generics/Internal/Profunctor/Lens.hs new file mode 100644 --- /dev/null +++ b/src/Data/Generics/Internal/Profunctor/Lens.hs @@ -0,0 +1,137 @@ +{-# OPTIONS_HADDOCK hide #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE NoMonomorphismRestriction #-} +{-# LANGUAGE Rank2Types #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TupleSections #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE TypeFamilyDependencies #-} +{-# LANGUAGE TypeOperators #-} + +----------------------------------------------------------------------------- +-- | +-- Module : Data.Generics.Internal.Profunctor.Lens +-- Copyright : (C) 2020 Csongor Kiss +-- License : BSD3 +-- Maintainer : Csongor Kiss +-- Stability : experimental +-- Portability : non-portable +-- +-- Internal lens helpers. Only exported for Haddock +-- +----------------------------------------------------------------------------- +module Data.Generics.Internal.Profunctor.Lens where + +import Data.Profunctor.Indexed (Profunctor(..), Strong(..)) +import Data.Bifunctor +import GHC.Generics +import Data.Generics.Internal.Profunctor.Iso + +type Lens s t a b + = forall p i . Strong p => p i a b -> p i s t + +type LensLike p s t a b + = p a b -> p s t + + +ravel :: (ALens a b i a b -> ALens a b i s t) -> Lens s t a b +ravel l pab = conv (l idLens) pab + where + conv :: ALens a b i s t -> Lens s t a b + conv (ALens _get _set) = lens _get _set + +-- | Setting +set :: ((a -> b) -> s -> t) -> (s, b) -> t +set f (s, b) + = f (const b) s + +view :: Lens s s a a -> s -> a +view l = withLensPrim l (\get _ -> snd . get) + +--withLens :: Lens s t a b -> ((s -> a) -> ((s, b) -> t) -> r) -> r +--ithLens l k = +-- case l idLens of +-- ALens _get _set -> k (snd . _get) (\(s, b) -> _set ((fst $ _get s), b)) + +withLensPrim :: Lens s t a b -> (forall c . (s -> (c,a)) -> ((c, b) -> t) -> r) -> r +withLensPrim l k = + case l idLens of + ALens _get _set -> k _get _set + +idLens :: ALens a b i a b +idLens = ALens (fork (const ()) id) snd +{-# INLINE idLens #-} + +-- | Lens focusing on the first element of a product +first :: Lens ((a :*: b) x) ((a' :*: b) x) (a x) (a' x) +first + = lens (\(a :*: b) -> (b,a)) (\(b, a') -> a' :*: b) + +-- | Lens focusing on the second element of a product +second :: Lens ((a :*: b) x) ((a :*: b') x) (b x) (b' x) +second + = lens (\(a :*: b) -> (a,b)) (\(a, b') -> a :*: b') + +fork :: (a -> b) -> (a -> c) -> a -> (b, c) +fork f g a = (f a, g a) + +-------------------------------------------------------------------------------- + +data Coyoneda f b = forall a. Coyoneda (a -> b) (f a) + +instance Functor (Coyoneda f) where + fmap f (Coyoneda g fa) + = Coyoneda (f . g) fa + +inj :: Functor f => Coyoneda f a -> f a +inj (Coyoneda f a) = fmap f a + +proj :: Functor f => f a -> Coyoneda f a +proj fa = Coyoneda id fa + +(??) :: Functor f => f (a -> b) -> a -> f b +fab ?? a = fmap ($ a) fab + +assoc3L :: Lens ((a, b), c) ((a', b'), c') (a, (b, c)) (a', (b', c')) +assoc3L f = assoc3 f + +stron :: (Either s s', b) -> Either (s, b) (s', b) +stron (e, b) = bimap (,b) (, b) e + +choosing :: forall s t a b s' t' . Lens s t a b -> Lens s' t' a b -> Lens (Either s s') (Either t t') a b +choosing l r = withLensPrim l (\getl setl -> + withLensPrim r (\getr setr -> + let --g :: Either s s' -> a + g e = case e of + Left v -> let (c, v') = getl v in (Left c, v') + Right v -> let (c, v') = getr v in (Right c, v') + s = bimap setl setr . stron + in lens g s)) + +lens :: (s -> (c,a)) -> ((c,b) -> t) -> Lens s t a b +lens get _set = dimap get _set . second' +{-# INLINE lens #-} + +------------------------------------------------------------------------------ + +data ALens a b i s t = forall c . ALens (s -> (c,a)) ((c, b) -> t) + +instance Functor (ALens a b i s) where + fmap f (ALens _get _set) = ALens _get (f . _set) + +instance Profunctor (ALens a b) where + dimap f g (ALens get _set) = ALens (get . f) (g . _set) + lmap f = dimap f id + rmap f = dimap id f + +swap :: (a, b) -> (b, a) +swap (x, y) = (y, x) + +instance Strong (ALens a b) where + first' = dimap swap swap . second' + {-# INLINE first' #-} + second' (ALens get _set) = ALens get' set' + where + get' (c, a1) = let (c1, a) = get a1 in ((c, c1), a) + set' ((c, c1), b) = (c, _set (c1, b)) + {-# INLINE second' #-} diff --git a/src/Data/Generics/Internal/Profunctor/Prism.hs b/src/Data/Generics/Internal/Profunctor/Prism.hs new file mode 100644 --- /dev/null +++ b/src/Data/Generics/Internal/Profunctor/Prism.hs @@ -0,0 +1,81 @@ +{-# OPTIONS_HADDOCK hide #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE LambdaCase #-} +{-# LANGUAGE NoMonomorphismRestriction #-} +{-# LANGUAGE Rank2Types #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE TypeFamilyDependencies #-} +{-# LANGUAGE TypeOperators #-} + +----------------------------------------------------------------------------- +-- | +-- Module : Data.Generics.Internal.Profunctor.Prism +-- Copyright : (C) 2020 Csongor Kiss +-- License : BSD3 +-- Maintainer : Csongor Kiss +-- Stability : experimental +-- Portability : non-portable +-- +-- Internal lens helpers. Only exported for Haddock +-- +----------------------------------------------------------------------------- +module Data.Generics.Internal.Profunctor.Prism where + +import Data.Profunctor.Indexed +import GHC.Generics + +type APrism i s t a b = Market a b i a b -> Market a b i s t + +type Prism s t a b + = forall p i . (Choice p) => p i a b -> p i s t + +type Prism' s a = forall p i . (Choice p) => p i a a -> p i s s + +left :: Prism ((a :+: c) x) ((b :+: c) x) (a x) (b x) +left = prism L1 $ gsum Right (Left . R1) + +right :: Prism ((a :+: b) x) ((a :+: c) x) (b x) (c x) +right = prism R1 $ gsum (Left . L1) Right + +prism :: (b -> t) -> (s -> Either t a) -> Prism s t a b +prism bt seta eta = dimap seta (either id bt) (right' eta) + +_Left :: Prism (Either a c) (Either b c) a b +_Left = left' + +_Right :: Prism (Either c a) (Either c b) a b +_Right = right' + +prismPRavel :: APrism i s t a b -> Prism s t a b +prismPRavel l pab = (prism2prismp $ l idPrism) pab + +build :: (Tagged i b b -> Tagged i t t) -> b -> t +build p = unTagged #. p .# Tagged + +match :: Prism s t a b -> s -> Either t a +match k = withPrism k $ \_ _match -> _match + +-------------------------------------------------------------------------------- +-- Prism stuff + +without' :: Prism s t a b -> Prism s t c d -> Prism s t (Either a c) (Either b d) +without' k = + withPrism k $ \bt _ k' -> + withPrism k' $ \dt setc -> + prism (either bt dt) $ \s -> fmap Right (setc s) +{-# INLINE without' #-} + +withPrism :: APrism i s t a b -> ((b -> t) -> (s -> Either t a) -> r) -> r +withPrism k f = case k idPrism of + Market bt seta -> f bt seta + +prism2prismp :: Market a b i s t -> Prism s t a b +prism2prismp (Market bt seta) = prism bt seta + +idPrism :: Market a b i a b +idPrism = Market id Right + +gsum :: (a x -> c) -> (b x -> c) -> ((a :+: b) x) -> c +gsum f _ (L1 x) = f x +gsum _ g (R1 y) = g y diff --git a/src/Data/Generics/Internal/VL/Traversal.hs b/src/Data/Generics/Internal/VL/Traversal.hs new file mode 100644 --- /dev/null +++ b/src/Data/Generics/Internal/VL/Traversal.hs @@ -0,0 +1,76 @@ +{-# OPTIONS_HADDOCK hide #-} +{-# LANGUAGE AllowAmbiguousTypes #-} +{-# LANGUAGE ConstraintKinds #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE NoMonomorphismRestriction #-} +{-# LANGUAGE Rank2Types #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE TypeFamilyDependencies #-} +{-# LANGUAGE TypeOperators #-} + +----------------------------------------------------------------------------- +-- | +-- Module : Data.Generics.Internal.VL.Traversal +-- Copyright : (C) 2020 Csongor Kiss +-- License : BSD3 +-- Maintainer : Csongor Kiss +-- Stability : experimental +-- Portability : non-portable +-- +-- Internal lens helpers. Only exported for Haddock +-- +----------------------------------------------------------------------------- +module Data.Generics.Internal.VL.Traversal where + +-- | Type alias for traversal +type Traversal' s a + = forall f. Applicative f => (a -> f a) -> s -> f s + +type Traversal s t a b + = forall f. Applicative f => (a -> f b) -> s -> f t + +confusing :: Applicative f => Traversal s t a b -> (a -> f b) -> s -> f t +confusing t = \f -> lowerYoneda . lowerCurried . t (liftCurriedYoneda . f) +{-# INLINE confusing #-} + +liftCurriedYoneda :: Applicative f => f a -> Curried (Yoneda f) a +liftCurriedYoneda fa = Curried (`yap` fa) +{-# INLINE liftCurriedYoneda #-} + +yap :: Applicative f => Yoneda f (a -> b) -> f a -> Yoneda f b +yap (Yoneda k) fa = Yoneda (\ab_r -> k (ab_r .) <*> fa) +{-# INLINE yap #-} + +newtype Curried f a = + Curried { runCurried :: forall r. f (a -> r) -> f r } + +instance Functor f => Functor (Curried f) where + fmap f (Curried g) = Curried (g . fmap (.f)) + {-# INLINE fmap #-} + +instance (Functor f) => Applicative (Curried f) where + pure a = Curried (fmap ($ a)) + {-# INLINE pure #-} + Curried mf <*> Curried ma = Curried (ma . mf . fmap (.)) + {-# INLINE (<*>) #-} + +liftCurried :: Applicative f => f a -> Curried f a +liftCurried fa = Curried (<*> fa) + +lowerCurried :: Applicative f => Curried f a -> f a +lowerCurried (Curried f) = f (pure id) +newtype Yoneda f a = Yoneda { runYoneda :: forall b. (a -> b) -> f b } + +liftYoneda :: Functor f => f a -> Yoneda f a +liftYoneda a = Yoneda (\f -> fmap f a) + +lowerYoneda :: Yoneda f a -> f a +lowerYoneda (Yoneda f) = f id + +instance Functor (Yoneda f) where + fmap f m = Yoneda (\k -> runYoneda m (k . f)) + +instance Applicative f => Applicative (Yoneda f) where + pure a = Yoneda (\f -> pure (f a)) + Yoneda m <*> Yoneda n = Yoneda (\f -> m (f .) <*> n id) diff --git a/src/Data/Generics/Internal/Void.hs b/src/Data/Generics/Internal/Void.hs new file mode 100644 --- /dev/null +++ b/src/Data/Generics/Internal/Void.hs @@ -0,0 +1,19 @@ +{-# LANGUAGE PolyKinds #-} +module Data.Generics.Internal.Void where + +{- + Note [Uncluttering type signatures] + ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + + Because the various instances in the library always match (the Has* classes + are essentially glorified constraint synonyms), they get replaced with + their constraints, resulting in large, unreadable types. + + Writing an (overlapping instance) for this Void type means that the original + instance might not be the one selected, thus GHC leaves the constraints in + place until further information is provided, at which point the type + machinery has sufficient information to reduce to sensible types. +-} +data Void +data Void1 a +data Void2 a b diff --git a/src/Data/Generics/Internal/Wrapped.hs b/src/Data/Generics/Internal/Wrapped.hs new file mode 100644 --- /dev/null +++ b/src/Data/Generics/Internal/Wrapped.hs @@ -0,0 +1,55 @@ +{-# LANGUAGE AllowAmbiguousTypes #-} +{-# LANGUAGE TypeApplications #-} +{-# language ConstraintKinds #-} +{-# language DataKinds #-} +{-# language FlexibleContexts #-} +{-# language FlexibleInstances #-} +{-# language FunctionalDependencies #-} +{-# language MultiParamTypeClasses #-} +{-# language ScopedTypeVariables #-} +{-# language TypeFamilies #-} +{-# language TypeOperators #-} +{-# language UndecidableInstances #-} + +module Data.Generics.Internal.Wrapped + ( Context + , derived + ) where + +import Data.Generics.Internal.Profunctor.Iso + +import Data.Generics.Internal.Families.Changing ( UnifyHead ) + +import Data.Kind (Constraint) +import GHC.Generics +import GHC.TypeLits + +type Context s t a b + = ( Generic s + , Generic t + , GWrapped (Rep s) (Rep t) a b + , UnifyHead s t + , UnifyHead t s + , ErrorUnlessOnlyOne s (Rep s) + ) + +derived :: Context s t a b => Iso s t a b +derived = repIso . gWrapped +{-# INLINE derived #-} + +type family ErrorUnlessOnlyOne a b :: Constraint where + ErrorUnlessOnlyOne t (M1 i k a) = ErrorUnlessOnlyOne t a + ErrorUnlessOnlyOne t (K1 i a) = () + ErrorUnlessOnlyOne t a = + TypeError ('ShowType t ':<>: 'Text " is not a single-constructor, single-field datatype") + +-------------------------------------------------------------------------------- + +class GWrapped s t a b | s -> a, t -> b, s b -> t, t a -> s where + gWrapped :: Iso (s x) (t x) a b + +instance GWrapped s t a b => GWrapped (M1 i k s) (M1 i k t) a b where + gWrapped = mIso . gWrapped + +instance (a ~ c, b ~ d) => GWrapped (K1 i a) (K1 i b) c d where + gWrapped = kIso diff --git a/src/Data/Generics/Product/Internal/Fields.hs b/src/Data/Generics/Product/Internal/Fields.hs new file mode 100644 --- /dev/null +++ b/src/Data/Generics/Product/Internal/Fields.hs @@ -0,0 +1,104 @@ +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE AllowAmbiguousTypes #-} +{-# LANGUAGE ConstraintKinds #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE FunctionalDependencies #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TypeApplications #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE TypeInType #-} +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE UndecidableInstances #-} +{-# LANGUAGE UndecidableSuperClasses #-} + +module Data.Generics.Product.Internal.Fields + ( Context_ + , Context' + , Context0 + , Context + , derived + ) where + +import Data.Generics.Internal.Families +import Data.Generics.Product.Internal.GLens +import Data.Kind (Constraint, Type) +import GHC.Generics +import GHC.TypeLits (Symbol, ErrorMessage(..), TypeError) +import Data.Generics.Internal.Errors +import Data.Generics.Internal.Profunctor.Lens +import Data.Generics.Internal.Profunctor.Iso + +-- Full context +class Context (field :: Symbol) s t a b | s field -> a, t field -> b, s field b -> t, t field a -> s +instance + ( HasTotalFieldP field (Rep s) ~ 'Just a + , HasTotalFieldP field (Rep t) ~ 'Just b + , HasTotalFieldP field (Rep (Indexed s)) ~ 'Just a' + , HasTotalFieldP field (Rep (Indexed t)) ~ 'Just b' + , t ~ Infer s a' b + , s ~ Infer t b' a + ) => Context field s t a b + +-- Alternative type inference +type Context_ field s t a b + = ( HasTotalFieldP field (Rep s) ~ 'Just a + , HasTotalFieldP field (Rep t) ~ 'Just b + , UnifyHead s t + , UnifyHead t s + ) + +-- Monomorphic +type Context' field s a + = ( Generic s + , ErrorUnless field s (CollectField field (Rep s)) + , GLens' (HasTotalFieldPSym field) (Rep s) a + , Defined (Rep s) + (NoGeneric s '[ 'Text "arising from a generic lens focusing on the " + ':<>: QuoteType field ':<>: 'Text " field of type " ':<>: QuoteType a + , 'Text "in " ':<>: QuoteType s]) + (() :: Constraint) + ) + +-- No inference +type Context0 field s t a b + = ( Generic s + , Generic t + , GLens (HasTotalFieldPSym field) (Rep s) (Rep t) a b + , ErrorUnless field s (CollectField field (Rep s)) + , Defined (Rep s) + (NoGeneric s '[ 'Text "arising from a generic lens focusing on the " + ':<>: QuoteType field ':<>: 'Text " field of type " ':<>: QuoteType a + , 'Text "in " ':<>: QuoteType s]) + (() :: Constraint) + ) + +derived :: forall field s t a b. Context0 field s t a b => Lens s t a b +derived = repIso . glens @(HasTotalFieldPSym field) +{-# INLINE derived #-} + +type family ErrorUnless (field :: Symbol) (s :: Type) (stat :: TypeStat) :: Constraint where + ErrorUnless field s ('TypeStat _ _ '[]) + = TypeError + ( 'Text "The type " + ':<>: 'ShowType s + ':<>: 'Text " does not contain a field named '" + ':<>: 'Text field ':<>: 'Text "'." + ) + + ErrorUnless field s ('TypeStat (n ': ns) _ _) + = TypeError + ( 'Text "Not all constructors of the type " + ':<>: 'ShowType s + ':$$: 'Text " contain a field named '" + ':<>: 'Text field ':<>: 'Text "'." + ':$$: 'Text "The offending constructors are:" + ':$$: ShowSymbols (n ': ns) + ) + + ErrorUnless _ _ ('TypeStat '[] '[] _) + = () + +data HasTotalFieldPSym :: Symbol -> (TyFun (Type -> Type) (Maybe Type)) +type instance Eval (HasTotalFieldPSym sym) tt = HasTotalFieldP sym tt diff --git a/src/Data/Generics/Product/Internal/GLens.hs b/src/Data/Generics/Product/Internal/GLens.hs new file mode 100644 --- /dev/null +++ b/src/Data/Generics/Product/Internal/GLens.hs @@ -0,0 +1,81 @@ +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE TypeInType #-} +{-# LANGUAGE AllowAmbiguousTypes #-} +{-# LANGUAGE ConstraintKinds #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE FunctionalDependencies #-} +{-# LANGUAGE KindSignatures #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE Rank2Types #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TypeApplications #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE UndecidableInstances #-} + +----------------------------------------------------------------------------- +-- | +-- Module : Data.Generics.Product.Internal.GLens +-- Copyright : (C) 2020 Csongor Kiss +-- License : BSD3 +-- Maintainer : Csongor Kiss +-- Stability : experimental +-- Portability : non-portable +-- +-- Derive record field getters and setters generically. +-- +----------------------------------------------------------------------------- + +module Data.Generics.Product.Internal.GLens + ( GLens (..) + , GLens' + , TyFun + , Eval + ) where + +import Data.Generics.Internal.Profunctor.Lens (Lens, choosing, first, second) +import Data.Generics.Internal.Profunctor.Iso (kIso, sumIso, mIso) + +import Data.Kind (Type) +import GHC.Generics + +type Pred = TyFun (Type -> Type) (Maybe Type) + +type TyFun a b = a -> b -> Type +type family Eval (f :: TyFun a b) (x :: a) :: b + +-- A generic lens that uses some predicate to determine which field to focus on +class GLens (pred :: Pred) (s :: Type -> Type) (t :: Type -> Type) a b | s pred -> a, t pred -> b where + glens :: Lens (s x) (t x) a b + +type GLens' pred s a = GLens pred s s a a + +instance GProductLens (Eval pred l) pred l r l' r' a b + => GLens pred (l :*: r) (l' :*: r') a b where + + glens = gproductLens @(Eval pred l) @pred + {-# INLINE glens #-} + +instance (GLens pred l l' a b, GLens pred r r' a b) => GLens pred (l :+: r) (l' :+: r') a b where + glens = sumIso . choosing (glens @pred) (glens @pred) + {-# INLINE glens #-} + +instance GLens pred (K1 r a) (K1 r b) a b where + glens = kIso + {-# INLINE glens #-} + +instance (GLens pred f g a b) => GLens pred (M1 m meta f) (M1 m meta g) a b where + glens = mIso . glens @pred + {-# INLINE glens #-} + +class GProductLens (left :: Maybe Type) (pred :: Pred) l r l' r' a b | pred l r -> a, pred l' r' -> b where + gproductLens :: Lens ((l :*: r) x) ((l' :*: r') x) a b + +instance GLens pred l l' a b => GProductLens ('Just x) pred l r l' r a b where + gproductLens = first . glens @pred + {-# INLINE gproductLens #-} + +instance GLens pred r r' a b => GProductLens 'Nothing pred l r l r' a b where + gproductLens = second . glens @pred + {-# INLINE gproductLens #-} diff --git a/src/Data/Generics/Product/Internal/HList.hs b/src/Data/Generics/Product/Internal/HList.hs new file mode 100644 --- /dev/null +++ b/src/Data/Generics/Product/Internal/HList.hs @@ -0,0 +1,347 @@ +{-# LANGUAGE AllowAmbiguousTypes #-} +{-# LANGUAGE ConstraintKinds #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE FunctionalDependencies #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TupleSections #-} +{-# LANGUAGE TypeApplications #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE TypeInType #-} +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE UndecidableInstances #-} + +----------------------------------------------------------------------------- +-- | +-- Module : Data.Generics.Product.Internal.HList +-- Copyright : (C) 2020 Csongor Kiss +-- License : BSD3 +-- Maintainer : Csongor Kiss +-- Stability : experimental +-- Portability : non-portable +-- +-- Derive an isomorphism between a product type and a flat HList. +-- +----------------------------------------------------------------------------- + +module Data.Generics.Product.Internal.HList + ( GIsList(..) + , IndexList (..) + , HList (..) + , type (++) + , Elem + , ListTuple (..) + , TupleToList + ) where + +import GHC.TypeLits + +import Data.Kind (Type) +import GHC.Generics +import Data.Profunctor.Indexed +import Data.Generics.Internal.Profunctor.Lens +import Data.Generics.Internal.Profunctor.Iso + +data HList (as :: [Type]) where + Nil :: HList '[] + (:>) :: a -> HList as -> HList (a ': as) + +infixr 5 :> + +type family ((as :: [k]) ++ (bs :: [k])) :: [k] where + '[] ++ bs = bs + (a ': as) ++ bs = a ': as ++ bs + +instance Semigroup (HList '[]) where + _ <> _ = Nil + +instance Monoid (HList '[]) where + mempty = Nil + mappend _ _ = Nil + +instance (Semigroup a, Semigroup (HList as)) => Semigroup (HList (a ': as)) where + (x :> xs) <> (y :> ys) = (x <> y) :> (xs <> ys) + +instance (Monoid a, Monoid (HList as)) => Monoid (HList (a ': as)) where + mempty = mempty :> mempty + mappend (x :> xs) (y :> ys) = mappend x y :> mappend xs ys + +class Elem (as :: [(k, Type)]) (key :: k) (i :: Nat) a | as key -> i a +instance {-# OVERLAPPING #-} pos ~ 0 => Elem (a ': xs) key pos a +instance (Elem xs key i a, pos ~ (i + 1)) => Elem (x ': xs) key pos a + +class GIsList + (f :: Type -> Type) + (g :: Type -> Type) + (as :: [Type]) + (bs :: [Type]) | f -> as, g -> bs, bs f -> g, as g -> f where + + glist :: Iso (f x) (g x) (HList as) (HList bs) + +instance + ( GIsList l l' as as' + , GIsList r r' bs bs' + , Appending as bs cs as' bs' cs' + , cs ~ (as ++ bs) + , cs' ~ (as' ++ bs') + ) => GIsList (l :*: r) (l' :*: r') cs cs' where + + glist = prodIso . pairing glist glist . appending + {-# INLINE glist #-} + +instance GIsList f g as bs => GIsList (M1 t meta f) (M1 t meta g) as bs where + glist = mIso . glist + {-# INLINE glist #-} + +instance GIsList (Rec0 a) (Rec0 b) '[a] '[b] where + glist = kIso . singleton + {-# INLINE glist #-} + +instance GIsList U1 U1 '[] '[] where + glist = iso (const Nil) (const U1) + {-# INLINE glist #-} + +-------------------------------------------------------------------------------- +-- | as ++ bs === cs +class Appending as bs cs as' bs' cs' + | as bs cs cs' -> as' bs' + , as' bs' cs cs' -> as bs + , as bs -> cs + , as' bs' -> cs' + where + appending :: Iso (HList as, HList bs) (HList as', HList bs') (HList cs) (HList cs') + +-- | [] ++ bs === bs +instance Appending '[] bs bs '[] bs' bs' where + appending = iso snd (Nil,) + +-- | (a : as) ++ bs === (a : cs) +instance + Appending as bs cs as' bs' cs' -- as ++ bs == cs + => Appending (a ': as) bs (a ': cs) (a' ': as') bs' (a' ': cs') where + appending + = pairing (fromIso consing) id -- ((a, as), bs) + . assoc3 -- (a, (as, bs)) + . pairing id appending -- (a, cs) + . consing -- (a : cs) + +singleton :: Iso a b (HList '[a]) (HList '[ b]) +singleton = iso (:> Nil) (\(x :> _) -> x) + +consing :: Iso (a, HList as) (b, HList bs) (HList (a ': as)) (HList (b ': bs)) +consing = iso (\(x, xs) -> x :> xs) (\(x :> xs) -> (x, xs)) + +-------------------------------------------------------------------------------- +class IndexList (i :: Nat) as bs a b | i as -> a, i bs -> b, i as b -> bs, i bs a -> as where + point :: Lens (HList as) (HList bs) a b + +instance {-# OVERLAPPING #-} + ( as ~ (a ': as') + , bs ~ (b ': as') + ) => IndexList 0 as bs a b where + point = lens (\(x :> xs) -> (xs, x)) (\(xs, x') -> x' :> xs) + {-# INLINE point #-} + +instance + ( IndexList (n - 1) as' bs' a b + , as ~ (x ': as') + , bs ~ (x ': bs') + ) => IndexList n as bs a b where + point = fromIso consing . second' . point @(n-1) + {-# INLINE point #-} + +-------------------------------------------------------------------------------- +-- * Convert tuples to/from HLists + +class ListTuple (tuple :: Type) (tuple' :: Type) (as :: [Type]) (bs :: [Type]) | as -> tuple, bs -> tuple' where + tupled :: Iso (HList as) (HList bs) tuple tuple' + tupled = iso (listToTuple @tuple @tuple' @as @bs) (tupleToList @tuple @tuple' @as @bs) + {-# INLINE tupled #-} + + tupleToList :: tuple' -> HList bs + listToTuple :: HList as -> tuple + +instance ListTuple () () '[] '[] + where + tupleToList _ = Nil + listToTuple _ = () + +instance ListTuple a a' '[a] '[a'] where + tupleToList a + = a :> Nil + listToTuple (a :> Nil) + = a + +instance ListTuple + (a1, b1) (a2, b2) + [a1, b1] [a2, b2] + where + tupleToList (a, b) + = a :> b :> Nil + listToTuple (a :> b :> Nil) + = (a, b) + +instance ListTuple + (a1, b1, c1) (a2, b2, c2) + [a1, b1, c1] [a2, b2, c2] + where + tupleToList (a, b, c) + = a :> b :> c :> Nil + listToTuple (a :> b :> c :> Nil) + = (a, b, c) + +instance ListTuple + (a1, b1, c1, d1) (a2, b2, c2, d2) + [a1, b1, c1, d1] [a2, b2, c2, d2] + where + tupleToList (a, b, c, d) + = a :> b :> c :> d:> Nil + listToTuple (a :> b :> c :> d :> Nil) + = (a, b, c, d) + +instance ListTuple + (a1, b1, c1, d1, e1) (a2, b2, c2, d2, e2) + [a1, b1, c1, d1, e1] [a2, b2, c2, d2, e2] + where + tupleToList (a, b, c, d, e) + = a :> b :> c :> d:> e :> Nil + listToTuple (a :> b :> c :> d :> e :> Nil) + = (a, b, c, d, e) + +instance ListTuple + (a1, b1, c1, d1, e1, f1) (a2, b2, c2, d2, e2, f2) + [a1, b1, c1, d1, e1, f1] [a2, b2, c2, d2, e2, f2] + where + tupleToList (a, b, c, d, e, f) + = a :> b :> c :> d:> e :> f :> Nil + listToTuple (a :> b :> c :> d :> e :> f :> Nil) + = (a, b, c, d, e, f) + +instance ListTuple + (a1, b1, c1, d1, e1, f1, g1) (a2, b2, c2, d2, e2, f2, g2) + [a1, b1, c1, d1, e1, f1, g1] [a2, b2, c2, d2, e2, f2, g2] + where + tupleToList (a, b, c, d, e, f, g) + = a :> b :> c :> d:> e :> f :> g :> Nil + listToTuple (a :> b :> c :> d :> e :> f :> g :> Nil) + = (a, b, c, d, e, f, g) + +instance ListTuple + (a1, b1, c1, d1, e1, f1, g1, h1) (a2, b2, c2, d2, e2, f2, g2, h2) + [a1, b1, c1, d1, e1, f1, g1, h1] [a2, b2, c2, d2, e2, f2, g2, h2] + where + tupleToList (a, b, c, d, e, f, g, h) + = a :> b :> c :> d:> e :> f :> g :> h :> Nil + listToTuple (a :> b :> c :> d :> e :> f :> g :> h :> Nil) + = (a, b, c, d, e, f, g, h) + +instance ListTuple + (a1, b1, c1, d1, e1, f1, g1, h1, j1) (a2, b2, c2, d2, e2, f2, g2, h2, j2) + [a1, b1, c1, d1, e1, f1, g1, h1, j1] [a2, b2, c2, d2, e2, f2, g2, h2, j2] + where + tupleToList (a, b, c, d, e, f, g, h, j) + = a :> b :> c :> d:> e :> f :> g :> h :> j :> Nil + listToTuple (a :> b :> c :> d :> e :> f :> g :> h :> j :> Nil) + = (a, b, c, d, e, f, g, h, j) + +instance ListTuple + (a1, b1, c1, d1, e1, f1, g1, h1, j1, k1) (a2, b2, c2, d2, e2, f2, g2, h2, j2, k2) + [a1, b1, c1, d1, e1, f1, g1, h1, j1, k1] [a2, b2, c2, d2, e2, f2, g2, h2, j2, k2] + where + tupleToList (a, b, c, d, e, f, g, h, j, k) + = a :> b :> c :> d:> e :> f :> g :> h :> j :> k :> Nil + listToTuple (a :> b :> c :> d :> e :> f :> g :> h :> j :> k :> Nil) + = (a, b, c, d, e, f, g, h, j, k) + +instance ListTuple + (a1, b1, c1, d1, e1, f1, g1, h1, j1, k1, l1) (a2, b2, c2, d2, e2, f2, g2, h2, j2, k2, l2) + [a1, b1, c1, d1, e1, f1, g1, h1, j1, k1, l1] [a2, b2, c2, d2, e2, f2, g2, h2, j2, k2, l2] + where + tupleToList (a, b, c, d, e, f, g, h, j, k, l) + = a :> b :> c :> d:> e :> f :> g :> h :> j :> k :> l :> Nil + listToTuple (a :> b :> c :> d :> e :> f :> g :> h :> j :> k :> l :> Nil) + = (a, b, c, d, e, f, g, h, j, k, l) + +instance ListTuple + (a1, b1, c1, d1, e1, f1, g1, h1, j1, k1, l1, m1) (a2, b2, c2, d2, e2, f2, g2, h2, j2, k2, l2, m2) + [a1, b1, c1, d1, e1, f1, g1, h1, j1, k1, l1, m1] [a2, b2, c2, d2, e2, f2, g2, h2, j2, k2, l2, m2] + where + tupleToList (a, b, c, d, e, f, g, h, j, k, l, m) + = a :> b :> c :> d:> e :> f :> g :> h :> j :> k :> l :> m :> Nil + listToTuple (a :> b :> c :> d :> e :> f :> g :> h :> j :> k :> l :> m :> Nil) + = (a, b, c, d, e, f, g, h, j, k, l, m) + +instance ListTuple + (a1, b1, c1, d1, e1, f1, g1, h1, j1, k1, l1, m1, n1) (a2, b2, c2, d2, e2, f2, g2, h2, j2, k2, l2, m2, n2) + [a1, b1, c1, d1, e1, f1, g1, h1, j1, k1, l1, m1, n1] [a2, b2, c2, d2, e2, f2, g2, h2, j2, k2, l2, m2, n2] + where + tupleToList (a, b, c, d, e, f, g, h, j, k, l, m, n) + = a :> b :> c :> d:> e :> f :> g :> h :> j :> k :> l :> m :> n :> Nil + listToTuple (a :> b :> c :> d :> e :> f :> g :> h :> j :> k :> l :> m :> n :> Nil) + = (a, b, c, d, e, f, g, h, j, k, l, m, n) + +instance ListTuple + (a1, b1, c1, d1, e1, f1, g1, h1, j1, k1, l1, m1, n1, o1) (a2, b2, c2, d2, e2, f2, g2, h2, j2, k2, l2, m2, n2, o2) + [a1, b1, c1, d1, e1, f1, g1, h1, j1, k1, l1, m1, n1, o1] [a2, b2, c2, d2, e2, f2, g2, h2, j2, k2, l2, m2, n2, o2] + where + tupleToList (a, b, c, d, e, f, g, h, j, k, l, m, n, o) + = a :> b :> c :> d:> e :> f :> g :> h :> j :> k :> l :> m :> n :> o :> Nil + listToTuple (a :> b :> c :> d :> e :> f :> g :> h :> j :> k :> l :> m :> n :> o :> Nil) + = (a, b, c, d, e, f, g, h, j, k, l, m, n, o) + +instance ListTuple + (a1, b1, c1, d1, e1, f1, g1, h1, j1, k1, l1, m1, n1, o1, p1) (a2, b2, c2, d2, e2, f2, g2, h2, j2, k2, l2, m2, n2, o2, p2) + [a1, b1, c1, d1, e1, f1, g1, h1, j1, k1, l1, m1, n1, o1, p1] [a2, b2, c2, d2, e2, f2, g2, h2, j2, k2, l2, m2, n2, o2, p2] + where + tupleToList (a, b, c, d, e, f, g, h, j, k, l, m, n, o, p) + = a :> b :> c :> d:> e :> f :> g :> h :> j :> k :> l :> m :> n :> o :> p :> Nil + listToTuple (a :> b :> c :> d :> e :> f :> g :> h :> j :> k :> l :> m :> n :> o :> p :> Nil) + = (a, b, c, d, e, f, g, h, j, k, l, m, n, o, p) + +instance ListTuple + (a1, b1, c1, d1, e1, f1, g1, h1, j1, k1, l1, m1, n1, o1, p1, q1) (a2, b2, c2, d2, e2, f2, g2, h2, j2, k2, l2, m2, n2, o2, p2, q2) + [a1, b1, c1, d1, e1, f1, g1, h1, j1, k1, l1, m1, n1, o1, p1, q1] [a2, b2, c2, d2, e2, f2, g2, h2, j2, k2, l2, m2, n2, o2, p2, q2] + where + tupleToList (a, b, c, d, e, f, g, h, j, k, l, m, n, o, p, q) + = a :> b :> c :> d:> e :> f :> g :> h :> j :> k :> l :> m :> n :> o :> p :> q :> Nil + listToTuple (a :> b :> c :> d :> e :> f :> g :> h :> j :> k :> l :> m :> n :> o :> p :> q :> Nil) + = (a, b, c, d, e, f, g, h, j, k, l, m, n, o, p, q) + +instance ListTuple + (a1, b1, c1, d1, e1, f1, g1, h1, j1, k1, l1, m1, n1, o1, p1, q1, r1) (a2, b2, c2, d2, e2, f2, g2, h2, j2, k2, l2, m2, n2, o2, p2, q2, r2) + [a1, b1, c1, d1, e1, f1, g1, h1, j1, k1, l1, m1, n1, o1, p1, q1, r1] [a2, b2, c2, d2, e2, f2, g2, h2, j2, k2, l2, m2, n2, o2, p2, q2, r2] + where + tupleToList (a, b, c, d, e, f, g, h, j, k, l, m, n, o, p, q, r) + = a :> b :> c :> d:> e :> f :> g :> h :> j :> k :> l :> m :> n :> o :> p :> q :> r :> Nil + listToTuple (a :> b :> c :> d :> e :> f :> g :> h :> j :> k :> l :> m :> n :> o :> p :> q :> r :> Nil) + = (a, b, c, d, e, f, g, h, j, k, l, m, n, o, p, q, r) + +instance ListTuple + (a1, b1, c1, d1, e1, f1, g1, h1, j1, k1, l1, m1, n1, o1, p1, q1, r1, s1) (a2, b2, c2, d2, e2, f2, g2, h2, j2, k2, l2, m2, n2, o2, p2, q2, r2, s2) + [a1, b1, c1, d1, e1, f1, g1, h1, j1, k1, l1, m1, n1, o1, p1, q1, r1, s1] [a2, b2, c2, d2, e2, f2, g2, h2, j2, k2, l2, m2, n2, o2, p2, q2, r2, s2] + where + tupleToList (a, b, c, d, e, f, g, h, j, k, l, m, n, o, p, q, r, s) + = a :> b :> c :> d:> e :> f :> g :> h :> j :> k :> l :> m :> n :> o :> p :> q :> r :> s :> Nil + listToTuple (a :> b :> c :> d :> e :> f :> g :> h :> j :> k :> l :> m :> n :> o :> p :> q :> r :> s :> Nil) + = (a, b, c, d, e, f, g, h, j, k, l, m, n, o, p, q, r, s) + +type family TupleToList a where + TupleToList () = '[] + TupleToList (a, b) = '[a, b] + TupleToList (a, b, c) = '[a, b, c] + TupleToList (a, b, c, d) = '[a, b, c, d] + TupleToList (a, b, c, d, e) = '[a, b, c, d, e] + TupleToList (a, b, c, d, e, f) = '[a, b, c, d, e, f] + TupleToList (a, b, c, d, e, f, g) = '[a, b, c, d, e, f, g] + TupleToList (a, b, c, d, e, f, g, h) = '[a, b, c, d, e, f, g, h] + TupleToList (a, b, c, d, e, f, g, h, j) = '[a, b, c, d, e, f, g, h, j] + TupleToList (a, b, c, d, e, f, g, h, j, k) = '[a, b, c, d, e, f, g, h, j, k] + TupleToList (a, b, c, d, e, f, g, h, j, k, l) = '[a, b, c, d, e, f, g, h, j, k, l] + TupleToList (a, b, c, d, e, f, g, h, j, k, l, m) = '[a, b, c, d, e, f, g, h, j, k, l, m] + TupleToList (a, b, c, d, e, f, g, h, j, k, l, m, n) = '[a, b, c, d, e, f, g, h, j, k, l, m, n] + TupleToList (a, b, c, d, e, f, g, h, j, k, l, m, n, o) = '[a, b, c, d, e, f, g, h, j, k, l, m, n, o] + TupleToList (a, b, c, d, e, f, g, h, j, k, l, m, n, o, p) = '[a, b, c, d, e, f, g, h, j, k, l, m, n, o, p] + TupleToList (a, b, c, d, e, f, g, h, j, k, l, m, n, o, p, q) = '[a, b, c, d, e, f, g, h, j, k, l, m, n, o, p, q] + TupleToList (a, b, c, d, e, f, g, h, j, k, l, m, n, o, p, q, r) = '[a, b, c, d, e, f, g, h, j, k, l, m, n, o, p, q, r] + TupleToList (a, b, c, d, e, f, g, h, j, k, l, m, n, o, p, q, r, s) = '[a, b, c, d, e, f, g, h, j, k, l, m, n, o, p, q, r, s] + TupleToList a = '[a] diff --git a/src/Data/Generics/Product/Internal/Param.hs b/src/Data/Generics/Product/Internal/Param.hs new file mode 100644 --- /dev/null +++ b/src/Data/Generics/Product/Internal/Param.hs @@ -0,0 +1,68 @@ +{-# LANGUAGE AllowAmbiguousTypes #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TypeApplications #-} +{-# LANGUAGE UndecidableInstances #-} +{-# LANGUAGE ConstraintKinds #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE KindSignatures #-} +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE DataKinds #-} + +module Data.Generics.Product.Internal.Param + ( Context + , derived + ) where + +import Data.Generics.Product.Internal.Types +import Data.Generics.Internal.VL.Traversal + +import GHC.Generics +import Data.Kind +import Data.Generics.Internal.Families +import Data.Generics.Internal.GenericN +import Data.Generics.Internal.Errors +import GHC.TypeLits + +type Context n s t a b + = ( GenericN s + , GenericN t + -- TODO: merge the old 'Changing' code with 'GenericN' + , Defined (Rep s) + (NoGeneric s + '[ 'Text "arising from a generic traversal of the type parameter at position " ':<>: QuoteType n + , 'Text "of type " ':<>: QuoteType a ':<>: 'Text " in " ':<>: QuoteType s + ]) + (() :: Constraint) + , s ~ Infer t (P n b 'PTag) a + , t ~ Infer s (P n a 'PTag) b + , Error ((ArgCount s) <=? n) n (ArgCount s) s + , a ~ ArgAt s n + , b ~ ArgAt t n + , GHasTypes ChGeneric (RepN s) (RepN t) (Param n a) (Param n b) + ) + +derived :: forall n s t a b. Context n s t a b => Traversal s t a b +derived = repIsoN . gtypes_ @ChGeneric . paramIso @n + +-- this could be an iso but since we're operating on a VL traversal it's easier this way. +repIsoN :: (GenericN a, GenericN b) => Traversal a b (RepN a x) (RepN b x) +repIsoN f a = toN <$> f (fromN a) + +-- this could be an iso but since we're operating on a VL traversal it's easier this way. +paramIso :: Traversal (Param n a) (Param n b) a b +paramIso f a = StarParam <$> f (getStarParam a) + +type family Error (b :: Bool) (expected :: Nat) (actual :: Nat) (s :: Type) :: Constraint where + Error 'False _ _ _ + = () + + Error 'True expected actual typ + = TypeError + ( 'Text "Expected a type with at least " + ':<>: 'ShowType (expected + 1) + ':<>: 'Text " parameters, but " + ':$$: 'ShowType typ + ':<>: 'Text " only has " + ':<>: 'ShowType actual + ) diff --git a/src/Data/Generics/Product/Internal/Positions.hs b/src/Data/Generics/Product/Internal/Positions.hs new file mode 100644 --- /dev/null +++ b/src/Data/Generics/Product/Internal/Positions.hs @@ -0,0 +1,194 @@ +{-# LANGUAGE TypeInType #-} +{-# LANGUAGE AllowAmbiguousTypes #-} +{-# LANGUAGE ConstraintKinds #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE FunctionalDependencies #-} +{-# LANGUAGE KindSignatures #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TypeApplications #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE UndecidableInstances #-} + +----------------------------------------------------------------------------- +-- | +-- Module : Data.Generics.Product.Internal.Positions +-- Copyright : (C) 2020 Csongor Kiss +-- License : BSD3 +-- Maintainer : Csongor Kiss +-- Stability : experimental +-- Portability : non-portable +-- +-- Derive positional product type getters and setters generically. +-- +----------------------------------------------------------------------------- + +module Data.Generics.Product.Internal.Positions + ( type (: QuoteType i ':<>: 'Text " of type " ':<>: QuoteType a + ':<>: 'Text " in " ':<>: QuoteType s + ]) + (() :: Constraint) + ) + +class Context (i :: Nat) s t a b | s i -> a, t i -> b, s i b -> t, t i a -> s +instance + ( ErrorUnless i s (0 Context i s t a b + +type Context_ i s t a b = + ( ErrorUnless i s (0 : QuoteType i ':<>: 'Text " of type " ':<>: QuoteType a + ':<>: 'Text " in " ':<>: QuoteType s + ]) + (() :: Constraint) + ) + +derived0 :: forall i s t a b. Context0 i s t a b => Lens s t a b +derived0 = (repIso . coerced @(CRep s) @(CRep t) . glens @(HasTotalPositionPSym i)) +{-# INLINE derived0 #-} + +derived' :: forall i s a. Context' i s a => Lens s s a a +derived' = (repIso . coerced @(CRep s) @(CRep s) . glens @(HasTotalPositionPSym i)) +{-# INLINE derived' #-} + +type family ErrorUnless (i :: Nat) (s :: Type) (hasP :: Bool) :: Constraint where + ErrorUnless i s 'False + = TypeError + ( 'Text "The type " + ':<>: 'ShowType s + ':<>: 'Text " does not contain a field at position " + ':<>: 'ShowType i + ) + + ErrorUnless _ _ 'True + = () + +data HasTotalPositionPSym :: Nat -> (TyFun (Type -> Type) (Maybe Type)) +type instance Eval (HasTotalPositionPSym t) tt = HasTotalPositionP t tt + + +-- We wouldn't need the universal 'x' here if we could express above that +-- forall x. Coercible (cs x) (Rep s x), but this requires quantified +-- constraints +coerced :: forall s t s' t' x. (Coercible t t', Coercible s s') + => Iso (s' x) (t' x) (s x) (t x) +coerced = iso coerce coerce +{-# INLINE coerced #-} + +-------------------------------------------------------------------------------- + +-- | Alias for the kind of the generic rep +type G = Type -> Type + +-------------------------------------------------------------------------------- + +-- | In-order labeling of the generic tree with the field positions +-- +-- We replace the (K1 R a) nodes with (K1 (Pos n) a), where 'n' is the position +-- of the field in question in the data type. This is convenient, because we +-- can reuse all the existing functions as long as they are polymorphic in the +-- first parameter of 'K1'. +type family CRep (a :: Type) :: G where + CRep rep = Fst (Traverse (Rep rep) 1) + +-- | The actual traversal. +-- +-- Might be cleaner if the sum and product parts were separated (as there's +-- and invariant that 'n' should be zero when we're at a sum node, which holds +-- for derived Generic instances (where the sums are strictly above the products)) +type family Traverse (a :: G) (n :: Nat) :: (G, Nat) where + Traverse (M1 mt m s) n + = Traverse1 (M1 mt m) (Traverse s n) + Traverse (l :+: r) n + = '(Fst (Traverse l n) :+: Fst (Traverse r n), n) + Traverse (l :*: r) n + = TraverseProd (:*:) (Traverse l n) r + Traverse (K1 _ p) n + = '(K1 (Pos n) p, n + 1) + Traverse U1 n + = '(U1, n) + +type family Traverse1 (w :: G -> G) (z :: (G, Nat)) :: (G, Nat) where + Traverse1 w '(i, n) = '(w i, n) + +-- | For products, we first traverse the left-hand side, followed by the second +-- using the counter returned by the left traversal. +type family TraverseProd (c :: G -> G -> G) (a :: (G, Nat)) (r :: G) :: (G, Nat) where + TraverseProd w '(i, n) r = Traverse1 (w i) (Traverse r n) + +-------------------------------------------------------------------------------- +-- Utilities + +type family Fst (p :: (a, b)) :: a where + Fst '(a, b) = a + +type family Size f :: Nat where + Size (l :*: r) + = Size l + Size r + Size (l :+: r) + = Min (Size l) (Size r) + Size (D1 meta f) + = Size f + Size (C1 meta f) + = Size f + Size f + = 1 + +type x +-- Stability : experimental +-- Portability : non-portable +-- +-- Structural subtype relationships between product types. +-- +----------------------------------------------------------------------------- + +module Data.Generics.Product.Internal.Subtype + ( Context + , gsmash + , gupcast + ) where + +import Data.Generics.Internal.Families +import Data.Generics.Product.Internal.GLens + +import Data.Kind (Type) +import GHC.Generics +import GHC.TypeLits (Symbol) +import Data.Generics.Internal.Profunctor.Lens (view) + +import GHC.Generics (Generic (Rep)) +import GHC.TypeLits (TypeError, ErrorMessage (..)) +import Data.Kind (Constraint) +import Data.Generics.Internal.Errors + +type Context a b + = ( Generic a + , Generic b + , GSmash (Rep a) (Rep b) + , GUpcast (Rep a) (Rep b) + , CustomError a b + ) + +type family CustomError a b :: Constraint where + CustomError a b = + ( ErrorUnless b a (CollectFieldsOrdered (Rep b) \\ CollectFieldsOrdered (Rep a)) + , Defined (Rep a) + (NoGeneric a '[ 'Text "arising from a generic lens focusing on " ':<>: QuoteType b + , 'Text "as a supertype of " ':<>: QuoteType a + ]) + (() :: Constraint) + , Defined (Rep b) + (NoGeneric b '[ 'Text "arising from a generic lens focusing on " ':<>: QuoteType b + , 'Text "as a supertype of " ':<>: QuoteType a + ]) + (() :: Constraint) + ) + +type family ErrorUnless (sup :: Type) (sub :: Type) (diff :: [Symbol]) :: Constraint where + ErrorUnless _ _ '[] + = () + + ErrorUnless sup sub fs + = TypeError + ( 'Text "The type '" + ':<>: 'ShowType sub + ':<>: 'Text "' is not a subtype of '" + ':<>: 'ShowType sup ':<>: 'Text "'." + ':$$: 'Text "The following fields are missing from '" + ':<>: 'ShowType sub ':<>: 'Text "':" + ':$$: ShowSymbols fs + ) + +-------------------------------------------------------------------------------- +-- * Generic upcasting + +class GUpcast (sub :: Type -> Type) (sup :: Type -> Type) where + gupcast :: sub p -> sup p + +instance (GUpcast sub a, GUpcast sub b) => GUpcast sub (a :*: b) where + gupcast rep = gupcast rep :*: gupcast rep + +instance + GLens' (HasTotalFieldPSym field) sub t + => GUpcast sub (S1 ('MetaSel ('Just field) p f b) (Rec0 t)) where + + gupcast r = M1 (K1 (view (glens @(HasTotalFieldPSym field)) r)) + +instance GUpcast sub sup => GUpcast sub (C1 c sup) where + gupcast = M1 . gupcast + +instance GUpcast sub sup => GUpcast sub (D1 c sup) where + gupcast = M1 . gupcast + +-------------------------------------------------------------------------------- +-- * Generic smashing + +class GSmash sub sup where + gsmash :: sup p -> sub p -> sub p + +instance (GSmash a sup, GSmash b sup) => GSmash (a :*: b) sup where + gsmash rep (a :*: b) = gsmash rep a :*: gsmash rep b + +instance + ( leaf ~ (S1 ('MetaSel ('Just field) p f b) t) + , GSmashLeaf leaf sup (HasTotalFieldP field sup) + ) => GSmash (S1 ('MetaSel ('Just field) p f b) t) sup where + + gsmash = gsmashLeaf @_ @_ @(HasTotalFieldP field sup) + +instance GSmash sub sup => GSmash (C1 c sub) sup where + gsmash sup (M1 sub) = M1 (gsmash sup sub) + +instance GSmash sub sup => GSmash (D1 c sub) sup where + gsmash sup (M1 sub) = M1 (gsmash sup sub) + +class GSmashLeaf sub sup (w :: Maybe Type) where + gsmashLeaf :: sup p -> sub p -> sub p + +instance + GLens' (HasTotalFieldPSym field) sup t + => GSmashLeaf (S1 ('MetaSel ('Just field) p f b) (Rec0 t)) sup ('Just t) where + gsmashLeaf sup _ = M1 (K1 (view (glens @(HasTotalFieldPSym field)) sup)) + +instance GSmashLeaf (S1 ('MetaSel ('Just field) p f b) (Rec0 t)) sup 'Nothing where + gsmashLeaf _ = id + +data HasTotalFieldPSym :: Symbol -> (TyFun (Type -> Type) (Maybe Type)) +type instance Eval (HasTotalFieldPSym sym) tt = HasTotalFieldP sym tt diff --git a/src/Data/Generics/Product/Internal/Typed.hs b/src/Data/Generics/Product/Internal/Typed.hs new file mode 100644 --- /dev/null +++ b/src/Data/Generics/Product/Internal/Typed.hs @@ -0,0 +1,75 @@ +{-# LANGUAGE ConstraintKinds #-} +{-# LANGUAGE AllowAmbiguousTypes #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE KindSignatures #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TypeApplications #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE TypeInType #-} +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE UndecidableInstances #-} + +module Data.Generics.Product.Internal.Typed + ( Context + , derived + ) where + +import Data.Generics.Internal.Families +import Data.Generics.Product.Internal.GLens + +import Data.Kind (Constraint, Type) +import GHC.Generics (Generic (Rep)) +import GHC.TypeLits (TypeError, ErrorMessage (..)) +import Data.Generics.Internal.Profunctor.Lens (Lens) +import Data.Generics.Internal.Profunctor.Iso (repIso) +import Data.Generics.Internal.Errors + +type Context a s = ( Generic s + , ErrorUnlessOne a s (CollectTotalType a (Rep s)) + , Defined (Rep s) + (NoGeneric s '[ 'Text "arising from a generic lens focusing on a field of type " ':<>: QuoteType a]) + (() :: Constraint) + , GLens (HasTotalTypePSym a) (Rep s) (Rep s) a a + ) + +derived :: forall a s. Context a s => Lens s s a a +derived = repIso . glens @(HasTotalTypePSym a) +{-# INLINE derived #-} + +type family ErrorUnlessOne (a :: Type) (s :: Type) (stat :: TypeStat) :: Constraint where + ErrorUnlessOne a s ('TypeStat '[_] '[] '[]) + = TypeError + ( 'Text "The type " + ':<>: 'ShowType s + ':<>: 'Text " does not contain a value of type " + ':<>: 'ShowType a + ) + + ErrorUnlessOne a s ('TypeStat (n ': ns) _ _) + = TypeError + ( 'Text "Not all constructors of the type " + ':<>: 'ShowType s + ':<>: 'Text " contain a field of type " + ':<>: 'ShowType a ':<>: 'Text "." + ':$$: 'Text "The offending constructors are:" + ':$$: ShowSymbols (n ': ns) + ) + + ErrorUnlessOne a s ('TypeStat _ (m ': ms) _) + = TypeError + ( 'Text "The type " + ':<>: 'ShowType s + ':<>: 'Text " contains multiple values of type " + ':<>: 'ShowType a ':<>: 'Text "." + ':$$: 'Text "The choice of value is thus ambiguous. The offending constructors are:" + ':$$: ShowSymbols (m ': ms) + ) + + ErrorUnlessOne _ _ ('TypeStat '[] '[] _) + = () + +data HasTotalTypePSym :: Type -> (TyFun (Type -> Type) (Maybe Type)) +type instance Eval (HasTotalTypePSym t) tt = HasTotalTypeP t tt diff --git a/src/Data/Generics/Product/Internal/Types.hs b/src/Data/Generics/Product/Internal/Types.hs new file mode 100644 --- /dev/null +++ b/src/Data/Generics/Product/Internal/Types.hs @@ -0,0 +1,284 @@ +{-# LANGUAGE PackageImports #-} +{-# LANGUAGE AllowAmbiguousTypes #-} +{-# LANGUAGE ConstraintKinds #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE DefaultSignatures #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE KindSignatures #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE Rank2Types #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TypeApplications #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE UndecidableInstances #-} + +module Data.Generics.Product.Internal.Types where + +import Data.Kind +import Data.Int (Int8, Int16, Int32, Int64) +import Data.Word (Word, Word8, Word16, Word32, Word64) +import qualified Data.Text as T + +import GHC.Generics +import Data.Generics.Internal.GenericN +import GHC.TypeLits +import Data.Generics.Internal.Errors + +import "this" Data.Generics.Internal.VL.Traversal + + +-- | The children of a type are the types of its fields. +-- The 'Children' type family maps a type @a@ to its set of children. +-- +-- This type family is parameterized by a symbol @ch@ (that can be declared as +-- an empty data type). +-- The symbol 'ChGeneric' provides a default definition. You can create new +-- symbols to override the set of children of abstract, non-generic types. +-- +-- The following example declares a @Custom@ symbol to redefine 'Children' +-- for some abstract types from the @time@ library. +-- +-- @ +-- data Custom +-- type instance 'Children' Custom a = ChildrenCustom a +-- +-- type family ChildrenCustom (a :: Type) where +-- ChildrenCustom DiffTime = '[] +-- ChildrenCustom NominalDiffTime = '[] +-- -- Add more custom mappings here. +-- +-- ChildrenCustom a = Children ChGeneric a +-- @ +-- +-- To use this definition, replace 'types' with @'typesUsing' \@Custom@. +type family Children (ch :: Type) (a :: Type) :: [Type] + +-- | The default definition of 'Children'. +-- Primitive types from core libraries have no children, and other types are +-- assumed to be 'Generic'. +data ChGeneric +type instance Children ChGeneric a = ChildrenDefault a + +type family ChildrenDefault (a :: Type) :: [Type] where + ChildrenDefault Char = '[] + ChildrenDefault Double = '[] + ChildrenDefault Float = '[] + ChildrenDefault Integer = '[] + ChildrenDefault Int = '[] + ChildrenDefault Int8 = '[] + ChildrenDefault Int16 = '[] + ChildrenDefault Int32 = '[] + ChildrenDefault Int64 = '[] + ChildrenDefault Word = '[] + ChildrenDefault Word8 = '[] + ChildrenDefault Word16 = '[] + ChildrenDefault Word32 = '[] + ChildrenDefault Word64 = '[] + ChildrenDefault T.Text = '[] + ChildrenDefault (Param n _) = '[] + ChildrenDefault a + = Defined (Rep a) + (NoGeneric a + '[ 'Text "arising from a generic traversal." + , 'Text "Either derive the instance, or define a custom traversal using HasTypesCustom" + ]) + (ChildrenGeneric (Rep a) '[]) + +type family ChildrenGeneric (f :: k -> Type) (cs :: [Type]) :: [Type] where + ChildrenGeneric (M1 _ _ f) cs = ChildrenGeneric f cs + ChildrenGeneric (l :*: r) cs = ChildrenGeneric l (ChildrenGeneric r cs) + ChildrenGeneric (l :+: r) cs = ChildrenGeneric l (ChildrenGeneric r cs) + ChildrenGeneric (Rec0 a) cs = a ': cs + ChildrenGeneric _ cs = cs + +type Interesting (ch :: Type) (a :: Type) (t :: Type) + = Defined_list (Children ch t) (NoChildren ch t) + (IsNothing (Interesting' ch a '[t] (Children ch t))) + +type family NoChildren (ch :: Type) (a :: Type) :: Constraint where + NoChildren ch a = PrettyError + '[ 'Text "No type family instance for " ':<>: QuoteType (Children ch a) + , 'Text "arising from a traversal over " ':<>: QuoteType a + , 'Text "with custom strategy " ':<>: QuoteType ch + ] + + +type family Interesting' (ch :: Type) (a :: Type) (seen :: [Type]) (ts :: [Type]) :: Maybe [Type] where + Interesting' ch _ seen '[] = 'Just seen + Interesting' ch a seen (t ': ts) = + InterestingOr ch a (InterestingUnless ch a seen t (Elem t seen)) ts + +-- Short circuit +-- Note: we only insert 't' to the seen list if it's not already there (which is precisely when `s` is 'False) +type family InterestingUnless + (ch :: Type) (a :: Type) (seen :: [Type]) (t :: Type) (alreadySeen :: Bool) :: + Maybe [Type] where + InterestingUnless ch a seen a _ = 'Nothing + InterestingUnless ch a seen t 'True = 'Just seen + InterestingUnless ch a seen t 'False + = Defined_list (Children ch t) (NoChildren ch t) + (Interesting' ch a (t ': seen) (Children ch t)) + +-- Short circuit +type family InterestingOr + (ch :: Type) (a :: Type) (seen' :: Maybe [Type]) (ts :: [Type]) :: + Maybe [Type] where + InterestingOr ch a 'Nothing _ = 'Nothing + InterestingOr ch a ('Just seen) ts = Interesting' ch a seen ts + +type family Elem a as where + Elem a (a ': _) = 'True + Elem a (_ ': as) = Elem a as + Elem a '[] = 'False + +type family IsNothing a where + IsNothing ('Just _) = 'False + IsNothing 'Nothing = 'True + +-------------------------------------------------------------------------------- + +-------------------------------------------------------------------------------- +-- HasTypes +-------------------------------------------------------------------------------- + +class HasTypes s a where + types_ :: Traversal' s a + + types_ _ = pure + {-# INLINE types_ #-} + +instance + ( HasTypesUsing ChGeneric s s a a + ) => HasTypes s a where + types_ = typesUsing_ @ChGeneric + {-# INLINE types_ #-} + +-------------------------------------------------------------------------------- +data Void +instance {-# OVERLAPPING #-} HasTypes Void a where + types_ _ = pure + +instance {-# OVERLAPPING #-} HasTypes s Void where + types_ _ = pure + +instance {-# OVERLAPPING #-} HasTypesUsing ch Void Void a b where + typesUsing_ _ = pure + +instance {-# OVERLAPPING #-} HasTypesUsing ch s s Void Void where + typesUsing_ _ = pure +-------------------------------------------------------------------------------- + +-------------------------------------------------------------------------------- +-- HasTypesUsing +-------------------------------------------------------------------------------- + +-- | @since 1.2.0.0 +class HasTypesUsing (ch :: Type) s t a b where + typesUsing_ :: Traversal s t a b + +instance {-# OVERLAPPABLE #-} + ( HasTypesOpt ch (Interesting ch a s) s t a b + ) => HasTypesUsing ch s t a b where + typesUsing_ = typesOpt @ch @(Interesting ch a s) + {-# INLINE typesUsing_ #-} + +instance {-# OVERLAPPABLE #-} HasTypesUsing ch a b a b where + typesUsing_ = id + +-- | By adding instances to this class, we can override the default +-- behaviour in an ad-hoc manner. +-- For example: +-- +-- @ +-- instance HasTypesCustom Custom Opaque Opaque String String where +-- typesCustom f (Opaque str) = Opaque <$> f str +-- @ +-- +-- @since 1.2.0.0 +class HasTypesCustom (ch :: Type) s t a b where + -- | This function should never be used directly, only to override + -- the default traversal behaviour. To actually use the custom + -- traversal strategy, see 'typesUsing'. This is because 'typesUsing' does + -- additional optimisations, like ensuring that nodes with no relevant members will + -- not be traversed at runtime. + typesCustom :: Traversal s t a b + +instance {-# OVERLAPPABLE #-} + ( GHasTypes ch (Rep s) (Rep t) a b + , Generic s + , Generic t + -- if there's no Generic instance here, it means we got through the + -- Children check by a user-defined custom strategy. + -- Therefore, we can ignore the missing Generic instance, and + -- instead report a missing HasTypesCustom instance + , Defined (Rep s) + (PrettyError '[ 'Text "No instance " ':<>: QuoteType (HasTypesCustom ch s t a b)]) + (() :: Constraint) + ) => HasTypesCustom ch s t a b where + typesCustom f s = to <$> gtypes_ @ch f (from s) + +-------------------------------------------------------------------------------- +-- Internals +-------------------------------------------------------------------------------- +-- TODO: these should never leak out in error messages + +class HasTypesOpt (ch :: Type) (p :: Bool) s t a b where + typesOpt :: Traversal s t a b + +instance HasTypesCustom ch s t a b => HasTypesOpt ch 'True s t a b where + typesOpt = typesCustom @ch + +instance HasTypesOpt ch 'False s s a b where + typesOpt _ = pure + +-------------------------------------------------------------------------------- +-- TODO: pull out recursion here. + +class GHasTypes ch s t a b where + gtypes_ :: Traversal (s x) (t x) a b + +instance + ( GHasTypes ch l l' a b + , GHasTypes ch r r' a b + ) => GHasTypes ch (l :*: r) (l' :*: r') a b where + gtypes_ f (l :*: r) = (:*:) <$> gtypes_ @ch f l <*> gtypes_ @ch f r + {-# INLINE gtypes_ #-} + +instance + ( GHasTypes ch l l' a b + , GHasTypes ch r r' a b + ) => GHasTypes ch (l :+: r) (l' :+: r') a b where + gtypes_ f (L1 l) = L1 <$> gtypes_ @ch f l + gtypes_ f (R1 r) = R1 <$> gtypes_ @ch f r + {-# INLINE gtypes_ #-} + +instance GHasTypes ch s t a b => GHasTypes ch (M1 m meta s) (M1 m meta t) a b where + gtypes_ f (M1 s) = M1 <$> gtypes_ @ch f s + {-# INLINE gtypes_ #-} + +-- In the recursive case, we invoke 'HasTypesUsing' again, using the +-- same strategy +-- This instance is marked INCOHERENT, because +instance {-# INCOHERENT #-} HasTypesUsing ch s t a b => GHasTypes ch (Rec0 s) (Rec0 t) a b where + gtypes_ f (K1 x) = K1 <$> typesUsing_ @ch f x + {-# INLINE gtypes_ #-} + +-- | The default instance for 'HasTypes' acts as a synonym for +-- 'HasTypesUsing ChGeneric', so in most cases this instance should +-- behave the same as the one above. +-- However, there might be overlapping instances defined for +-- 'HasTypes' directly, in which case we want to prefer those +-- instances (even though the custom instances should always be added to 'HasTypesCustom') +instance {-# OVERLAPPING #-} HasTypes b a => GHasTypes ChGeneric (Rec0 b) (Rec0 b) a a where + gtypes_ f (K1 x) = K1 <$> types_ @b @a f x + {-# INLINE gtypes_ #-} + +instance GHasTypes ch U1 U1 a b where + gtypes_ _ _ = pure U1 + {-# INLINE gtypes_ #-} + +instance GHasTypes ch V1 V1 a b where + gtypes_ _ = pure + {-# INLINE gtypes_ #-} diff --git a/src/Data/Generics/Sum/Internal/Constructors.hs b/src/Data/Generics/Sum/Internal/Constructors.hs new file mode 100644 --- /dev/null +++ b/src/Data/Generics/Sum/Internal/Constructors.hs @@ -0,0 +1,138 @@ +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE AllowAmbiguousTypes #-} +{-# LANGUAGE ConstraintKinds #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE FunctionalDependencies #-} +{-# LANGUAGE KindSignatures #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TypeApplications #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE UndecidableInstances #-} + +----------------------------------------------------------------------------- +-- | +-- Module : Data.Generics.Sum.Internal.Constructors +-- Copyright : (C) 2020 Csongor Kiss +-- License : BSD3 +-- Maintainer : Csongor Kiss +-- Stability : experimental +-- Portability : non-portable +-- +-- Derive constructor-name-based prisms generically. +-- +----------------------------------------------------------------------------- + +module Data.Generics.Sum.Internal.Constructors + ( GAsConstructor (..) + , GAsConstructor' + + , Context' + , Context + , Context_ + , Context0 + + , derived0 + ) where + +import Data.Generics.Internal.Families +import Data.Generics.Internal.Errors +import Data.Generics.Product.Internal.HList + +import GHC.Generics +import GHC.TypeLits (Symbol) +import Data.Kind (Constraint, Type) +import Data.Generics.Internal.Profunctor.Iso +import Data.Generics.Internal.Profunctor.Prism + +import GHC.TypeLits (TypeError, ErrorMessage (..)) + +derived0 :: forall ctor s t a b. Context0 ctor s t a b => Prism s t a b +derived0 = repIso . _GCtor @ctor +{-# INLINE derived0 #-} + +type Context' ctor s a + = ( Context0 ctor s s a a + , ErrorUnless ctor s (HasCtorP ctor (Rep s))) + +class Context (ctor :: Symbol) s t a b | ctor s -> a, ctor t -> b +instance + ( ErrorUnless ctor s (HasCtorP ctor (Rep s)) + , GAsConstructor' ctor (Rep s) a -- TODO: add a test similar to #62 for prisms + , GAsConstructor' ctor (Rep (Indexed s)) a' + , GAsConstructor ctor (Rep s) (Rep t) a b + , t ~ Infer s a' b + , GAsConstructor' ctor (Rep (Indexed t)) b' + , s ~ Infer t b' a + ) => Context ctor s t a b + +class Context_ (ctor :: Symbol) s t a b +instance + ( ErrorUnless ctor s (HasCtorP ctor (Rep s)) + , GAsConstructor' ctor (Rep s) a -- TODO: add a test similar to #62 for prisms + , GAsConstructor' ctor (Rep (Indexed s)) a' + , GAsConstructor ctor (Rep s) (Rep t) a b + , GAsConstructor' ctor (Rep (Indexed t)) b' + , UnifyHead s t + , UnifyHead t s + ) => Context_ ctor s t a b + +type Context0 ctor s t a b + = ( Generic s + , Generic t + , GAsConstructor ctor (Rep s) (Rep t) a b + , Defined (Rep s) + (NoGeneric s '[ 'Text "arising from a generic prism focusing on the " + ':<>: QuoteType ctor ':<>: 'Text " constructor of type " ':<>: QuoteType a + , 'Text "in " ':<>: QuoteType s]) + (() :: Constraint) + ) + +type family ErrorUnless (ctor :: Symbol) (s :: Type) (contains :: Bool) :: Constraint where + ErrorUnless ctor s 'False + = TypeError + ( 'Text "The type " + ':<>: 'ShowType s + ':<>: 'Text " does not contain a constructor named " + ':<>: 'ShowType ctor + ) + + ErrorUnless _ _ 'True + = () +-------------------------------------------------------------------------------- + +-- |As 'AsConstructor' but over generic representations as defined by +-- "GHC.Generics". +class GAsConstructor (ctor :: Symbol) s t a b | ctor s -> a, ctor t -> b where + _GCtor :: Prism (s x) (t x) a b + +type GAsConstructor' ctor s a = GAsConstructor ctor s s a a + +instance + ( GIsList f g as bs + , ListTuple a b as bs + ) => GAsConstructor ctor (M1 C ('MetaCons ctor fixity fields) f) (M1 C ('MetaCons ctor fixity fields) g) a b where + + _GCtor = mIso . glist . tupled + {-# INLINE _GCtor #-} + +instance GSumAsConstructor ctor (HasCtorP ctor l) l r l' r' a b => GAsConstructor ctor (l :+: r) (l' :+: r') a b where + _GCtor = _GSumCtor @ctor @(HasCtorP ctor l) + {-# INLINE _GCtor #-} + +instance GAsConstructor ctor f f' a b => GAsConstructor ctor (M1 D meta f) (M1 D meta f') a b where + _GCtor = mIso . _GCtor @ctor + {-# INLINE _GCtor #-} + +class GSumAsConstructor (ctor :: Symbol) (contains :: Bool) l r l' r' a b | ctor l r -> a, ctor l' r' -> b where + _GSumCtor :: Prism ((l :+: r) x) ((l' :+: r') x) a b + +instance GAsConstructor ctor l l' a b => GSumAsConstructor ctor 'True l r l' r a b where + _GSumCtor = left . _GCtor @ctor + {-# INLINE _GSumCtor #-} + +instance GAsConstructor ctor r r' a b => GSumAsConstructor ctor 'False l r l r' a b where + _GSumCtor = right . _GCtor @ctor + {-# INLINE _GSumCtor #-} diff --git a/src/Data/Generics/Sum/Internal/Subtype.hs b/src/Data/Generics/Sum/Internal/Subtype.hs new file mode 100644 --- /dev/null +++ b/src/Data/Generics/Sum/Internal/Subtype.hs @@ -0,0 +1,132 @@ +{-# LANGUAGE MonoLocalBinds #-} +{-# LANGUAGE ConstraintKinds #-} +{-# LANGUAGE AllowAmbiguousTypes #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE KindSignatures #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TypeApplications #-} +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE TypeSynonymInstances #-} +{-# LANGUAGE UndecidableInstances #-} + +----------------------------------------------------------------------------- +-- | +-- Module : Data.Generics.Sum.Internal.Subtype +-- Copyright : (C) 2020 Csongor Kiss +-- License : BSD3 +-- Maintainer : Csongor Kiss +-- Stability : experimental +-- Portability : non-portable +-- +-- Structural subtype relationships between sum types. +-- +----------------------------------------------------------------------------- + +module Data.Generics.Sum.Internal.Subtype + ( Context + , derived + ) where + +import Data.Generics.Product.Internal.HList +import Data.Generics.Sum.Internal.Typed (GAsType (..)) + +import Data.Kind +import GHC.Generics +import Data.Generics.Internal.Profunctor.Iso +import Data.Generics.Internal.Profunctor.Prism +import Data.Generics.Internal.Families.Has + +type Context sub sup + = ( Generic sub + , Generic sup + , GAsSubtype (Rep sub) (Rep sup) + ) + +derived :: Context sub sup => Prism' sup sub +derived = repIso . _GSub . fromIso repIso +{-# INLINE derived #-} + +-------------------------------------------------------------------------------- + +-- |As 'AsSubtype' but over generic representations as defined by +-- "GHC.Generics". +class GAsSubtype (subf :: Type -> Type) (supf :: Type -> Type) where + _GSub :: Prism' (supf x) (subf x) + +instance + ( GSplash sub sup + , GDowncast sub sup + ) => GAsSubtype sub sup where + _GSub f = prism _GSplash _GDowncast f + {-# INLINE _GSub #-} + +-------------------------------------------------------------------------------- + +class GSplash (sub :: Type -> Type) (sup :: Type -> Type) where + _GSplash :: sub x -> sup x + +instance (GSplash a sup, GSplash b sup) => GSplash (a :+: b) sup where + _GSplash (L1 rep) = _GSplash rep + _GSplash (R1 rep) = _GSplash rep + {-# INLINE _GSplash #-} + +instance + ( GIsList subf subf as as + , ListTuple as' as' as as + , GAsType supf as' + ) => GSplash (C1 meta subf) supf where + _GSplash p = build (_GTyped . fromIso (mIso . glist . tupled)) p + {-# INLINE _GSplash #-} + +instance GSplash sub sup => GSplash (D1 c sub) sup where + _GSplash (M1 m) = _GSplash m + {-# INLINE _GSplash #-} + +-------------------------------------------------------------------------------- + +class GDowncast sub sup where + _GDowncast :: sup x -> Either (sup x) (sub x) + +instance + ( GIsList sup sup as as + , GDowncastC (HasPartialTypeP as sub) sub sup + ) => GDowncast sub (C1 m sup) where + _GDowncast (M1 m) = case _GDowncastC @(HasPartialTypeP as sub) m of + Left _ -> Left (M1 m) + Right r -> Right r + {-# INLINE _GDowncast #-} + +instance (GDowncast sub l, GDowncast sub r) => GDowncast sub (l :+: r) where + _GDowncast (L1 x) = case _GDowncast x of + Left _ -> Left (L1 x) + Right r -> Right r + _GDowncast (R1 x) = case _GDowncast x of + Left _ -> Left (R1 x) + Right r -> Right r + {-# INLINE _GDowncast #-} + +instance GDowncast sub sup => GDowncast sub (D1 m sup) where + _GDowncast (M1 m) = case _GDowncast m of + Left _ -> Left (M1 m) + Right r -> Right r + {-# INLINE _GDowncast #-} + +class GDowncastC (contains :: Bool) sub sup where + _GDowncastC :: sup x -> Either (sup x) (sub x) + +instance GDowncastC 'False sub sup where + _GDowncastC sup = Left sup + {-# INLINE _GDowncastC #-} + +instance + ( GAsType sub subl' + , GIsList sup sup subl subl + , ListTuple subl' subl' subl subl + ) => GDowncastC 'True sub sup where + _GDowncastC sup = Right (build (_GTyped . fromIso (glist . tupled)) sup) + {-# INLINE _GDowncastC #-} + diff --git a/src/Data/Generics/Sum/Internal/Typed.hs b/src/Data/Generics/Sum/Internal/Typed.hs new file mode 100644 --- /dev/null +++ b/src/Data/Generics/Sum/Internal/Typed.hs @@ -0,0 +1,108 @@ +{-# LANGUAGE ConstraintKinds #-} +{-# LANGUAGE AllowAmbiguousTypes #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE KindSignatures #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TypeApplications #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE UndecidableInstances #-} + +----------------------------------------------------------------------------- +-- | +-- Module : Data.Generics.Sum.Internal.Typed +-- Copyright : (C) 2020 Csongor Kiss +-- License : BSD3 +-- Maintainer : Csongor Kiss +-- Stability : experimental +-- Portability : non-portable +-- +-- Derive constructor-field-type-based prisms generically. +-- +----------------------------------------------------------------------------- + +module Data.Generics.Sum.Internal.Typed + ( Context + , derived + , GAsType (..) + ) where + +import Data.Kind +import GHC.Generics + +import GHC.TypeLits (TypeError, ErrorMessage (..), Symbol) +import Data.Generics.Internal.Errors +import Data.Generics.Internal.Families +import Data.Generics.Product.Internal.HList +import Data.Generics.Internal.Profunctor.Iso +import Data.Generics.Internal.Profunctor.Prism + +type Context a s + = ( Generic s + , ErrorUnlessOne a s (CollectPartialType (TupleToList a) (Rep s)) + , GAsType (Rep s) a + , Defined (Rep s) + (NoGeneric s '[ 'Text "arising from a generic prism focusing on a constructor of type " ':<>: QuoteType a]) + (() :: Constraint) + ) + +derived :: Context a s => Prism' s a +derived = repIso . _GTyped +{-# INLINE derived #-} + +type family ErrorUnlessOne (a :: Type) (s :: Type) (ctors :: [Symbol]) :: Constraint where + ErrorUnlessOne _ _ '[_] + = () + + ErrorUnlessOne a s '[] + = TypeError + ( 'Text "The type " + ':<>: 'ShowType s + ':<>: 'Text " does not contain a constructor whose field is of type " + ':<>: 'ShowType a + ) + + ErrorUnlessOne a s cs + = TypeError + ( 'Text "The type " + ':<>: 'ShowType s + ':<>: 'Text " contains multiple constructors whose fields are of type " + ':<>: 'ShowType a ':<>: 'Text "." + ':$$: 'Text "The choice of constructor is thus ambiguous, could be any of:" + ':$$: ShowSymbols cs + ) + +-------------------------------------------------------------------------------- + +-- |As 'AsType' but over generic representations as defined by "GHC.Generics". +class GAsType (f :: Type -> Type) (as :: Type) where + _GTyped :: Prism (f x) (f x) as as + +instance + ( GIsList f f as as + , ListTuple a a as as + ) => GAsType (M1 C meta f) a where + _GTyped = mIso . glist . tupled + {-# INLINE _GTyped #-} + +instance GSumAsType (HasPartialTypeP (TupleToList a) l) l r a => GAsType (l :+: r) a where + _GTyped = _GSumTyped @(HasPartialTypeP (TupleToList a) l) + {-# INLINE _GTyped #-} + +instance GAsType f a => GAsType (M1 D meta f) a where + _GTyped = mIso . _GTyped + {-# INLINE _GTyped #-} + +class GSumAsType (contains :: Bool) l r (a :: Type) where + _GSumTyped :: Prism ((l :+: r) x) ((l :+: r) x) a a + +instance GAsType l a => GSumAsType 'True l r a where + _GSumTyped = left . _GTyped + {-# INLINE _GSumTyped #-} + +instance GAsType r a => GSumAsType 'False l r a where + _GSumTyped = right . _GTyped + {-# INLINE _GSumTyped #-}