diff --git a/ChangeLog.md b/ChangeLog.md new file mode 100644 --- /dev/null +++ b/ChangeLog.md @@ -0,0 +1,3 @@ +# Changelog for barbies + +0.1.0.0 Initial release diff --git a/LICENSE b/LICENSE new file mode 100644 --- /dev/null +++ b/LICENSE @@ -0,0 +1,30 @@ +Copyright Author name here (c) 2018 + +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 Author name here 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/README.md b/README.md new file mode 100644 --- /dev/null +++ b/README.md @@ -0,0 +1,21 @@ +# barbie + +Types that are parametric on unary type-constructors that control +their shapes are like Barbies that can wear different clothes +to become a different doll. This is a common Haskell-idiom. E.g., + +```haskell + +data Barbie f + = Barbie + { name :: f String + , age :: f Int + } + +b1 :: Barbie Last -- Barbie with a monoid structure +b2 :: Barbie (Const a) -- container Barbie +b3 :: Barbie Identity -- Barbie's new clothes + +``` + +This package provides basic classes and abstractions to work with these types and easily transform them. 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/barbies.cabal b/barbies.cabal new file mode 100644 --- /dev/null +++ b/barbies.cabal @@ -0,0 +1,85 @@ +name: barbies +version: 0.1.0.0 +synopsis: Classes for working with types that can change clothes. +description: Types that are parametric on a functor are like Barbies that have an outfit for each role. This package provides the basic abstractions to work with them comfortably. +category: Data-structures +homepage: https://github.com/jcpetruzza/barbies#readme +bug-reports: https://github.com/jcpetruzza/barbies/issues +author: Daniel Gorin +maintainer: jcpetruzza@gmail.com +copyright: 2018 Daniel Gorin +license: BSD3 +license-file: LICENSE +build-type: Simple +cabal-version: >= 1.10 + +extra-source-files: + ChangeLog.md + README.md + +source-repository head + type: git + location: https://github.com/jcpetruzza/barbie + +library + + exposed-modules: + Data.Barbie + Data.Barbie.Constraints + Data.Barbie.Container + Data.Functor.Prod + + Data.Barbie.Internal.Bare + Data.Barbie.Internal.Constraints + Data.Barbie.Internal.Functor + Data.Barbie.Internal.Product + Data.Barbie.Internal.ProofB + Data.Barbie.Internal.Traversable + + other-modules: + Data.Barbie.Internal.Classification + Data.Barbie.Internal.Dicts + Data.Barbie.Internal.Generics + Data.Barbie.Internal.Instances + Data.Barbie.Internal.Tags + Data.Barbie.Internal.Wear + + hs-source-dirs: + src + + build-depends: + base >=4.7 && <5 + + ghc-options: -Wall + + default-language: Haskell2010 + + +test-suite barbies-test + type: exitcode-stdio-1.0 + + main-is: Spec.hs + + other-modules: + Barbies + Clothes + Spec.Bare + Spec.Constraints + Spec.Functor + Spec.Traversable + Spec.Product + Spec.Wrapper + + hs-source-dirs: + test + + ghc-options: -threaded -rtsopts -with-rtsopts=-N -Wall + + build-depends: + barbies + , base >=4.7 && <5 + , QuickCheck + , tasty + , tasty-quickcheck + + default-language: Haskell2010 diff --git a/src/Data/Barbie.hs b/src/Data/Barbie.hs new file mode 100644 --- /dev/null +++ b/src/Data/Barbie.hs @@ -0,0 +1,109 @@ +----------------------------------------------------------------------------- +-- | +-- Module : Data.Barbie +-- +-- A common Haskell idiom is to parameterise a datatype by a type @* -> *@, +-- typically a functor or a GADT. These are like outfits of a Barbie, +-- that turn her into a different doll. E.g. +-- +-- @ +-- data Barbie f +-- = Barbie +-- { name :: f 'String' +-- , age :: f 'Int' +-- } +-- +-- b1 :: Barbie 'Data.Monoid.Last' -- Barbie with a monoid structure +-- b2 :: Barbie ('Data.Functor.Const.Const' a) -- 'Data.Barbie.Container.Container' Barbie +-- b3 :: Barbie 'Data.Functor.Identity.Identity' -- Barbie's new clothes +-- @ +-- +-- This module define the classes to work with these types and easily +-- transform them. They all come with default instances based on +-- `GHC.Generics.Generic`, so using them is as easy as: +-- +-- @ +-- data Barbie f +-- = Barbie +-- { name :: f 'String' +-- , age :: f 'Int' +-- } +-- deriving +-- ( 'GHC.Generics.Generic' +-- , 'FunctorB', 'TraversableB', 'ProductB', 'ConstraintsB', 'ProofB' +-- ) +-- +-- deriving instance 'ConstraintsOf' 'Show' f Barbie => 'Show' Barbie +-- deriving instance 'ConstraintsOf' 'Eq' f Barbie => 'Eq' Barbie +-- @ +-- +-- Sometimes one wants to use @Barbie 'Data.Functor.Identity.Identity'@ +-- and it may feels lik a second-class record type, where one needs to +-- unpack values in each field. For those cases, we can leverage on +-- closed type-families ang get the best of both worlds: +-- +-- @ +-- data 'Bare' +-- +-- type family 'Wear' f a where +-- 'Wear' 'Bare' a = a +-- 'Wear' f a = f a +-- +-- data SignUpForm f +-- = SignUpForm' +-- { username :: 'Wear' f 'String', +-- , password :: 'Wear' f 'String' +-- , mailingOk :: 'Wear' f 'Boolean' +-- } +-- deriving ( ..., 'BareB') +-- +-- type SignUpRaw = SignUpForm 'Maybe' +-- type SignUpData = SignUpForm 'Bare' +-- +-- formData = SignUpForm "jbond" "shaken007" False :: SignUpData +-- @ + + +---------------------------------------------------------------------------- +module Data.Barbie + ( + -- * Functor + FunctorB(bmap) + + -- * Traversable + , TraversableB(btraverse) + , bsequence + + -- * Product + , ProductB(buniq, bprod) + , (/*/), (/*) + , bzip, bunzip, bzipWith, bzipWith3, bzipWith4 + + -- * Bare values + , Wear + , Bare + , BareB(bstrip, bcover) + , bstripFrom + , bcoverWith + + -- * Constraints and proofs of instance + , ConstraintsB(ConstraintsOf, adjProof) + , ProofB(bproof) + + -- * Wrapper + , Barbie(..) + ) + +where + +import Data.Barbie.Internal.Bare(Bare, BareB(..), bstripFrom, bcoverWith, Wear) +import Data.Barbie.Internal.Constraints(ConstraintsB(..)) +import Data.Barbie.Internal.Functor(FunctorB(..)) +import Data.Barbie.Internal.Instances(Barbie(..)) +import Data.Barbie.Internal.ProofB(ProofB(..)) +import Data.Barbie.Internal.Product + ( ProductB(..) + , bzip, bunzip, bzipWith, bzipWith3, bzipWith4 + , (/*/), (/*) + ) +import Data.Barbie.Internal.Traversable(TraversableB(..), bsequence) diff --git a/src/Data/Barbie/Constraints.hs b/src/Data/Barbie/Constraints.hs new file mode 100644 --- /dev/null +++ b/src/Data/Barbie/Constraints.hs @@ -0,0 +1,40 @@ +----------------------------------------------------------------------------- +-- | +-- Module : Data.Barbie +-- +-- Support for operating on Barbie-types with constrained functions. +-- +-- Consider the following function: +-- +-- @ +-- showIt :: 'Show' a => 'Maybe' a -> 'Data.Functor.Const' 'String' a +-- showIt = 'Data.Functor.Const' . 'show' +-- @ +-- +-- We would then like to be able to do: +-- +-- @ +-- 'Data.Barbie.bmap' 'showIt' :: 'Data.Barbie.FunctorB' b => b 'Maybe' -> b ('Data.Functor.Const' 'String') +-- @ +-- +-- This however doesn't work because of the @('Show' a)@ constraint in the +-- the type of @showIt@. +-- +-- This module adds support to overcome this problem. +---------------------------------------------------------------------------- +module Data.Barbie.Constraints + ( -- * Proof of instance + DictOf(..) + , packDict + , requiringDict + + -- * Retrieving proofs + , ConstraintsB(ConstraintsOf) + , ProofB(..) + ) + +where + +import Data.Barbie.Internal.Constraints +import Data.Barbie.Internal.Dicts +import Data.Barbie.Internal.ProofB diff --git a/src/Data/Barbie/Container.hs b/src/Data/Barbie/Container.hs new file mode 100644 --- /dev/null +++ b/src/Data/Barbie/Container.hs @@ -0,0 +1,61 @@ +----------------------------------------------------------------------------- +-- | +-- Module : Data.Barbie.Container +-- +-- We get a container of @a@'s for any Barbie-type when we make it wear a +-- @('Const' a)@ . The 'Container' wrapper gives us the expected +-- instances for a container type. +---------------------------------------------------------------------------- +{-# LANGUAGE DeriveGeneric #-} +{-# LANGUAGE StandaloneDeriving #-} +{-# LANGUAGE UndecidableInstances #-} +module Data.Barbie.Container + ( + Container(..) + ) + +where + +import Data.Barbie +import Data.Bifunctor (first) +import Data.Bitraversable (bitraverse) +import Data.Coerce (coerce) +import Data.Functor.Const +import Data.Functor.Prod (uncurryn) +import GHC.Generics (Generic) + +-- | Wrapper for container-Barbies. +newtype Container b a = + Container { getContainer :: b (Const a) } + deriving (Generic) + +deriving instance Eq (b (Const a)) => Eq (Container b a) +deriving instance Ord (b (Const a)) => Ord (Container b a) + +deriving instance Read (b (Const a)) => Read (Container b a) +deriving instance Show (b (Const a)) => Show (Container b a) + +instance FunctorB b => Functor (Container b) where + fmap f = + Container . (bmap (first f)) . getContainer + +instance TraversableB b => Foldable (Container b) where + foldMap f = + getConst . btraverse (coerce . first f) . getContainer + +instance TraversableB b => Traversable (Container b) where + traverse f = + fmap Container . btraverse (bitraverse f pure) . getContainer + +instance ProductB b => Applicative (Container b) where + pure a + = Container $ buniq (Const a) + + l <*> r + = Container $ bmap (uncurryn appConst) (getContainer l /*/ getContainer r) + where + appConst :: Const (a -> b) x -> Const a x -> Const b x + appConst (Const f) (Const a) + = Const (f a) + + diff --git a/src/Data/Barbie/Internal/Bare.hs b/src/Data/Barbie/Internal/Bare.hs new file mode 100644 --- /dev/null +++ b/src/Data/Barbie/Internal/Bare.hs @@ -0,0 +1,213 @@ +{-# LANGUAGE ConstraintKinds #-} +{-# LANGUAGE DefaultSignatures #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE LambdaCase #-} +{-# LANGUAGE Rank2Types #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE TypeApplications #-} +{-# LANGUAGE TypeOperators #-} +module Data.Barbie.Internal.Bare + ( Wear, Bare + , BareB(..) + , bstripFrom, bcoverWith + + , Gbstrip(..) + , gbstripDefault + , gbcoverDefault + + , CanDeriveGenericInstance + , CanDeriveGenericInstance' + ) + +where + +import Data.Barbie.Internal.Functor (FunctorB(..)) +import Data.Barbie.Internal.Generics +import Data.Barbie.Internal.Tags (I, B) +import Data.Barbie.Internal.Wear +import Data.Functor.Identity (Identity(..)) + +import GHC.Generics +import Unsafe.Coerce (unsafeCoerce) + + +-- | Class of Barbie-types defined using 'Wear' and can therefore +-- have 'Bare' versions. Must satisfy: +-- +-- @ +-- 'bcover' . 'bstrip' = 'id' +-- 'bstrip' . 'bcover' = 'id' +-- @ +class FunctorB b => BareB b where + bstrip :: b Identity -> b Bare + bcover :: b Bare -> b Identity + + default bstrip :: CanDeriveGenericInstance b => b Identity -> b Bare + bstrip = gbstripDefault + + default bcover :: CanDeriveGenericInstance' b => b Bare -> b Identity + bcover = gbcoverDefault + +-- | Generalization of 'bstrip' to arbitrary functors +bstripFrom :: BareB b => (forall a . f a -> a) -> b f -> b Bare +bstripFrom f + = bstrip . bmap (Identity . f) + +-- | Generalization of 'bcover' to arbitrary functors +bcoverWith :: BareB b => (forall a . a -> f a) -> b Bare -> b f +bcoverWith f + = bmap (f . runIdentity) . bcover + +-- | All types that admit a generic FunctorB' instance, and have all +-- their occurrences of 'f' under a 'Wear' admit a generic 'BareB' +-- instance. +type CanDeriveGenericInstance b + = ( Generic (b (Target I)) + , Generic (b (Target B)) + , Gbstrip (Rep (b (Target I))) + , Rep (b (Target B)) ~ Repl (Target I) (Target B) (Rep (b (Target I))) + ) + +type CanDeriveGenericInstance' b + = ( Generic (b (Target I)) + , Generic (b (Target B)) + , Gbcover (Rep (b (Target B))) + , Rep (b (Target I)) ~ Repl (Target B) (Target I) (Rep (b (Target B))) + ) + + +-- | Default implementatio of 'bstrip' based on 'Generic'. +gbstripDefault :: CanDeriveGenericInstance b => b Identity -> b Bare +gbstripDefault b + = unsafeUntargetBarbie @B $ to $ gbstrip $ from (unsafeTargetBarbie @I b) + +-- | Default implementatio of 'bstrip' based on 'Generic'. +gbcoverDefault :: CanDeriveGenericInstance' b => b Bare -> b Identity +gbcoverDefault b + = unsafeUntargetBarbie @I $ to $ gbcover $ from (unsafeTargetBarbie @B b) + + +unsafeTargetBare :: a -> Target (W B) a +unsafeTargetBare = unsafeCoerce + +unsafeUntargetBare :: Target (W B) a -> a +unsafeUntargetBare = unsafeCoerce + + +class Gbstrip rep where + gbstrip :: rep x -> Repl (Target I) (Target B) rep x + +class Gbcover rep where + gbcover :: rep x -> Repl (Target B) (Target I) rep x + +-- ---------------------------------- +-- Trivial cases +-- ---------------------------------- + +instance Gbstrip x => Gbstrip (M1 i c x) where + {-# INLINE gbstrip #-} + gbstrip (M1 x) = M1 (gbstrip x) + +instance Gbstrip V1 where + gbstrip _ = undefined + +instance Gbstrip U1 where + {-# INLINE gbstrip #-} + gbstrip u1 = u1 + +instance (Gbstrip l, Gbstrip r) => Gbstrip (l :*: r) where + {-# INLINE gbstrip #-} + gbstrip (l :*: r) + = (gbstrip l) :*: gbstrip r + +instance (Gbstrip l, Gbstrip r) => Gbstrip (l :+: r) where + {-# INLINE gbstrip #-} + gbstrip = \case + L1 l -> L1 (gbstrip l) + R1 r -> R1 (gbstrip r) + + +instance Gbcover x => Gbcover (M1 i c x) where + {-# INLINE gbcover #-} + gbcover (M1 x) = M1 (gbcover x) + +instance Gbcover V1 where + gbcover _ = undefined + +instance Gbcover U1 where + {-# INLINE gbcover #-} + gbcover u1 = u1 + +instance (Gbcover l, Gbcover r) => Gbcover (l :*: r) where + {-# INLINE gbcover #-} + gbcover (l :*: r) + = (gbcover l) :*: gbcover r + +instance (Gbcover l, Gbcover r) => Gbcover (l :+: r) where + {-# INLINE gbcover #-} + gbcover = \case + L1 l -> L1 (gbcover l) + R1 r -> R1 (gbcover r) + +-- -------------------------------- +-- The interesting cases (gbstrip) +-- -------------------------------- + + +instance {-# OVERLAPPING #-} Gbstrip (K1 R (Target (W I) a)) where + {-# INLINE gbstrip #-} + gbstrip (K1 ia) + = K1 $ unsafeTargetBare $ runIdentity $ unsafeUntarget @(W I) ia + +instance {-# OVERLAPPING #-} BareB b => Gbstrip (K1 R (b (Target I))) where + {-# INLINE gbstrip #-} + gbstrip (K1 bf) + = K1 $ unsafeTargetBarbie @B $ bstrip $ unsafeUntargetBarbie @I bf + +instance {-# OVERLAPPING #-} + ( Functor h + , BareB b + , Repl (Target I) (Target B) (K1 R (h (b (Target I)))) -- shouldn't be + ~ (K1 R (h (b (Target B)))) -- necessary but ghc chokes otherwise + ) + => Gbstrip (K1 R (h (b (Target I)))) where + {-# INLINE gbstrip #-} + gbstrip (K1 hbf) + = K1 (fmap (unsafeTargetBarbie @B . bstrip . unsafeUntargetBarbie @I) hbf) + + +instance (K1 i c) ~ Repl (Target I) (Target B) (K1 i c) => Gbstrip (K1 i c) where + {-# INLINE gbstrip #-} + gbstrip k1 = k1 + + +-- -------------------------------- +-- The interesting cases (gbcover) +-- -------------------------------- + + +instance {-# OVERLAPPING #-} Gbcover (K1 R (Target (W B) a)) where + {-# INLINE gbcover #-} + gbcover (K1 a) + = K1 $ unsafeTarget @(W I) $ Identity $ unsafeUntargetBare a + +instance {-# OVERLAPPING #-} BareB b => Gbcover (K1 R (b (Target B))) where + {-# INLINE gbcover #-} + gbcover (K1 bf) + = K1 $ unsafeTargetBarbie @I $ bcover $ unsafeUntargetBarbie @B bf + +instance {-# OVERLAPPING #-} + ( Functor h + , BareB b + , Repl (Target B) (Target I) (K1 R (h (b (Target B)))) -- shouldn't be + ~ (K1 R (h (b (Target I)))) -- necessary but ghc chokes otherwise + ) + => Gbcover (K1 R (h (b (Target B)))) where + {-# INLINE gbcover #-} + gbcover (K1 hbb) + = K1 (fmap (unsafeTargetBarbie @I . bcover . unsafeUntargetBarbie @B) hbb) + +instance (K1 i c) ~ Repl (Target B) (Target I) (K1 i c) => Gbcover (K1 i c) where + {-# INLINE gbcover #-} + gbcover k1 = k1 diff --git a/src/Data/Barbie/Internal/Classification.hs b/src/Data/Barbie/Internal/Classification.hs new file mode 100644 --- /dev/null +++ b/src/Data/Barbie/Internal/Classification.hs @@ -0,0 +1,46 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE UndecidableInstances #-} +module Data.Barbie.Internal.Classification + ( BarbieType(..) + , GClassifyBarbie + , ClassifyBarbie + ) + +where + +import Data.Barbie.Internal.Generics(Target, RecUsage(..), NonRec(..), RecRep, W) +import Data.Barbie.Internal.Tags(F) + +import GHC.Generics + +data BarbieType + = NoBarbie -- ^ The parameter is never used. + | WearBarbie -- ^ The parameter is used, and always under a 'Wear'. + | NonWearBarbie -- ^ The parameter is used, never under a 'Wear'. + | MixedBarbie -- ^ THe parameter is used, sometimes under a 'Wear', somtimes not. + +type family MergeBarbieType l r where + MergeBarbieType 'NoBarbie r = r + MergeBarbieType l 'NoBarbie = l + + MergeBarbieType 'MixedBarbie _ = 'MixedBarbie + MergeBarbieType _ 'MixedBarbie = 'MixedBarbie + + MergeBarbieType x x = x + MergeBarbieType _l _r = 'MixedBarbie + +type family GClassifyBarbie rep where + GClassifyBarbie (M1 _i _c x) = GClassifyBarbie x + GClassifyBarbie V1 = 'NoBarbie + GClassifyBarbie U1 = 'NoBarbie + GClassifyBarbie (l :*: r) = MergeBarbieType (GClassifyBarbie l) (GClassifyBarbie r) + GClassifyBarbie (l :+: r) = MergeBarbieType (GClassifyBarbie l) (GClassifyBarbie r) + GClassifyBarbie (K1 R (NonRec (Target (W F) a))) = 'WearBarbie + GClassifyBarbie (K1 R (NonRec (Target F a))) = 'NonWearBarbie + GClassifyBarbie (K1 R (NonRec (b (Target F)))) = GClassifyBarbie (Rep (b (Target F))) + GClassifyBarbie (K1 R (RecUsage (b (Target F)))) = 'NoBarbie -- break recursion + GClassifyBarbie (K1 _i _c) = 'NoBarbie + +type ClassifyBarbie b = GClassifyBarbie (RecRep (b (Target F))) diff --git a/src/Data/Barbie/Internal/Constraints.hs b/src/Data/Barbie/Internal/Constraints.hs new file mode 100644 --- /dev/null +++ b/src/Data/Barbie/Internal/Constraints.hs @@ -0,0 +1,234 @@ +{-# LANGUAGE ConstraintKinds #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE DefaultSignatures #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE LambdaCase #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TypeApplications #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE UndecidableInstances #-} +module Data.Barbie.Internal.Constraints + ( ConstraintsB(..) + + , CanDeriveGenericInstance + , ConstraintsOfMatchesGenericDeriv + , GConstraintsOf + , GAdjProof + , gadjProofDefault + + , ConstraintByType + ) + +where + +import Data.Barbie.Internal.Classification (BarbieType(..), ClassifyBarbie, GClassifyBarbie) +import Data.Barbie.Internal.Dicts(DictOf(..), packDict) +import Data.Barbie.Internal.Functor(FunctorB(..)) +import Data.Barbie.Internal.Generics +import Data.Barbie.Internal.Tags(F, PxF) +import Data.Barbie.Internal.Wear(Wear) + +import Data.Functor.Product(Product(..)) +import Data.Kind(Constraint) + +import Data.Proxy + +import GHC.Generics + + +-- | Instances of this class provide means to talk about constraints, +-- both at compile-time, using 'ConstraintsOf' and at run-time, +-- in the form of class instance dictionaries, via 'adjProof'. +-- +-- A manual definition would look like this: +-- +-- @ +-- data T f = A (f 'Int') (f 'String') | B (f 'Bool') (f 'Int') +-- +-- instance 'ConstraintsB' T where +-- type 'ConstraintsOf' c f T +-- = (c (f 'Int'), c (f 'String'), c (f 'Bool')) +-- +-- adjProof t = case t of +-- A x y -> A ('Pair' ('packDict' x) ('packDict' y)) +-- B z w -> B ('Pair' ('packDict' z) ('packDict' w)) +-- @ +-- +-- There is a default implementation of 'ConstraintsOf' for +-- 'Generic' types, so in practice one will simply do: +-- +-- @ +-- derive instance 'Generic' T +-- instance 'ConstraintsB' T +-- @ +class FunctorB b => ConstraintsB b where + -- | @'ConstraintsOf' c f b@ should contain a constraint @c (f x)@ + -- for each @f x@ occurring in @b@. E.g.: + -- + -- @ + -- 'ConstraintsOf' 'Show' f Barbie = ('Show' (f 'String'), 'Show' (f 'Int')) + -- @ + type ConstraintsOf (c :: * -> Constraint) (f :: * -> *) b :: Constraint + type ConstraintsOf c f b = GConstraintsOf c f (RecRep (b (Target F))) + + -- | Adjoint a proof-of-instance to a barbie-type. + adjProof + :: forall c f + . ConstraintsOf c f b + => b f -> b (Product (DictOf c f) f) + + default adjProof + :: forall c f + . ( CanDeriveGenericInstance b + , ConstraintsOfMatchesGenericDeriv c f b + , ConstraintsOf c f b + ) + => b f -> b (Product (DictOf c f) f) + adjProof = gadjProofDefault + +-- | Intuivively, the requirements to have @'ConstraintsB' B@ derived are: +-- +-- * There is an instance of @'Generic' (B f)@ for every @f@ +-- +-- * If @f@ is used as argument to some type in the definition of @B@, it +-- is only on a Barbie-type with a 'ConstraintsB' instance. +type CanDeriveGenericInstance b + = ( Generic (b (Target F)) + , Generic (b (Target PxF)) + , GAdjProof (ClassifyBarbie b) b (RecRep (b (Target F))) + , Rep (b (Target PxF)) ~ Repl' (Target F) (Target PxF) (RecRep (b (Target F))) + ) + +type ConstraintsOfMatchesGenericDeriv c f b + = ( ConstraintsOf c f b ~ GConstraintsOf c f (RecRep (b (Target F))) + , ConstraintsOf c f b ~ ConstraintByType (ClassifyBarbie b) c f (RecRep (b (Target F))) + ) + + +-- =============================================================== +-- Generic derivations +-- =============================================================== + +type family ConstraintByType bt (c :: * -> Constraint) (f :: * -> *) r :: Constraint where + ConstraintByType bt c f (M1 _i _c x) = ConstraintByType bt c f x + ConstraintByType bt c f V1 = () + ConstraintByType bt c f U1 = () + ConstraintByType bt c f (l :*: r) = (ConstraintByType bt c f l, ConstraintByType bt c f r) + ConstraintByType bt c f (l :+: r) = (ConstraintByType bt c f l, ConstraintByType bt c f r) + ConstraintByType 'WearBarbie c f (K1 R (NonRec (Target (W F) a))) = (c (Wear f a), Wear f a ~ f a) + ConstraintByType 'NonWearBarbie c f (K1 R (NonRec (Target F a))) = c (f a) + ConstraintByType bt c f (K1 R (NonRec (b (Target F)))) = ConstraintsOf c f b + ConstraintByType bt c f (K1 R (RecUsage (b (Target F)))) = () -- break recursion + ConstraintByType bt c f (K1 _i _c) = () + +type GConstraintsOf c f r + = ConstraintByType (GClassifyBarbie r) c f r + + +-- | Default implementation of 'adjProof' based on 'Generic'. +gadjProofDefault + :: forall b c f + . ( CanDeriveGenericInstance b + , ConstraintsOfMatchesGenericDeriv c f b + , ConstraintsOf c f b + ) + => b f -> b (Product (DictOf c f) f) +gadjProofDefault b + = unsafeUntargetBarbie @PxF $ to $ + gadjProof pcbf pbt $ fromWithRecAnn (unsafeTargetBarbie @F b) + where + pcbf = Proxy :: Proxy (c (b f)) + pbt = Proxy :: Proxy (ClassifyBarbie b) + + +class GAdjProof (bt :: BarbieType) b rep where + + gadjProof + :: ( ConstraintByType bt c f rep + , GConstraintsOf c f (RecRep (b (Target F))) -- for the recursive case! + ) + => Proxy (c (b f)) + -> Proxy bt + -> rep x + -> Repl' (Target F) (Target PxF) rep x + + +-- ---------------------------------- +-- Trivial cases +-- ---------------------------------- + +instance GAdjProof bt b x => GAdjProof bt b (M1 _i _c x) where + {-# INLINE gadjProof #-} + gadjProof pcbf pbt (M1 x) + = M1 (gadjProof pcbf pbt x) + +instance GAdjProof bt b V1 where + gadjProof _ _ _ = undefined + +instance GAdjProof bt b U1 where + {-# INLINE gadjProof #-} + gadjProof _ _ u1 = u1 + +instance (GAdjProof bt b l, GAdjProof bt b r) => GAdjProof bt b (l :*: r) where + {-# INLINE gadjProof #-} + gadjProof pcbf pbt (l :*: r) + = (gadjProof pcbf pbt l) :*: (gadjProof pcbf pbt r) + +instance (GAdjProof bt b l, GAdjProof bt b r) => GAdjProof bt b (l :+: r) where + {-# INLINE gadjProof #-} + gadjProof pcbf pbt = \case + L1 l -> L1 (gadjProof pcbf pbt l) + R1 r -> R1 (gadjProof pcbf pbt r) + + +-- -------------------------------- +-- The interesting cases +-- -------------------------------- + +instance {-# OVERLAPPING #-} GAdjProof 'WearBarbie b (K1 R (NonRec (Target (W F) a))) where + {-# INLINE gadjProof #-} + gadjProof pcbf _ (K1 (NonRec fa)) + = K1 $ unsafeTarget @(W PxF) (Pair (mkProof pcbf) $ unsafeUntarget @(W F) fa) + where + mkProof :: (c (f a), Wear f a ~ f a) => Proxy (c (b f)) -> DictOf c f a + mkProof _ = packDict + + +instance {-# OVERLAPPING #-} GAdjProof 'NonWearBarbie b (K1 R (NonRec (Target F a))) where + {-# INLINE gadjProof #-} + gadjProof pcbf _ (K1 (NonRec fa)) + = K1 $ unsafeTarget @PxF (Pair (mkProof pcbf) $ unsafeUntarget @F fa) + where + mkProof :: c (f a) => Proxy (c (b f)) -> DictOf c f a + mkProof _ = packDict + + +instance {-# OVERLAPPING #-} + ( CanDeriveGenericInstance b + , bt ~ ClassifyBarbie b + ) + => GAdjProof bt b (K1 R (RecUsage (b (Target F)))) where + {-# INLINE gadjProof #-} + gadjProof pcbf pbt (K1 (RecUsage bf)) + = K1 $ to $ gadjProof pcbf pbt $ fromWithRecAnn bf + +instance {-# OVERLAPPING #-} + ConstraintsB b' + => GAdjProof bt b (K1 R (NonRec (b' (Target F)))) where + {-# INLINE gadjProof #-} + gadjProof pcbf _ (K1 (NonRec bf)) + = K1 $ unsafeTargetBarbie @PxF $ adjProof' pcbf $ unsafeUntargetBarbie @F bf + where + adjProof' + :: ConstraintsOf c f b' + => Proxy (c (b f)) -> b' f -> b' (Product (DictOf c f) f) + adjProof' _ = adjProof + +instance + (K1 i a) ~ Repl' (Target F) (Target PxF) (K1 i (NonRec a)) + => GAdjProof bt b (K1 i (NonRec a)) where + {-# INLINE gadjProof #-} + gadjProof _ _ (K1 (NonRec a)) = K1 a diff --git a/src/Data/Barbie/Internal/Dicts.hs b/src/Data/Barbie/Internal/Dicts.hs new file mode 100644 --- /dev/null +++ b/src/Data/Barbie/Internal/Dicts.hs @@ -0,0 +1,38 @@ +{-# LANGUAGE ConstraintKinds #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE KindSignatures #-} +{-# LANGUAGE Rank2Types #-} +{-# LANGUAGE TypeFamilies #-} +module Data.Barbie.Internal.Dicts + ( DictOf(..) + , packDict + , requiringDict + ) + +where + +import Data.Functor.Classes(Show1(..)) + +-- | @'DictOf' c f a@ is evidence that there exists an instance +-- of @c (f a)@. +data DictOf c f a where + PackedDict :: c (f a) => DictOf c f a + + +instance Eq (DictOf c f a) where + _ == _ = True + +instance Show (DictOf c f a) where + showsPrec _ PackedDict = showString "PackedDict" + +instance Show1 (DictOf c f) where + liftShowsPrec _ _ = showsPrec + +-- | Pack the dictionary associated with an instance. +packDict :: c (f a) => DictOf c f a +packDict = PackedDict + +-- | Turn a constrained-function into an unconstrained one +-- that uses the packed instance dictionary instead. +requiringDict :: (c (f a) => r) -> (DictOf c f a -> r) +requiringDict r = \PackedDict -> r diff --git a/src/Data/Barbie/Internal/Functor.hs b/src/Data/Barbie/Internal/Functor.hs new file mode 100644 --- /dev/null +++ b/src/Data/Barbie/Internal/Functor.hs @@ -0,0 +1,131 @@ +{-# LANGUAGE ConstraintKinds #-} +{-# LANGUAGE DefaultSignatures #-} +{-# LANGUAGE DeriveGeneric #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE LambdaCase #-} +{-# LANGUAGE Rank2Types #-} +{-# LANGUAGE TypeApplications #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE TypeOperators #-} +module Data.Barbie.Internal.Functor + ( FunctorB(..) + + , GFunctorB + , gbmapDefault + , CanDeriveGenericInstance + ) + +where + +import Data.Barbie.Internal.Generics +import Data.Barbie.Internal.Tags (F,G) +import GHC.Generics + +-- | Barbie-types that can be mapped over. Instances of 'FunctorB' should +-- satisfy the following laws: +-- +-- @ +-- 'bmap' 'id' = 'id' +-- 'bmap' f . 'bmap' g = 'bmap' (f . g) +-- @ +-- +-- There is a default 'bmap' implementation for 'Generic' types, so +-- instances can derived automatically. +class FunctorB b where + bmap :: (forall a . f a -> g a) -> b f -> b g + + default bmap + :: CanDeriveGenericInstance b + => (forall a . f a -> g a) -> b f -> b g + bmap = gbmapDefault + +-- | Intuivively, the requirements to have @'FunctorB' B@ derived are: +-- +-- * There is an instance of @'Generic' (B f)@ for every @f@ +-- +-- * If @f@ is used as argument to some type in the definition of @B@, it +-- is only on a Barbie-type with a 'FunctorB' instance. +-- +-- * Recursive usages of @B f@ are allowed to appear as argument to a +-- 'Functor' (e.g. @'Maybe' (B f)') +type CanDeriveGenericInstance b + = ( Generic (b (Target F)) + , Generic (b (Target G)) + , GFunctorB (Rep (b (Target F))) + , Rep (b (Target G)) ~ Repl (Target F) (Target G) (Rep (b (Target F))) + ) + + +-- | Default implementation of 'bmap' based on 'Generic'. +gbmapDefault + :: CanDeriveGenericInstance b + => (forall a . f a -> g a) -> b f -> b g +gbmapDefault f b + = unsafeUntargetBarbie @G $ to $ gbmap f $ from (unsafeTargetBarbie @F b) + + +class GFunctorB b where + gbmap :: (forall a . f a -> g a) -> b x -> Repl (Target F) (Target G) b x + + +-- ---------------------------------- +-- Trivial cases +-- ---------------------------------- + +instance GFunctorB x => GFunctorB (M1 i c x) where + {-# INLINE gbmap #-} + gbmap f (M1 x) = M1 (gbmap f x) + +instance GFunctorB V1 where + gbmap _ _ = undefined + +instance GFunctorB U1 where + {-# INLINE gbmap #-} + gbmap _ u1 = u1 + +instance (GFunctorB l, GFunctorB r) => GFunctorB (l :*: r) where + {-# INLINE gbmap #-} + gbmap f (l :*: r) + = (gbmap f l) :*: gbmap f r + +instance (GFunctorB l, GFunctorB r) => GFunctorB (l :+: r) where + {-# INLINE gbmap #-} + gbmap f = \case + L1 l -> L1 (gbmap f l) + R1 r -> R1 (gbmap f r) + + +-- -------------------------------- +-- The interesting cases +-- -------------------------------- + +instance {-# OVERLAPPING #-} GFunctorB (K1 R (Target (W F) a)) where + {-# INLINE gbmap #-} + gbmap f (K1 fa) + = K1 $ unsafeTarget @(W G) (f $ unsafeUntarget @(W F) fa) + +instance {-# OVERLAPPING #-} GFunctorB (K1 R (Target F a)) where + {-# INLINE gbmap #-} + gbmap f (K1 fa) + = K1 $ unsafeTarget @G (f $ unsafeUntarget @F fa) + +instance {-# OVERLAPPING #-} FunctorB b => GFunctorB (K1 R (b (Target F))) where + {-# INLINE gbmap #-} + gbmap f (K1 bf) + = K1 $ bmap (unsafeTarget @G . f . unsafeUntarget @F) bf + +instance {-# OVERLAPPING #-} + ( Functor h + , FunctorB b + , Repl (Target F) (Target G) (K1 R (h (b (Target F)))) -- shouldn't be + ~ (K1 R (h (b (Target G)))) -- necessary but ghc chokes otherwise + ) + => GFunctorB (K1 R (h (b (Target F)))) where + {-# INLINE gbmap #-} + gbmap f (K1 hbf) + = K1 (fmap (unsafeTargetBarbie @G . bmap f . unsafeUntargetBarbie @F) hbf) + +instance (K1 i c) ~ Repl (Target F) (Target G) (K1 i c) => GFunctorB (K1 i c) where + {-# INLINE gbmap #-} + gbmap _ k1 = k1 diff --git a/src/Data/Barbie/Internal/Generics.hs b/src/Data/Barbie/Internal/Generics.hs new file mode 100644 --- /dev/null +++ b/src/Data/Barbie/Internal/Generics.hs @@ -0,0 +1,112 @@ +----------------------------------------------------------------------------- +-- | +-- Module : Data.Barbie.Internal.Functor +-- +-- GHC is at the momemt unable to derive @'Generic1' b@ for a Barbie-type +-- @b@. Instead, we use a trick by which we use the uninhabited type +-- 'Target' to identify the point where an 'f' occurs. That is, we coerce +-- a @b f@ into a @b 'Target'@, operate on the representation of this type, +-- and finally coerce back to the desired type. +---------------------------------------------------------------------------- +{-# LANGUAGE ExplicitForAll #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE TypeOperators #-} +module Data.Barbie.Internal.Generics + ( Target + , unsafeTargetBarbie + , unsafeUntarget + , unsafeTarget + , unsafeUntargetBarbie + + , W + + , Repl, Repl' + + , RecRep + , RecUsage(..), NonRec(..) + , AnnRec, DeannRec + , toWithRecAnn + , fromWithRecAnn + + ) + +where + +import GHC.Generics +import Unsafe.Coerce (unsafeCoerce) + +-- | We use 'Target' to identify the position in +-- in the generic representation where @f@ is used. +-- This is a hack to overcome the fact that 'Generic1' +-- does not currently work on a type @T f@ whenever +-- if 'f' is applied in 'T', which are all the interesting +-- cases! +data Target (f :: * -> *) a + +unsafeTargetBarbie :: forall t b f . b f -> b (Target t) +unsafeTargetBarbie = unsafeCoerce + +unsafeUntarget :: forall t f a . Target t a -> f a +unsafeUntarget = unsafeCoerce + +unsafeTarget :: forall t f a . f a -> Target t a +unsafeTarget = unsafeCoerce + +unsafeUntargetBarbie :: forall t b f . b (Target t) -> b f +unsafeUntargetBarbie = unsafeCoerce + +type family Repl f g rep where + Repl f g (M1 i c x) = M1 i c (Repl f g x) + Repl f g V1 = V1 + Repl f g U1 = U1 + Repl (Target f) (Target g) (K1 i (Target (W f) a)) = K1 i (Target (W g) a) + Repl f g (K1 i (f a)) = K1 i (g a) + Repl f g (K1 i (b f)) = K1 i (b g) + Repl f g (K1 i (h (b f))) = K1 i (h (b g)) + Repl f g (K1 i c) = K1 i c + Repl f g (l :+: r) = (Repl f g l) :+: (Repl f g r) + Repl f g (l :*: r) = (Repl f g l) :*: (Repl f g r) + + +-- | We use 'RecUsage' to identify the position in the +-- generic representation where the barbie type is used +-- recursively. +newtype RecUsage a + = RecUsage a + +newtype NonRec a + = NonRec a + +type family AnnRec a rep where + AnnRec a (M1 i c x) = M1 i c (AnnRec a x) + AnnRec a V1 = V1 + AnnRec a U1 = U1 + AnnRec a (K1 i a) = K1 i (RecUsage a) + AnnRec a (K1 i a') = K1 i (NonRec a') + AnnRec a (l :*: r) = AnnRec a l :*: AnnRec a r + AnnRec a (l :+: r) = AnnRec a l :+: AnnRec a r + +type family DeannRec rep where + DeannRec (M1 i c x) = M1 i c (DeannRec x) + DeannRec V1 = V1 + DeannRec U1 = U1 + DeannRec (K1 i (RecUsage a)) = K1 i a + DeannRec (K1 i (NonRec a)) = K1 i a + DeannRec (l :*: r) = DeannRec l :*: DeannRec r + DeannRec (l :+: r) = DeannRec l :+: DeannRec r + +fromWithRecAnn :: Generic a => a -> RecRep a x +fromWithRecAnn = unsafeCoerce . from + +toWithRecAnn :: Generic a => RecRep a x -> a +toWithRecAnn = to . unsafeCoerce + +type RecRep a = AnnRec a (Rep a) + +type Repl' f g rep + = Repl f g (DeannRec rep) + + +-- | We use 'W' to identify usagaes of 'Wear' in the generic +-- representation of a barbie-type. +data W (f :: * -> *) a diff --git a/src/Data/Barbie/Internal/Instances.hs b/src/Data/Barbie/Internal/Instances.hs new file mode 100644 --- /dev/null +++ b/src/Data/Barbie/Internal/Instances.hs @@ -0,0 +1,34 @@ +{-# LANGUAGE GeneralizedNewtypeDeriving #-} +{-# LANGUAGE KindSignatures #-} +{-# LANGUAGE UndecidableInstances #-} +module Data.Barbie.Internal.Instances ( Barbie(..) ) + +where + +import Data.Barbie.Internal.Bare +import Data.Barbie.Internal.Constraints +import Data.Barbie.Internal.Dicts +import Data.Barbie.Internal.Functor +import Data.Barbie.Internal.Traversable +import Data.Barbie.Internal.Product +import Data.Barbie.Internal.ProofB + +-- | A wrapper for Barbie-types, providing useful instances. +newtype Barbie b (f :: * -> *) + = Barbie { getBarbie :: b f } + deriving (FunctorB, ProductB, BareB, ConstraintsB, ProofB) + +instance TraversableB b => TraversableB (Barbie b) where + btraverse f = fmap Barbie . btraverse f . getBarbie + + +instance (ProofB b, ConstraintsOf Monoid f b) => Monoid (Barbie b f) where + mempty = bmap mk bproof + where + mk :: DictOf Monoid f a -> f a + mk = requiringDict mempty + + mappend = bzipWith3 mk bproof + where + mk :: DictOf Monoid f a -> f a -> f a -> f a + mk = requiringDict mappend diff --git a/src/Data/Barbie/Internal/Product.hs b/src/Data/Barbie/Internal/Product.hs new file mode 100644 --- /dev/null +++ b/src/Data/Barbie/Internal/Product.hs @@ -0,0 +1,236 @@ +{-# LANGUAGE ConstraintKinds #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE DefaultSignatures #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE Rank2Types #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE TypeApplications #-} +{-# LANGUAGE UndecidableInstances #-} +module Data.Barbie.Internal.Product + ( ProductB(buniq, bprod) + , bzip, bunzip, bzipWith, bzipWith3, bzipWith4 + , (/*/), (/*) + + , CanDeriveGenericInstance, CanDeriveGenericInstance' + , GProductB + , gbprodDefault, gbuniqDefault + ) + +where + +import Data.Barbie.Internal.Functor(FunctorB(..)) +import Data.Barbie.Internal.Generics +import Data.Barbie.Internal.Tags(F, G, FxG) +import Data.Functor.Product (Product(..)) +import Data.Functor.Prod + +import GHC.Generics + + +-- | Barbie-types that can form products, subject to the laws: +-- +-- @ +-- 'bmap' \('Pair' a _) . 'uncurry' . 'bprod' = 'fst' +-- 'bmap' \('Pair' _ b) . 'uncurry' . 'bprod' = 'snd' +-- @ +-- +-- Notice that because of the laws, having an internal product structure is not +-- enough to have a lawful instance. E.g. +-- +-- @ +-- data Ok f = Ok {o1 :: f 'String', o2 :: f 'Int'} -- has an instance +-- data Bad f = Bad{b1 :: f 'String', hiddenFromArg: 'Int'} -- no lawful instance +-- @ +-- +-- Intuitively, the laws for this class require that `b` hides no structure +-- from its argument @f@. Because of this, any @x :: forall a . f a@ +-- determines a unique value of @b f@, witnessed by the 'buniq' method. +-- Formally: +-- +-- @ +-- 'const' ('buniq' x) = 'bmap' ('const' x) +-- @ +-- +-- There is a default implementation of 'bprod' and 'buniq' for 'Generic' types, +-- so instances can derived automatically. +class FunctorB b => ProductB b where + bprod :: b f -> b g -> b (Product f g) + + buniq :: (forall a . f a) -> b f + + default bprod :: CanDeriveGenericInstance b => b f -> b g -> b (Product f g) + bprod = gbprodDefault + + default buniq :: CanDeriveGenericInstance' b => (forall a . f a) -> b f + buniq = gbuniqDefault + + +-- | An alias of 'bprod', since this is like a 'zip' for Barbie-types. +bzip :: ProductB b => b f -> b g -> b (Product f g) +bzip = bprod + +-- | An equivalent of 'unzip' for Barbie-types. +bunzip :: ProductB b => b (Product f g) -> (b f, b g) +bunzip bfg = (bmap (\(Pair a _) -> a) bfg, bmap (\(Pair _ b) -> b) bfg) + +-- | An equivalent of 'Data.List.zipWith' for Barbie-types. +bzipWith :: ProductB b => (forall a. f a -> g a -> h a) -> b f -> b g -> b h +bzipWith f bf bg + = bmap (\(Pair fa ga) -> f fa ga) (bf `bprod` bg) + +-- | An equivalent of 'Data.List.zipWith3' for Barbie-types. +bzipWith3 + :: ProductB b + => (forall a. f a -> g a -> h a -> i a) + -> b f -> b g -> b h -> b i +bzipWith3 f bf bg bh + = bmap (\(Pair (Pair fa ga) ha) -> f fa ga ha) + (bf `bprod` bg `bprod` bh) + + +-- | An equivalent of 'Data.List.zipWith4' for Barbie-types. +bzipWith4 + :: ProductB b + => (forall a. f a -> g a -> h a -> i a -> j a) + -> b f -> b g -> b h -> b i -> b j +bzipWith4 f bf bg bh bi + = bmap (\(Pair (Pair (Pair fa ga) ha) ia) -> f fa ga ha ia) + (bf `bprod` bg `bprod` bh `bprod` bi) + +-- | The requirements to to derive @'ProductB' (B f)@ are more strict than those for +-- 'FunctorB' or 'TraversableB'. Intuitively, we need: +-- +-- * There is an instance of @'Generic' (B f)@ for every @f@ +-- +-- * @B@ has only one constructor. +-- +-- * Every field of @B@' constructor is of the form 'f t'. That is, @B@ has no +-- hidden structure. +type CanDeriveGenericInstance b + = ( Generic (b (Target F)) + , Generic (b (Target G)) + , Generic (b (Target FxG)) + , GProductB (Rep (b (Target F))) + , Rep (b (Target G)) ~ Repl (Target F) (Target G) (Rep (b (Target F))) + , Rep (b (Target FxG)) ~ Repl (Target F) (Target FxG) (Rep (b (Target F))) + ) + +type CanDeriveGenericInstance' b + = ( Generic (b (Target F)) + , GProductB (Rep (b (Target F))) + ) + +-- | Like 'bprod', but returns a binary 'Prod', instead of 'Product', which +-- composes better. +-- +-- See '/*/' for usage. +(/*/) + :: ProductB b => b f -> b g -> b (Prod '[f, g]) +l /*/ r + = bmap (\(Pair f g) -> Cons f (Cons g Unit)) (l `bprod` r) +infixr 4 /*/ + +-- | Similar to '/*/' but one of the sides is already a 'Prod fs'. +-- +-- Note that '/*', '/*/' and 'uncurryn' are meant to be used together: +-- '/*' and '/*/' combine @b f1, b f2...b fn@ into a single product that +-- can then be consumed by using `uncurryn` on an n-ary function. E.g. +-- +-- @ +-- f :: f a -> g a -> h a -> i a +-- +-- 'bmap' ('uncurryn' f) (bf '/*' bg '/*/' bh) +-- @ +(/*) :: ProductB b => b f -> b (Prod fs) -> b (Prod (f ': fs)) +l /* r = + bmap (\(Pair f fs) -> oneTuple f `prod` fs) (l `bprod` r) +infixr 4 /* + +-- ====================================== +-- Generic derivation of instances +-- ====================================== + +-- | Default implementation of 'bprod' based on 'Generic'. +gbprodDefault + :: CanDeriveGenericInstance b + => b f -> b g -> b (Product f g) +gbprodDefault l r + = let l' = from (unsafeTargetBarbie @F l) + r' = from (unsafeTargetBarbie @G r) + in unsafeUntargetBarbie @FxG $ to (gbprod l' r') + +gbuniqDefault + :: CanDeriveGenericInstance' b + => (forall a . f a) -> b f +gbuniqDefault x + = unsafeUntargetBarbie @F $ to (gbuniq x) + +class GProductB b where + gbprod + :: b x + -> Repl (Target F) (Target G) b x + -> Repl (Target F) (Target FxG) b x + + gbuniq + :: (forall a . f a) -> b x + +-- ---------------------------------- +-- Trivial cases +-- ---------------------------------- + +instance GProductB x => GProductB (M1 i c x) where + {-# INLINE gbprod #-} + gbprod (M1 l) (M1 r) = M1 (gbprod l r) + + {-# INLINE gbuniq #-} + gbuniq x = M1 (gbuniq x) + +instance GProductB U1 where + {-# INLINE gbprod #-} + gbprod U1 U1 = U1 + + {-# INLINE gbuniq #-} + gbuniq _ = U1 + +instance(GProductB l, GProductB r) => GProductB (l :*: r) where + {-# INLINE gbprod #-} + gbprod (l1 :*: l2) (r1 :*: r2) + = (l1 `gbprod` r1) :*: (l2 `gbprod` r2) + + {-# INLINE gbuniq #-} + gbuniq x = (gbuniq x :*: gbuniq x) + + +-- -------------------------------- +-- The interesting cases +-- -------------------------------- + +instance {-# OVERLAPPING #-} GProductB (K1 R (Target (W F) a)) where + {-# INLINE gbprod #-} + gbprod (K1 fa) (K1 ga) + = let fxga = Pair (unsafeUntarget @(W F) fa) (unsafeUntarget @(W G) ga) + in K1 (unsafeTarget @(W FxG) fxga) + + {-# INLINE gbuniq #-} + gbuniq x = K1 (unsafeTarget @(W F) x) + +instance {-# OVERLAPPING #-} GProductB (K1 R (Target F a)) where + {-# INLINE gbprod #-} + gbprod (K1 fa) (K1 ga) + = let fxga = Pair (unsafeUntarget @F fa) (unsafeUntarget @G ga) + in K1 (unsafeTarget @FxG fxga) + + {-# INLINE gbuniq #-} + gbuniq x = K1 (unsafeTarget @F x) + + +instance {-# OVERLAPPING #-} ProductB b => GProductB (K1 R (b (Target F))) where + {-# INLINE gbprod #-} + gbprod (K1 bf) (K1 bg) + = let bfxg = unsafeUntargetBarbie @F bf `bprod` unsafeUntargetBarbie @G bg + in K1 (unsafeTargetBarbie @FxG bfxg) + + {-# INLINE gbuniq #-} + gbuniq x = K1 (unsafeTargetBarbie @F (buniq x)) diff --git a/src/Data/Barbie/Internal/ProofB.hs b/src/Data/Barbie/Internal/ProofB.hs new file mode 100644 --- /dev/null +++ b/src/Data/Barbie/Internal/ProofB.hs @@ -0,0 +1,157 @@ +{-# LANGUAGE ConstraintKinds #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE DefaultSignatures #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE KindSignatures #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TypeApplications #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE UndecidableInstances #-} +module Data.Barbie.Internal.ProofB + ( ProofB(..) + + , CanDeriveGenericInstance, ConstraintsOfMatchesGenericDeriv + , GConstraintsOf + , GProof + , gbproofDefault + ) + +where + +import Data.Barbie.Internal.Classification (BarbieType(..), ClassifyBarbie) +import Data.Barbie.Internal.Dicts(DictOf(..), packDict) +import Data.Barbie.Internal.Generics +import Data.Barbie.Internal.Constraints hiding (CanDeriveGenericInstance, ConstraintsOfMatchesGenericDeriv) +import Data.Barbie.Internal.Product(ProductB(..)) +import Data.Barbie.Internal.Tags(P, F) +import Data.Barbie.Internal.Wear(Wear) + +import Data.Proxy + +import GHC.Generics + +-- | Barbie-types with products have a canonical proof of instance. +-- +-- There is a default 'bproof' implementation for 'Generic' types, so +-- instances can derived automatically. +class (ConstraintsB b, ProductB b) => ProofB b where + bproof :: ConstraintsOf c f b => b (DictOf c f) + + default bproof + :: ( CanDeriveGenericInstance b + , ConstraintsOfMatchesGenericDeriv c f b + , ConstraintsOf c f b + ) + => b (DictOf c f) + bproof = gbproofDefault + +-- | Every type that admits a generic instance of 'ProductB' and +-- 'ConstraintsB', has a generic instance of 'ProofB' as well. +type CanDeriveGenericInstance b + = ( Generic (b (Target P)) + , GProof (ClassifyBarbie b) b (RecRep (b (Target F))) + , Rep (b (Target P)) ~ Repl' (Target F) (Target P) (RecRep (b (Target F))) + ) + +type ConstraintsOfMatchesGenericDeriv c f b + = ( ConstraintsOf c f b ~ GConstraintsOf c f (RecRep (b (Target F))) + , ConstraintsOf c f b ~ ConstraintByType (ClassifyBarbie b) c f (RecRep (b (Target F))) + ) + +-- =============================================================== +-- Generic derivations +-- =============================================================== + +-- | Default implementation of 'bproof' based on 'Generic'. +gbproofDefault + :: forall b c f + . ( CanDeriveGenericInstance b + , ConstraintsOfMatchesGenericDeriv c f b + , ConstraintsOf c f b + ) + => b (DictOf c f) +gbproofDefault + = unsafeUntargetBarbie @P $ to $ gbproof pcbf pbt pb + where + pcbf = Proxy :: Proxy (c (b f)) + pbt = Proxy :: Proxy (ClassifyBarbie b) + pb = Proxy :: Proxy (RecRep (b (Target F)) x) + + + +class GProof (bt :: BarbieType) b rep where + gbproof + :: ( ConstraintByType bt c f rep + , GConstraintsOf c f (RecRep (b (Target F))) -- for the recursive case! + ) + => Proxy (c (b f)) + -> Proxy bt + -> Proxy (rep x) + -> Repl' (Target F) (Target P) rep x + + +-- ---------------------------------- +-- Trivial cases +-- ---------------------------------- + +instance GProof bt b x => GProof bt b (M1 _i _c x) where + {-# INLINE gbproof #-} + gbproof pcbf pbt pm1 + = M1 (gbproof pcbf pbt (unM1 <$> pm1)) + +instance GProof bt b U1 where + {-# INLINE gbproof #-} + gbproof _ _ _ = U1 + +instance (GProof bt b l, GProof bt b r) => GProof bt b (l :*: r) where + {-# INLINE gbproof #-} + gbproof pcbf pbt pp + = + gbproof pcbf pbt (left <$> pp) :*: gbproof pcbf pbt (right <$> pp) + where + left (l :*: _) = l + right (_ :*: r) = r + + +-- -------------------------------- +-- The interesting cases +-- -------------------------------- + +instance {-# OVERLAPPING #-} GProof 'WearBarbie b (K1 R (NonRec (Target (W F) a))) where + {-# INLINE gbproof #-} + gbproof pcbf _ _ + = K1 $ unsafeTarget @(W P) (mkProof pcbf) + where + mkProof :: (c (f a), Wear f a ~ f a) => Proxy (c (b f)) -> DictOf c f a + mkProof _ = packDict + +instance {-# OVERLAPPING #-} GProof 'NonWearBarbie b (K1 R (NonRec (Target F a))) where + {-# INLINE gbproof #-} + gbproof pcbf _ _ + = K1 $ unsafeTarget @P (mkProof pcbf) + where + mkProof :: c (f a) => Proxy (c (b f)) -> DictOf c f a + mkProof _ = packDict + +instance {-# OVERLAPPING #-} + ( CanDeriveGenericInstance b + , bt ~ ClassifyBarbie b + ) + => GProof bt b (K1 R (RecUsage (b (Target F)))) where + {-# INLINE gbproof #-} + gbproof pcbf pbt _ + = K1 $ to $ gbproof pcbf pbt pr + where + pr = Proxy :: Proxy (RecRep (b (Target F)) x) + +instance {-# OVERLAPPING #-} + ProofB b' => GProof bt b (K1 R (NonRec (b' (Target F)))) where + {-# INLINE gbproof #-} + gbproof pcbf _ _ + = K1 $ unsafeTargetBarbie @P (proof' pcbf) + where + proof' :: ConstraintsOf c f b' => Proxy (c (b f)) -> b' (DictOf c f) + proof' _ = bproof diff --git a/src/Data/Barbie/Internal/Tags.hs b/src/Data/Barbie/Internal/Tags.hs new file mode 100644 --- /dev/null +++ b/src/Data/Barbie/Internal/Tags.hs @@ -0,0 +1,32 @@ +module Data.Barbie.Internal.Tags + ( F, G, FxG + , P, PxF + , I, B + ) + +where + +-- NB. For type-safety, none of the tags defined here +-- should be exported. + +-- | THIS SHOULD NEVER SHOW UP IN HADDOCK! +data F a + +-- | THIS SHOULD NEVER SHOW UP IN HADDOCK! +data G a + +-- | THIS SHOULD NEVER SHOW UP IN HADDOCK! +data FxG a + + +-- | THIS SHOULD NEVER SHOW UP IN HADDOCK! +data P a + +-- | THIS SHOULD NEVER SHOW UP IN HADDOCK! +data PxF a + +-- | THIS SHOULD NEVER SHOW UP IN HADDOCK! +data I a + +-- | THIS SHOULD NEVER SHOW UP IN HADDOCK! +data B a diff --git a/src/Data/Barbie/Internal/Traversable.hs b/src/Data/Barbie/Internal/Traversable.hs new file mode 100644 --- /dev/null +++ b/src/Data/Barbie/Internal/Traversable.hs @@ -0,0 +1,153 @@ +----------------------------------------------------------------------------- +-- | +-- Module : Data.Barbie.Internal.Functor +---------------------------------------------------------------------------- +{-# LANGUAGE ConstraintKinds #-} +{-# LANGUAGE DefaultSignatures #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE LambdaCase #-} +{-# LANGUAGE Rank2Types #-} +{-# LANGUAGE TypeApplications #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE TypeOperators #-} +module Data.Barbie.Internal.Traversable + ( TraversableB(..) + , bsequence + + , CanDeriveGenericInstance + , GTraversableB + , gbtraverseDefault + ) + +where + +import Data.Barbie.Internal.Functor (FunctorB(..)) +import Data.Barbie.Internal.Generics +import Data.Barbie.Internal.Tags (F,G) +import Data.Functor.Compose (Compose(..)) +import GHC.Generics + + +-- | Barbie-types that can be traversed from left to right. Instances should +-- satisfy the following laws: +-- +-- @ +-- t . 'btraverse' f = 'btraverse' (t . f) -- naturality +-- 'btraverse' 'Data.Functor.Identity' = 'Data.Functor.Identity' -- identity +-- 'btraverse' ('Compose' . 'fmap' g . f) = 'Compose' . 'fmap' ('btraverse' g) . 'btraverse' f -- composition +-- @ +-- +-- There is a default 'btraverse' implementation for 'Generic' types, so +-- instances can derived automatically. +class FunctorB b => TraversableB b where + btraverse :: Applicative t => (forall a . f a -> t (g a)) -> b f -> t (b g) + + default btraverse + :: ( Applicative t, CanDeriveGenericInstance b) + => (forall a . f a -> t (g a)) -> b f -> t (b g) + btraverse = gbtraverseDefault + + + +-- | Evaluate each action in the structure from left to right, +-- and collect the results. +bsequence :: (Applicative f, TraversableB b) => b (Compose f g) -> f (b g) +bsequence + = btraverse getCompose + + +-- | Intuivively, the requirements to have @'TraversableB' B@ derived are: +-- +-- * There is an instance of @'Generic' (B f)@ for every @f@ +-- +-- * If @f@ is used as argument to some type in the definition of @B@, it +-- is only on a Barbie-type with a 'TraversableB' instance. +-- +-- * Recursive usages of @B f@ are allowed to appear as argument to a +-- 'Traversable' (e.g. @'Maybe' (B f)') +type CanDeriveGenericInstance b + = ( Generic (b (Target F)) + , Generic (b (Target G)) + , GTraversableB (Rep (b (Target F))) + , Rep (b (Target G)) ~ Repl (Target F) (Target G) (Rep (b (Target F))) + ) + +-- | Default implementation of 'btraverse' based on 'Generic'. +gbtraverseDefault + :: ( Applicative t, CanDeriveGenericInstance b) + => (forall a . f a -> t (g a)) + -> b f -> t (b g) +gbtraverseDefault f b + = unsafeUntargetBarbie @G . to <$> gbtraverse f (from (unsafeTargetBarbie @F b)) + + + +class GTraversableB b where + gbtraverse + :: Applicative t + => (forall a . f a -> t (g a)) + -> b x -> t (Repl (Target F) (Target G) b x) + +-- ---------------------------------- +-- Trivial cases +-- ---------------------------------- + +instance GTraversableB x => GTraversableB (M1 i c x) where + {-# INLINE gbtraverse #-} + gbtraverse f (M1 x) = M1 <$> gbtraverse f x + +instance GTraversableB V1 where + {-# INLINE gbtraverse #-} + gbtraverse _ _ = undefined + +instance GTraversableB U1 where + {-# INLINE gbtraverse #-} + gbtraverse _ u1 = pure u1 + +instance (GTraversableB l, GTraversableB r) => GTraversableB (l :*: r) where + {-# INLINE gbtraverse #-} + gbtraverse f (l :*: r) + = (:*:) <$> gbtraverse f l <*> gbtraverse f r + +instance (GTraversableB l, GTraversableB r) => GTraversableB (l :+: r) where + {-# INLINE gbtraverse #-} + gbtraverse f = \case + L1 l -> L1 <$> gbtraverse f l + R1 r -> R1 <$> gbtraverse f r + + +-- -------------------------------- +-- The interesting cases +-- -------------------------------- + +instance {-# OVERLAPPING #-} GTraversableB (K1 R (Target (W F) a)) where + {-# INLINE gbtraverse #-} + gbtraverse f (K1 fa) + = K1 . unsafeTarget @(W G) <$> f (unsafeUntarget @(W F) fa) + +instance {-# OVERLAPPING #-} GTraversableB (K1 R (Target F a)) where + {-# INLINE gbtraverse #-} + gbtraverse f (K1 fa) + = K1 . unsafeTarget @G <$> f (unsafeUntarget @F fa) + +instance {-# OVERLAPPING #-} TraversableB b => GTraversableB (K1 R (b (Target F))) where + {-# INLINE gbtraverse #-} + gbtraverse f (K1 bf) + = K1 <$> btraverse (fmap (unsafeTarget @G) . f . unsafeUntarget @F) bf + +instance {-# OVERLAPPING #-} + ( Traversable h + , TraversableB b + , Repl (Target F) (Target G) (K1 R (h (b (Target F)))) -- shouldn't be + ~ (K1 R (h (b (Target G)))) -- necessary but ghc chokes otherwise + ) + => GTraversableB (K1 R (h (b (Target F)))) where + {-# INLINE gbtraverse #-} + gbtraverse f (K1 hbf) + = K1 <$> traverse (fmap (unsafeTargetBarbie @G) . btraverse f . unsafeUntargetBarbie @F) hbf + + +instance (K1 i c) ~ Repl (Target F) (Target G) (K1 i c) => GTraversableB (K1 i c) where + {-# INLINE gbtraverse #-} + gbtraverse _ k1 = pure k1 diff --git a/src/Data/Barbie/Internal/Wear.hs b/src/Data/Barbie/Internal/Wear.hs new file mode 100644 --- /dev/null +++ b/src/Data/Barbie/Internal/Wear.hs @@ -0,0 +1,34 @@ +{-# LANGUAGE TypeFamilies #-} +module Data.Barbie.Internal.Wear + ( Bare, Wear + ) + +where + + +import Data.Barbie.Internal.Generics(Target, W) + +-- | The 'Wear' type-function allows one to define a Barbie-type as +-- +-- @ +-- data B f +-- = B { f1 :: 'Wear' f 'Int' +-- , f2 :: 'Wear' f 'Bool' +-- } +-- @ +-- +-- This way, one can use 'Bare' as a phantom that denotes no functor +-- around the typw: +-- +-- +-- @ +-- B { f1 :: 5, f2 = 'True' } :: B 'Bare' +-- @ +type family Wear f a where + Wear Bare a = a + Wear (Target f) a = Target (W f) a + Wear f a = f a + + +-- | 'Bare' is the only type such that @'Wear' 'Bare' a ~ a'@. +data Bare a diff --git a/src/Data/Functor/Prod.hs b/src/Data/Functor/Prod.hs new file mode 100644 --- /dev/null +++ b/src/Data/Functor/Prod.hs @@ -0,0 +1,250 @@ +----------------------------------------------------------------------------- +-- | +-- Module : Data.Functor.Prod +-- +-- Generalize the standard two-functor 'Product' to the product of +-- @n@-functors. Intuitively, this means: +-- +-- @ +-- 'Product' f g a ~~ (f a, g a) +-- +-- 'Prod' '[] a ~~ Const () a +-- 'Prod' '[f] a ~~ (f a) +-- 'Prod' '[f, g] a ~~ (f a, g a) +-- 'Prod' '[f, g, h] a ~~ (f a, g a, h a) +-- ⋮ +-- @ +---------------------------------------------------------------------------- +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE KindSignatures #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE LambdaCase #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE TypeOperators #-} +module Data.Functor.Prod + ( -- * n-tuples of functors. + Prod(Unit, Cons) + , zeroTuple + , oneTuple + , fromProduct + , toProduct + + -- * Flat product of functor products + , prod + + -- * Lifting functions + , uncurryn + + -- * Type-level helpers + , type (++) + , Curried + ) + +where + +import Control.Applicative(Alternative(..)) +import Data.Functor.Product(Product(..)) +import Data.Functor.Classes(Eq1(..), Ord1(..), Show1(..)) + +import qualified Data.Functor.Classes as FC + +-- | Product of n functors. +data Prod :: [* -> *] -> * -> * where + Unit :: Prod '[] a + Cons :: (f a) -> Prod fs a -> Prod (f ': fs) a + +-- | The unit of the product. +zeroTuple :: Prod '[] a +zeroTuple + = Unit + +-- | Lift a functor to a 1-tuple. +oneTuple :: f a -> Prod '[f] a +oneTuple fa + = Cons fa Unit + +-- | Conversion from a standard 'Product' +fromProduct :: Product f g a -> Prod '[f, g] a +fromProduct (Pair fa ga) + = Cons fa $ Cons ga Unit + +-- | Conversion to a standard 'Product' +toProduct :: Prod '[f, g] a -> Product f g a +toProduct (Cons fa (Cons ga Unit)) + = Pair fa ga + + +-- | Flat product of products. +prod :: Prod ls a -> Prod rs a -> Prod (ls ++ rs) a +l `prod` r = + case l of + Unit -> r + Cons la l' -> Cons la (l' `prod` r) + +-- | Type-level, poly-kinded, list-concatenation. +type family (++) l r :: [k] where + '[] ++ ys = ys + (x ': xs) ++ ys = x ': (xs ++ ys) + +-- -------------------------------------------------------------- +-- Uncurrying of functions +-- -------------------------------------------------------------- + +-- | @'Prod' '[f, g, h] a -> r@ is the type of the uncurried form +-- of a function @f a -> g a -> h a -> r@. 'Curried' moves from +-- the former to the later. E.g. +-- +-- @ +-- 'Curried' ('Prod' '[] a -> r) = r a +-- 'Curried' ('Prod' '[f] a -> r) = f a -> r a +-- 'Curried' ('Prod' '[f, g] a -> r) = f a -> g a -> r a +-- @ +type family Curried t where + Curried (Prod '[] a -> r a) = r a + Curried (Prod (f ': fs) a -> r a) = f a -> Curried (Prod fs a -> r a) + +-- | Like 'uncurry' but using 'Prod' instead of pairs. Can +-- be thought of as a family of functions: +-- +-- @ +-- 'uncurryn' :: r a -> 'Prod' '[] a +-- 'uncurryn' :: (f a -> r a) -> 'Prod' '[f] a +-- 'uncurryn' :: (f a -> g a -> r a) -> 'Prod' '[f, g] a +-- 'uncurryn' :: (f a -> g a -> h a -> r a) -> 'Prod' '[f, g, h] a +-- ⋮ +-- @ +uncurryn :: Curried (Prod fs a -> r a) -> Prod fs a -> r a +uncurryn fun = \case + Unit -> fun + Cons fa fs' -> + let fun' = fun fa + in uncurryn fun' fs' + +-- -------------------------------------------------------------- +-- Instances +-- -------------------------------------------------------------- + +-- | Inductively defined instance: @'Functor' ('Prod' '[])@. +instance Functor (Prod '[]) where + fmap _ Unit = Unit + +-- | Inductively defined instance: @'Functor' ('Prod' (f ': fs))@. +instance (Functor f, Functor (Prod fs)) => Functor (Prod (f ': fs)) where + fmap f (Cons fa fas) + = Cons (fmap f fa) (fmap f fas) + +-- | Inductively defined instance: @'Applicative' ('Prod' '[])@. +instance Applicative (Prod '[]) where + pure _ + = Unit + + Unit <*> Unit + = Unit + +-- | Inductively defined instance: @'Applicative' ('Prod' (f ': fs))@. +instance (Applicative f, Applicative (Prod fs)) => Applicative (Prod (f ': fs)) where + pure a + = Cons (pure a) (pure a) + + Cons f fs <*> Cons a as + = Cons (f <*> a) (fs <*> as) + +-- | Inductively defined instance: @'Alternative' ('Prod' '[])@. +instance Alternative (Prod '[]) where + empty + = Unit + + Unit <|> Unit + = Unit + +-- | Inductively defined instance: @'Alternative' ('Prod' (f ': fs))@. +instance (Alternative f, Alternative (Prod fs)) => Alternative (Prod (f ': fs)) where + empty + = Cons empty empty + + Cons f fs <|> Cons g gs + = Cons (f <|> g) (fs <|> gs) + + +-- NB. There are Monad instances for `Data.Functor.Product`, but I'm not convinced they +-- make much sense. In particular, we seem to get a O(n^2) bind. + +-- | Inductively defined instance: @'Foldable' ('Prod' '[])@. +instance Foldable (Prod '[]) where + foldMap _ = mempty + +-- | Inductively defined instance: @'Foldable' ('Prod' (f ': fs))@. +instance (Foldable f, Foldable (Prod fs)) => Foldable (Prod (f ': fs)) where + foldMap f (Cons fa fas) + = foldMap f fa `mappend` foldMap f fas + +-- | Inductively defined instance: @'Traversable' ('Prod' '[])@. +instance Traversable (Prod '[]) where + traverse _ Unit = pure Unit + +-- | Inductively defined instance: @'Traversable' ('Prod' (f ': fs))@. +instance (Traversable f, Traversable (Prod fs)) => Traversable (Prod (f ': fs)) where + traverse f (Cons fa fas) + = Cons <$> (traverse f fa) <*> (traverse f fas) + +-- | Inductively defined instance: @'Eq1' ('Prod' '[])@. +instance Eq1 (Prod '[]) where + liftEq _ Unit Unit = True + +-- | Inductively defined instance: @'Eq1' ('Prod' (f ': fs))@. +instance (Eq1 f, Eq1 (Prod fs)) => Eq1 (Prod (f ': fs)) where + liftEq eq (Cons l ls) (Cons r rs) + = liftEq eq l r && liftEq eq ls rs + +-- | Inductively defined instance: @'Eq' ('Prod' '[])@. +instance Eq a => Eq (Prod '[] a) where + (==) = FC.eq1 + +-- | Inductively defined instance: @'Eq' ('Prod' (f ': fs))@. +instance (Eq1 f, Eq a, Eq1 (Prod fs)) => Eq (Prod (f ': fs) a) where + (==) = FC.eq1 + +-- | Inductively defined instance: @'Ord1' ('Prod' '[])@. +instance Ord1 (Prod '[]) where + liftCompare _ Unit Unit = EQ + +-- | Inductively defined instance: @'Ord1' ('Prod' (f ': fs))@. +instance (Ord1 f, Ord1 (Prod fs)) => Ord1 (Prod (f ': fs)) where + liftCompare cmp (Cons l ls) (Cons r rs) + = liftCompare cmp l r `mappend` liftCompare cmp ls rs + +-- | Inductively defined instance: @'Ord' ('Prod' '[])@. +instance Ord a => Ord (Prod '[] a) where + compare = FC.compare1 + +-- | Inductively defined instance: @'Ord' ('Prod' (f ': fs))@. +instance (Ord1 f, Ord a, Ord1 (Prod fs)) => Ord (Prod (f ': fs) a) where + compare = FC.compare1 + +-- | Inductively defined instance: @'Show1' ('Prod' '[])@. +instance Show1 (Prod '[]) where + liftShowsPrec _ _ _ Unit = showString "zeroTuple" + +-- | Inductively defined instance: @'Show1' ('Prod' (f ': fs))@. +instance (Show1 f, Show1 (Prod fs)) => Show1 (Prod (f ': fs)) where + liftShowsPrec sp sl d = \case + (Cons fa Unit) -> + showParen (d > 10) $ + showString "oneTuple " . liftShowsPrec sp sl 11 fa + (Cons fa fas) -> + showParen (d > 10) $ + showString "oneTuple " . liftShowsPrec sp sl 11 fa + . showString " `prod` " + . liftShowsPrec sp sl 0 fas + +-- | Inductively defined instance: @'Show' ('Prod' '[])@. +instance Show a => Show (Prod '[] a) where + showsPrec = FC.showsPrec1 + +-- | Inductively defined instance: @'Show' ('Prod' (f ': fs))@. +instance (Show1 f, Show a, Show1 (Prod fs)) => Show (Prod (f ': fs) a) where + showsPrec = FC.showsPrec1 + diff --git a/test/Barbies.hs b/test/Barbies.hs new file mode 100644 --- /dev/null +++ b/test/Barbies.hs @@ -0,0 +1,349 @@ +{-# LANGUAGE DeriveAnyClass #-} +{-# LANGUAGE DeriveGeneric #-} +{-# LANGUAGE DeriveDataTypeable #-} +{-# LANGUAGE EmptyCase #-} +{-# LANGUAGE KindSignatures #-} +{-# LANGUAGE StandaloneDeriving #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE UndecidableInstances #-} +module Barbies + ( Void + + , Record0(..) + , Record1(..) + , Record3(..) + + , Record1W(..) + , Record3W(..) + + , Ignore1(..) + + , Sum3(..) + , Sum3W(..) + + , CompositeRecord(..) + , CompositeRecordW(..) + , SumRec(..) + , SumRecW(..) + , InfRec(..) + , InfRecW(..) + + , NestedF(..) + , NestedFW(..) + ) + +where + +import Data.Barbie + +import Data.Typeable +import GHC.Generics +import Test.Tasty.QuickCheck + +--------------------------------------------------- +-- Trivial Barbies +--------------------------------------------------- + +data Void (f :: * -> *) + deriving + ( Generic, Typeable + , FunctorB, TraversableB, ConstraintsB, BareB + ) + +instance Eq (Void f) where (==) v = case v of +instance Show (Void f) where showsPrec _ v = case v of + + +---------------------------------------------------- +-- Product Barbies +---------------------------------------------------- + +data Record0 (f :: * -> *) + = Record0 + deriving + ( Generic, Typeable + , Eq, Show + , FunctorB, TraversableB, ProductB, ConstraintsB, ProofB, BareB + ) + +instance Arbitrary (Record0 f) where arbitrary = pure Record0 + + +data Record1 f + = Record1 { rec1_f1 :: f Int } + deriving + ( Generic, Typeable + , FunctorB, TraversableB, ProductB, ConstraintsB, ProofB + ) + +deriving instance ConstraintsOf Show f Record1 => Show (Record1 f) +deriving instance ConstraintsOf Eq f Record1 => Eq (Record1 f) + +instance ConstraintsOf Arbitrary f Record1 => Arbitrary (Record1 f) where + arbitrary = Record1 <$> arbitrary + + +data Record1W f + = Record1W { rec1w_f1 :: Wear f Int } + deriving + ( Generic, Typeable + , FunctorB, TraversableB, ProductB, ConstraintsB, ProofB + , BareB + ) + +deriving instance ConstraintsOf Show f Record1W => Show (Record1W f) +deriving instance ConstraintsOf Eq f Record1W => Eq (Record1W f) + +instance ConstraintsOf Arbitrary f Record1W => Arbitrary (Record1W f) where + arbitrary = Record1W <$> arbitrary + + + +data Record3 f + = Record3 + { rec3_f1 :: f Int + , rec3_f2 :: f Bool + , rec3_f3 :: f Char + } + deriving + ( Generic, Typeable + , FunctorB, TraversableB, ProductB, ConstraintsB, ProofB + ) + +deriving instance ConstraintsOf Show f Record3 => Show (Record3 f) +deriving instance ConstraintsOf Eq f Record3 => Eq (Record3 f) + +instance ConstraintsOf Arbitrary f Record3 => Arbitrary (Record3 f) where + arbitrary = Record3 <$> arbitrary <*> arbitrary <*> arbitrary + + +data Record3W f + = Record3W + { rec3w_f1 :: Wear f Int + , rec3w_f2 :: Wear f Bool + , rec3w_f3 :: Wear f Char + } + deriving + ( Generic, Typeable + , FunctorB, TraversableB, ProductB, ConstraintsB, ProofB + , BareB + ) + +deriving instance ConstraintsOf Show f Record3W => Show (Record3W f) +deriving instance ConstraintsOf Eq f Record3W => Eq (Record3W f) + +instance ConstraintsOf Arbitrary f Record3W => Arbitrary (Record3W f) where + arbitrary = Record3W <$> arbitrary <*> arbitrary <*> arbitrary + + +----------------------------------------------------- +-- Bad products +----------------------------------------------------- + +data Ignore1 (f :: * -> *) + = Ignore1 { ign1_f1 :: Int } + deriving + ( Generic, Typeable + , Eq, Show + , FunctorB, TraversableB, ConstraintsB + ) + +instance Arbitrary (Ignore1 f) where arbitrary = Ignore1 <$> arbitrary + + +----------------------------------------------------- +-- Sums +----------------------------------------------------- + +data Sum3 f + = Sum3_0 + | Sum3_1 (f Int) + | Sum3_2 (f Int) (f Bool) + deriving + ( Generic, Typeable + , FunctorB, TraversableB, ConstraintsB + ) + +deriving instance ConstraintsOf Show f Sum3 => Show (Sum3 f) +deriving instance ConstraintsOf Eq f Sum3 => Eq (Sum3 f) + +instance ConstraintsOf Arbitrary f Sum3 => Arbitrary (Sum3 f) where + arbitrary + = oneof + [ pure Sum3_0 + , Sum3_1 <$> arbitrary + , Sum3_2 <$> arbitrary <*> arbitrary + ] + +data Sum3W f + = Sum3W_0 + | Sum3W_1 (Wear f Int) + | Sum3W_2 (Wear f Int) (Wear f Bool) + deriving + ( Generic, Typeable + , FunctorB, TraversableB, ConstraintsB + , BareB + ) + +deriving instance ConstraintsOf Show f Sum3W => Show (Sum3W f) +deriving instance ConstraintsOf Eq f Sum3W => Eq (Sum3W f) + +instance ConstraintsOf Arbitrary f Sum3W => Arbitrary (Sum3W f) where + arbitrary + = oneof + [ pure Sum3W_0 + , Sum3W_1 <$> arbitrary + , Sum3W_2 <$> arbitrary <*> arbitrary + ] + + +----------------------------------------------------- +-- Composite and recursive +----------------------------------------------------- + +data CompositeRecord f + = CompositeRecord + { crec_f1 :: f Int + , crec_F2 :: f Bool + , crec_f3 :: Record3 f + , crec_f4 :: Record1 f + } + deriving + ( Generic, Typeable + , FunctorB, TraversableB, ProductB, ConstraintsB, ProofB + ) + +deriving instance ConstraintsOf Show f CompositeRecord => Show (CompositeRecord f) +deriving instance ConstraintsOf Eq f CompositeRecord => Eq (CompositeRecord f) + +instance ConstraintsOf Arbitrary f CompositeRecord => Arbitrary (CompositeRecord f) where + arbitrary + = CompositeRecord <$> arbitrary <*> arbitrary <*> arbitrary <*> arbitrary + +data CompositeRecordW f + = CompositeRecordW + { crecw_f1 :: Wear f Int + , crecw_F2 :: Wear f Bool + , crecw_f3 :: Record3W f + , crecw_f4 :: Record1W f + } + deriving + ( Generic, Typeable + , FunctorB, TraversableB, ProductB, ConstraintsB, ProofB + , BareB + ) + +deriving instance ConstraintsOf Show f CompositeRecordW => Show (CompositeRecordW f) +deriving instance ConstraintsOf Eq f CompositeRecordW => Eq (CompositeRecordW f) + +instance ConstraintsOf Arbitrary f CompositeRecordW => Arbitrary (CompositeRecordW f) where + arbitrary + = CompositeRecordW <$> arbitrary <*> arbitrary <*> arbitrary <*> arbitrary + + +data SumRec f + = SumRec_0 + | SumRec_1 (f Int) + | SumRec_2 (f Int) (SumRec f) + deriving + ( Generic, Typeable + , FunctorB, TraversableB, ConstraintsB + ) + +deriving instance ConstraintsOf Show f SumRec => Show (SumRec f) +deriving instance ConstraintsOf Eq f SumRec => Eq (SumRec f) + +instance ConstraintsOf Arbitrary f SumRec => Arbitrary (SumRec f) where + arbitrary + = oneof + [ pure SumRec_0 + , SumRec_1 <$> arbitrary + , SumRec_2 <$> arbitrary <*> arbitrary + ] + +data SumRecW f + = SumRecW_0 + | SumRecW_1 (Wear f Int) + | SumRecW_2 (Wear f Int) (SumRecW f) + deriving + ( Generic, Typeable + , FunctorB, TraversableB, ConstraintsB + , BareB + ) + +deriving instance ConstraintsOf Show f SumRecW => Show (SumRecW f) +deriving instance ConstraintsOf Eq f SumRecW => Eq (SumRecW f) + +instance ConstraintsOf Arbitrary f SumRecW => Arbitrary (SumRecW f) where + arbitrary + = oneof + [ pure SumRecW_0 + , SumRecW_1 <$> arbitrary + , SumRecW_2 <$> arbitrary <*> arbitrary + ] + + +data InfRec f + = InfRec { ir_1 :: f Int, ir_2 :: InfRec f } + deriving + ( Generic, Typeable + , FunctorB, TraversableB, ProductB, ConstraintsB, ProofB + ) + +deriving instance ConstraintsOf Show f InfRec => Show (InfRec f) +deriving instance ConstraintsOf Eq f InfRec => Eq (InfRec f) + +data InfRecW f + = InfRecW { irw_1 :: Wear f Int, irw_2 :: InfRecW f } + deriving + ( Generic, Typeable + , FunctorB, TraversableB, ProductB, ConstraintsB, ProofB + , BareB + ) + +deriving instance ConstraintsOf Show f InfRecW => Show (InfRecW f) +deriving instance ConstraintsOf Eq f InfRecW => Eq (InfRecW f) + + +----------------------------------------------------- +-- Nested under functors +----------------------------------------------------- + +data NestedF f + = NestedF + { npf_1 :: f Int + , npf_2 :: [Record3 f] + , npf_3 :: Maybe (Sum3 f) + , npf_4 :: Maybe (NestedF f) + } + deriving + ( Generic, Typeable + , FunctorB, TraversableB + ) + +deriving instance (Show (f Int), Show (Record3 f), Show (Sum3 f)) => Show (NestedF f) +deriving instance (Eq (f Int), Eq (Record3 f), Eq (Sum3 f)) => Eq (NestedF f) + +instance (Arbitrary (f Int), ConstraintsOf Arbitrary f Record3, ConstraintsOf Arbitrary f Sum3) => Arbitrary (NestedF f) where + arbitrary = NestedF <$> arbitrary <*> arbitrary <*> arbitrary <*> arbitrary + + +data NestedFW f + = NestedFW + { npfw_1 :: Wear f Int + , npfw_2 :: [Record3W f] + , npfw_3 :: Maybe (Sum3W f) + , npfw_4 :: Maybe (NestedFW f) + } + deriving + ( Generic, Typeable + , FunctorB, TraversableB + , BareB + -- , ConstraintsB + ) + +deriving instance (Wear f Int ~ f Int, Show (f Int), Show (Record3W f), Show (Sum3W f)) => Show (NestedFW f) +deriving instance (Wear f Int ~ f Int, Eq (f Int), Eq (Record3W f), Eq (Sum3W f)) => Eq (NestedFW f) + +instance (Wear f Int ~ f Int, Wear f Bool ~ f Bool, Wear f Char ~ f Char, Arbitrary (f Int), Arbitrary (f Bool), Arbitrary (f Char)) => Arbitrary (NestedFW f) where + arbitrary = NestedFW <$> arbitrary <*> arbitrary <*> arbitrary <*> arbitrary diff --git a/test/Clothes.hs b/test/Clothes.hs new file mode 100644 --- /dev/null +++ b/test/Clothes.hs @@ -0,0 +1,192 @@ +{-# LANGUAGE DeriveDataTypeable #-} +{-# LANGUAGE GeneralizedNewtypeDeriving #-} +{-# LANGUAGE LambdaCase #-} +{-# LANGUAGE Rank2Types #-} +module Clothes + +where + +import Prelude hiding ((.), id) + +import Control.Category +import Data.Functor.Identity +import qualified Data.List.NonEmpty as NE +import Data.Typeable + +import Test.Tasty.QuickCheck + +data UnitF a = UnitF deriving(Eq, Show, Typeable) + +data F a = F [a] + deriving(Eq, Show, Typeable) + +data G a = NoG | G1 a | Gn [a] + deriving(Eq, Show, Typeable) + +data H a = NoH1 | NoH2 | H1 [a] | H2 [a] | H3 [a] + deriving(Eq, Show, Typeable) + +data I a = NoI1 | NoI2 | NoI3 | I1 a | I2 (a,a) + deriving(Eq, Show, Typeable) + + +instance Arbitrary a => Arbitrary (F a) where + arbitrary = F <$> arbitrary + +instance Arbitrary a => Arbitrary (G a) where + arbitrary = oneof + [ pure NoG + , G1 <$> arbitrary + , Gn <$> arbitrary + ] + +instance Arbitrary a => Arbitrary (H a) where + arbitrary = oneof + [ pure NoH1 + , pure NoH2 + , H1 <$> arbitrary + , H2 <$> arbitrary + , H3 <$> arbitrary + ] + +instance Arbitrary a => Arbitrary (I a) where + arbitrary = oneof + [ pure NoI1 + , pure NoI2 + , pure NoI3 + , I1 <$> arbitrary + , I2 <$> arbitrary + ] + +newtype NatTransf f g + = NatTransf {applyNat :: (forall a . f a -> g a)} + + +instance Category NatTransf where + id = NatTransf id + f . g = NatTransf (applyNat f . applyNat g) + +point :: (forall a . a -> f a) -> NatTransf Identity f +point mkPoint + = NatTransf (\(Identity a) -> mkPoint a) + +unit :: (forall a . f a) -> NatTransf UnitF f +unit u + = NatTransf (\UnitF -> u) + +headF :: NatTransf NE.NonEmpty Identity +headF + = NatTransf (\(a NE.:| _) -> Identity a) + +terminal :: NatTransf f UnitF +terminal + = NatTransf (const UnitF) + + +instance (ArbitraryF f, ArbitraryF g) => Arbitrary (NatTransf f g) where + arbitrary + = do fromList <- arbitraryf + pure (fromList . flattenf) + + +class ArbitraryF f where + arbitraryf :: Gen (NatTransf [] f) + flattenf :: NatTransf f [] + + +instance ArbitraryF F where + arbitraryf + = pure $ NatTransf F + + flattenf + = NatTransf (\(F as) -> as) + + +instance ArbitraryF G where + arbitraryf + = mkArbitraryf + [unit NoG] + [point G1 , point (Gn . pure)] + [NatTransf (Gn . NE.toList)] + + flattenf + = NatTransf $ \case + NoG -> [] + G1 a -> [a] + Gn as -> as + + +instance ArbitraryF H where + arbitraryf + = mkArbitraryf + [unit NoH1, unit NoH2] + [point (H1 . pure), point (H2 . pure)] + [ NatTransf (H1 . NE.toList) + , NatTransf (H2 . NE.toList) + , NatTransf (H2 . NE.toList) + ] + + flattenf + = NatTransf $ \case + NoH1 -> [] + NoH2 -> [] + H1 as -> as + H2 as -> as + H3 as -> as + +instance ArbitraryF I where + arbitraryf + = mkArbitraryf + [unit NoI1, unit NoI2, unit NoI3] + [point I1, NatTransf (\(Identity a) -> I2 (a, a))] + [ NatTransf mkI2 ] + where + mkI2 = \case + a NE.:| [] -> I2 (a, a) + a NE.:| (b:_) -> I2 (a, b) + + flattenf + = NatTransf $ \case + NoI1 -> [] + NoI2 -> [] + NoI3 -> [] + I1 a -> [a] + I2 (a,b) -> [a,b] + +mkArbitraryf + :: [NatTransf UnitF f] + -> [NatTransf Identity f] + -> [NatTransf NE.NonEmpty f] + -> Gen (NatTransf [] f) +mkArbitraryf us is ls + = do let nullary = us + unary = is ++ map (. terminal) nullary + nary = ls ++ map (. headF) unary + build <$> elements nullary <*> elements unary <*> elements nary + where + build u i l + = NatTransf $ \case + [] -> applyNat u UnitF + [a] -> applyNat i (Identity a) + a:as -> applyNat l (a NE.:| as) + +newtype FG + = FG (NatTransf F G) + deriving (Arbitrary) + +newtype GH + = GH (NatTransf G H) + deriving (Arbitrary) + +newtype HI + = HI (NatTransf H I) + deriving (Arbitrary) + +instance Show FG + where show _ = " G>" + +instance Show GH + where show _ = " H>" + +instance Show HI + where show _ = " I>" diff --git a/test/Spec.hs b/test/Spec.hs new file mode 100644 --- /dev/null +++ b/test/Spec.hs @@ -0,0 +1,128 @@ +{-# LANGUAGE TypeApplications #-} +import Test.Tasty (defaultMain, testGroup) + +import qualified Spec.Bare as Bare +import qualified Spec.Constraints as Constraints +import qualified Spec.Functor as Functor +import qualified Spec.Product as Product +import qualified Spec.Traversable as Traversable +import qualified Spec.Wrapper as Wrapper + + +import Barbies + +main :: IO () +main + = defaultMain $ + testGroup "Tests" + [ testGroup "Functor Laws" + [ Functor.laws @Record0 + , Functor.laws @Record1 + , Functor.laws @Record3 + + , Functor.laws @Record1W + , Functor.laws @Record3W + + , Functor.laws @Ignore1 + + , Functor.laws @Sum3 + , Functor.laws @SumRec + + , Functor.laws @Sum3W + , Functor.laws @SumRecW + + , Functor.laws @CompositeRecord + , Functor.laws @NestedF + + , Functor.laws @CompositeRecordW + ] + + , testGroup "Traversable Laws" + [ Traversable.laws @Record0 + , Traversable.laws @Record1 + , Traversable.laws @Record3 + + , Traversable.laws @Record1W + , Traversable.laws @Record3W + + , Traversable.laws @Ignore1 + + , Traversable.laws @Sum3 + , Traversable.laws @SumRec + + , Traversable.laws @Sum3W + , Traversable.laws @SumRecW + + , Traversable.laws @CompositeRecord + , Traversable.laws @NestedF + + , Traversable.laws @CompositeRecordW + ] + + , testGroup "Product Laws" + [ Product.laws @Record0 + , Product.laws @Record1 + , Product.laws @Record3 + , Product.laws @CompositeRecord + + , Product.laws @Record1W + , Product.laws @Record3W + , Product.laws @CompositeRecordW + ] + + , testGroup "Uniq Laws" + [ Product.uniqLaws @Record0 + , Product.uniqLaws @Record1 + , Product.uniqLaws @Record3 + , Product.uniqLaws @CompositeRecord + + , Product.uniqLaws @Record1W + , Product.uniqLaws @Record3W + , Product.uniqLaws @CompositeRecordW + ] + + , testGroup "adjProof projection" + [ Constraints.lawAdjProofPrj @Record0 + , Constraints.lawAdjProofPrj @Record1 + , Constraints.lawAdjProofPrj @Record3 + + , Constraints.lawAdjProofPrj @Record1W + , Constraints.lawAdjProofPrj @Record3W + + + , Constraints.lawAdjProofPrj @Ignore1 + + , Constraints.lawAdjProofPrj @Sum3 + , Constraints.lawAdjProofPrj @SumRec + + , Constraints.lawAdjProofPrj @Sum3W + , Constraints.lawAdjProofPrj @SumRecW + + , Constraints.lawAdjProofPrj @CompositeRecord + , Constraints.lawAdjProofPrj @CompositeRecordW + ] + + , testGroup "bproof projection" + [ Constraints.lawProofEquivPrj @Record0 + , Constraints.lawProofEquivPrj @Record1 + , Constraints.lawProofEquivPrj @Record3 + , Constraints.lawProofEquivPrj @CompositeRecord + + , Constraints.lawProofEquivPrj @Record1W + , Constraints.lawProofEquivPrj @Record3W + , Constraints.lawProofEquivPrj @CompositeRecordW + ] + + , testGroup "Bare laws" + [ Bare.laws @Record1W + , Bare.laws @Record3W + , Bare.laws @Sum3W + , Bare.laws @SumRecW + , Bare.laws @NestedFW + ] + + , testGroup "Generic wrapper" + [ Wrapper.lawsMonoid @Record3 + , Wrapper.lawsMonoid @Record3W + ] + ] diff --git a/test/Spec/Bare.hs b/test/Spec/Bare.hs new file mode 100644 --- /dev/null +++ b/test/Spec/Bare.hs @@ -0,0 +1,31 @@ +{-# LANGUAGE AllowAmbiguousTypes #-} +{-# LANGUAGE ScopedTypeVariables #-} +module Spec.Bare ( laws ) + +where + +import Data.Barbie (BareB(..)) +import Data.Functor.Identity + +import Data.Typeable (Typeable, typeRep, Proxy(..)) + +import Test.Tasty(testGroup, TestTree) +import Test.Tasty.QuickCheck(Arbitrary(..), testProperty, (===)) + +laws + :: forall b + . ( BareB b + , Eq (b Identity) , Show (b Identity) , Arbitrary (b Identity) + -- , Show (b Bare), Eq (b Bare), Arbitrary (b Bare) + , Typeable b + ) + => TestTree +laws + = testGroup (show (typeRep (Proxy :: Proxy b))) + [ testProperty "bcover . bstrip = id" $ \b -> + bcover (bstrip b) === (b :: b Identity) + + -- TODO: FIXME + -- , testProperty "bstrip . bcover = id" $ \b -> + -- bstrip (bcover b) === (b :: b Bare) + ] diff --git a/test/Spec/Constraints.hs b/test/Spec/Constraints.hs new file mode 100644 --- /dev/null +++ b/test/Spec/Constraints.hs @@ -0,0 +1,50 @@ +{-# LANGUAGE AllowAmbiguousTypes #-} +{-# LANGUAGE ScopedTypeVariables #-} +module Spec.Constraints + ( lawAdjProofPrj + , lawProofEquivPrj + ) + +where + +import Clothes(F) +import Data.Barbie(bmap, ConstraintsB(..), ProofB(..)) +import Data.Barbie.Constraints(DictOf) + +import Data.Functor.Product (Product(Pair)) +import Data.Typeable(Typeable, Proxy(..), typeRep) + +import Test.Tasty(TestTree) +import Test.Tasty.QuickCheck(Arbitrary(..), testProperty, (===)) + + +lawAdjProofPrj + :: forall b + . ( ConstraintsB b, ConstraintsOf Show F b + , Eq (b F) + , Show (b F) + , Arbitrary (b F) + , Typeable b + ) + => TestTree +lawAdjProofPrj + = testProperty (show (typeRep (Proxy :: Proxy b))) $ \b -> + bmap second (adjProof b :: b (Product (DictOf Show F) F)) === b + where + second (Pair _ b) = b + + +lawProofEquivPrj + :: forall b + . ( ProofB b, ConstraintsOf Show F b + , Eq (b (DictOf Show F)) + , Show (b F), Show (b (DictOf Show F)) + , Arbitrary (b F) + , Typeable b + ) + => TestTree +lawProofEquivPrj + = testProperty (show (typeRep (Proxy :: Proxy b))) $ \b -> + bmap first (adjProof b :: b (Product (DictOf Show F) F)) === bproof + where + first (Pair a _) = a diff --git a/test/Spec/Functor.hs b/test/Spec/Functor.hs new file mode 100644 --- /dev/null +++ b/test/Spec/Functor.hs @@ -0,0 +1,33 @@ +{-# LANGUAGE AllowAmbiguousTypes #-} +{-# LANGUAGE ScopedTypeVariables #-} +module Spec.Functor ( laws ) + +where + +import Clothes (F, H, FG(..), GH(..), NatTransf(..)) + +import Data.Barbie (FunctorB(..)) + +import Data.Typeable (Typeable, typeRep, Proxy(..)) + +import Test.Tasty(testGroup, TestTree) +import Test.Tasty.QuickCheck(Arbitrary(..), testProperty, (===)) + +laws + :: forall b + . ( FunctorB b + , Eq (b F), Eq (b H) + , Show (b F), Show (b H) + , Arbitrary (b F) + , Typeable b + ) + => TestTree +laws + = testGroup (show (typeRep (Proxy :: Proxy b))) + [ testProperty "bmap id = id" $ \b -> + bmap id b === (b :: b F) + + , testProperty "bmap (f . g) = bmap f . bmap g)" $ + \b (GH (NatTransf f)) (FG (NatTransf g)) -> + bmap (f . g) b === (bmap f . bmap g) (b :: b F) + ] diff --git a/test/Spec/Product.hs b/test/Spec/Product.hs new file mode 100644 --- /dev/null +++ b/test/Spec/Product.hs @@ -0,0 +1,46 @@ +{-# LANGUAGE AllowAmbiguousTypes #-} +{-# LANGUAGE ScopedTypeVariables #-} +module Spec.Product ( laws, uniqLaws ) + +where + +import Clothes(F, G) + +import Data.Barbie(FunctorB(..), ProductB(..)) + +import Data.Functor.Product(Product(Pair)) +import Data.Typeable(Typeable, Proxy(..), typeRep) + +import Test.Tasty(TestTree) +import Test.Tasty.QuickCheck(Arbitrary(..), testProperty, (===)) + + +laws + :: forall b + . ( ProductB b + , Eq (b F), Eq (b G) + , Show (b F), Show (b G) + , Arbitrary (b F), Arbitrary (b G) + , Typeable b + ) + => TestTree +laws + = testProperty (show (typeRep (Proxy :: Proxy b))) $ \l r -> + bmap first (bprod l r) == (l :: b F) && + bmap second (bprod l r) == (r :: b G) + where + first (Pair a _) = a + second (Pair _ b) = b + +uniqLaws + :: forall b + . ( ProductB b + , Eq (b Maybe) + , Show (b F), Show (b Maybe) + , Arbitrary (b F) + , Typeable b + ) + => TestTree +uniqLaws + = testProperty (show (typeRep (Proxy :: Proxy b))) $ \b -> + bmap (const Nothing) (b :: b F) === buniq Nothing diff --git a/test/Spec/Traversable.hs b/test/Spec/Traversable.hs new file mode 100644 --- /dev/null +++ b/test/Spec/Traversable.hs @@ -0,0 +1,45 @@ +{-# LANGUAGE AllowAmbiguousTypes #-} +{-# LANGUAGE ScopedTypeVariables #-} +module Spec.Traversable ( laws ) + +where + +import Clothes (F, G, H, FG(..), GH(..), NatTransf(..)) + +import Data.Barbie (TraversableB(..)) + +import Data.Functor.Compose (Compose(..)) +import Data.Functor.Identity (Identity(..)) +import Data.Maybe (maybeToList) +import Data.Typeable (Typeable, typeRep, Proxy(..)) + +import Test.Tasty(testGroup, TestTree) +import Test.Tasty.QuickCheck(Arbitrary(..), testProperty, (===)) + +laws + :: forall b + . ( TraversableB b + , Eq (b F), Eq (b G), Eq (b H) + , Show (b F), Show (b G), Show (b H) + , Arbitrary (b F) + , Typeable b + ) + => TestTree +laws + = testGroup (show (typeRep (Proxy :: Proxy b))) + [testProperty "naturality" $ + \b (FG (NatTransf fg)) -> + let f = Just . fg + t = maybeToList + in (t . btraverse f) (b :: b F) === btraverse (t . f) (b :: b F) + + , testProperty "identity" $ \b -> + btraverse Identity b === Identity (b :: b F) + + , testProperty "composition" $ + \b (FG (NatTransf fg)) (GH (NatTransf gh)) -> + let f x = Just (fg x) + g x = [gh x] + in btraverse (Compose . fmap g . f) b === + (Compose . fmap (btraverse g) . btraverse f) (b :: b F) + ] diff --git a/test/Spec/Wrapper.hs b/test/Spec/Wrapper.hs new file mode 100644 --- /dev/null +++ b/test/Spec/Wrapper.hs @@ -0,0 +1,39 @@ +{-# OPTIONS_GHC -fno-warn-orphans #-} +{-# LANGUAGE AllowAmbiguousTypes #-} +{-# LANGUAGE ScopedTypeVariables #-} +module Spec.Wrapper ( + lawsMonoid + ) + +where + +import Data.Barbie (Barbie(..), ConstraintsOf, ProofB) + +import Data.Monoid + +import Test.Tasty(testGroup, TestTree) +import Test.Tasty.QuickCheck(Arbitrary(..), testProperty) + +lawsMonoid + :: forall b + . ( Arbitrary (b []), Eq (b []), Show (b []) + , ProofB b + , ConstraintsOf Monoid [] b + ) + => TestTree +lawsMonoid + = testGroup "Monoid laws" + [ testProperty "neutral element" $ \b -> + unwrap (Barbie b <> mempty) == b && + unwrap (mempty <> Barbie b) == b + + , testProperty "associativity" $ \b1 b2 b3 -> + unwrap ((Barbie b1 <> Barbie b2) <> Barbie b3) == + unwrap ( Barbie b1 <> (Barbie b2 <> Barbie b3)) + ] + where + unwrap = getBarbie :: Barbie b [] -> b [] + + +instance Arbitrary (b f) => Arbitrary (Barbie b f) where + arbitrary = Barbie <$> arbitrary