diff --git a/ChangeLog.md b/ChangeLog.md --- a/ChangeLog.md +++ b/ChangeLog.md @@ -1,5 +1,23 @@ # Revision history for boring +## 0.2.2 + +- Support GHC-8.6.5...9.10.1 + +## 0.2.1 + +- Add instances for `SNat`, `SSymbol`, and `SChar` + (singletons introduced in `base-4.18.0.0`) + +## 0.2 + +- Make `boring` package dependency light. + `fin`, `bin`, `ral`, `vec`, `dec`, `singleton-bool` instances + are migrated to corresponding packages. + Rest are migrated to `boring-instances` for now. +- Data.Boring is `Trustworthy` +- Add Generic derivation. Thanks to David Feuer. + ## 0.1.3 - Allow `vec-0.3` diff --git a/boring.cabal b/boring.cabal --- a/boring.cabal +++ b/boring.cabal @@ -1,66 +1,68 @@ +cabal-version: 2.2 name: boring -version: 0.1.3 +version: 0.2.2.1 synopsis: Boring and Absurd types description: * @Boring@ types are isomorphic to @()@. - . + . * @Absurd@ types are isomorphic to @Void@. . See [What does () mean in Haskell -answer by Conor McBride](https://stackoverflow.com/questions/33112439/what-does-mean-in-haskell/33115522#33115522) homepage: https://github.com/phadej/boring bug-reports: https://github.com/phadej/boring/issues -license: BSD3 +license: BSD-3-Clause license-file: LICENSE author: Oleg Grenrus maintainer: Oleg.Grenrus -copyright: (c) 2017-2019 Oleg Grenrus +copyright: (c) 2017-2021 Oleg Grenrus category: Data build-type: Simple extra-source-files: ChangeLog.md -cabal-version: >=1.10 tested-with: - GHC ==7.8.4 - || ==7.10.3 - || ==8.0.2 - || ==8.2.2 - || ==8.4.4 - || ==8.6.5 - || ==8.8.1 + GHC ==8.6.5 + || ==8.8.4 + || ==8.10.7 + || ==9.0.2 + || ==9.2.8 + || ==9.4.8 + || ==9.6.6 + || ==9.8.4 + || ==9.10.3 + || ==9.12.2 + || ==9.14.1 source-repository head type: git location: https://github.com/phadej/boring.git + subdir: boring +flag tagged + description: + You can disable the use of the `tagged` package using `-f-tagged`. + . + Disabling this is an unsupported configuration, but it may be useful for accelerating builds in sandboxes for expert users. + + default: True + manual: True + library exposed-modules: Data.Boring build-depends: - adjunctions >=4.4 && <4.5 - , base >=4.7 && <4.14 - , base-compat >=0.10.5 && <0.12 - , bin >=0.1 && <0.2 - , constraints ==0.4.1.3 || >=0.10 && <0.12 - , dec >=0.0.3 && <0.1 - , fin >=0.0.3 && <0.2 - , generics-sop >=0.3.2.0 && <0.6 - , ral >=0.1 && <0.2 - , singleton-bool >=0.1.4 && <0.2 - , streams >=3.3 && <3.4 - , tagged >=0.8.6 && <0.9 - , transformers >=0.3 && <0.6 - , transformers-compat >=0.5 && <0.7 - , vec >=0.1 && <0.4 + base >=4.12.0.0 && <4.23 - if !impl(ghc >=8.0) - build-depends: semigroups >=0.18.5 && <0.20 + if impl(ghc <7.6) + build-depends: ghc-prim - if !impl(ghc >=7.10) - build-depends: void >=0.7.2 && <0.8 + if flag(tagged) + build-depends: tagged >=0.8.6 && <0.9 other-extensions: CPP + DefaultSignatures FlexibleContexts GADTs + Trustworthy TypeOperators hs-source-dirs: src diff --git a/src/Data/Boring.hs b/src/Data/Boring.hs --- a/src/Data/Boring.hs +++ b/src/Data/Boring.hs @@ -1,12 +1,10 @@ -{-# LANGUAGE CPP #-} -{-# LANGUAGE DataKinds #-} -{-# LANGUAGE EmptyCase #-} -{-# LANGUAGE FlexibleContexts #-} -{-# LANGUAGE GADTs #-} -{-# LANGUAGE TypeOperators #-} -{-# LANGUAGE ConstraintKinds #-} -{-# LANGUAGE ScopedTypeVariables #-} -{-# LANGUAGE UndecidableInstances #-} +{-# LANGUAGE CPP #-} +{-# LANGUAGE DefaultSignatures #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE Trustworthy #-} +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE EmptyCase #-} -- | 'Boring' and 'Absurd' classes. One approach. -- -- Different approach would be to have @@ -55,59 +53,50 @@ -- * Classes Boring (..), Absurd (..), + -- ** Generic implementation + GBoring, + GAbsurd, -- * More interesting stuff vacuous, - boringRep, - untainted, devoid, united, - -- ** Dec - -- - -- | @'Dec' a@ can be 'Boring' in two ways: When 'a' is 'Boring' or 'Absurd'. - boringYes, - absurdNo, - ) where +) where -import Prelude () -import Prelude.Compat +import Prelude (Either (..), Functor (..), Maybe (..), const, (.)) -import Control.Applicative (Const (..)) -import Data.Functor.Identity (Identity (..)) +import Control.Applicative (Const (..), (<$)) import Data.Functor.Compose (Compose (..)) +import Data.Functor.Identity (Identity (..)) import Data.Functor.Product (Product (..)) import Data.Functor.Sum (Sum (..)) -import Data.Functor.Rep (Representable (..)) -import Data.Constraint (Dict (..)) import Data.List.NonEmpty (NonEmpty (..)) import Data.Proxy (Proxy (..)) -import Data.Tagged (Tagged (..)) -import Data.Type.Dec (Dec (..), Decidable (..)) -import Data.Stream.Infinite (Stream (..)) -import GHC.Generics hiding (Rep) +import GHC.Generics + (Generic (..), K1 (..), M1 (..), Par1 (..), Rec1 (..), U1 (..), V1, + (:*:) (..), (:+:) (..), (:.:) (..)) -import qualified Data.Bin as Bin -import qualified Data.Bin.Pos as Pos -import qualified Data.BinP.PosP as PosP -import qualified Data.Fin as Fin -import qualified Data.Nat as Nat -import qualified Data.RAList.NonEmpty as NERAList -import qualified Data.RAVec as RAVec -import qualified Data.Singletons.Bool as Bool -import qualified Data.Type.Bin as Bin -import qualified Data.Type.Nat as Nat -import qualified Data.Type.Nat.LE as ZeroSucc -import qualified Data.Type.Nat.LE.ReflStep as ReflStep -import qualified Data.Vec.Lazy as Vec -import qualified Data.Vec.Pull as Vec.Pull -import qualified Data.Void as V -import qualified Generics.SOP as SOP +import qualified Data.Void as V -#if MIN_VERSION_base(4,7,0) import qualified Data.Coerce as Co import qualified Data.Type.Coercion as Co + import qualified Data.Type.Equality as Eq + +import qualified Type.Reflection as Typeable + +#if MIN_VERSION_base(4,18,0) +import qualified GHC.TypeLits as TypeLits +import qualified GHC.TypeNats as TypeNats #endif +#ifdef MIN_VERSION_tagged +import Data.Tagged (Tagged (..)) +#endif + +-- $setup +-- >>> :set -XDeriveGeneric +-- >>> import GHC.Generics (Generic) + ------------------------------------------------------------------------------- -- Boring ------------------------------------------------------------------------------- @@ -143,6 +132,8 @@ -- class Boring a where boring :: a + default boring :: (Generic a, GBoring (Rep a)) => a + boring = to gboring instance Boring () where boring = () @@ -156,27 +147,20 @@ instance Boring a => Boring (Const a b) where boring = Const boring +#ifdef MIN_VERSION_tagged instance Boring b => Boring (Tagged a b) where boring = Tagged boring +#endif instance Boring a => Boring (Identity a) where boring = Identity boring -instance Boring a => Boring (SOP.I a) where - boring = SOP.I boring - -instance Boring b => Boring (SOP.K b a) where - boring = SOP.K boring - instance Boring (f (g a)) => Boring (Compose f g a) where boring = Compose boring instance (Boring (f a), Boring (g a)) => Boring (Product f g a) where boring = Pair boring boring -instance c => Boring (Dict c) where - boring = Dict - instance (Boring a, Boring b) => Boring (a, b) where boring = (boring, boring) @@ -189,9 +173,6 @@ instance (Boring a, Boring b, Boring c, Boring d, Boring e) => Boring (a, b, c, d, e) where boring = (boring, boring, boring, boring, boring) -instance Boring a => Boring (Stream a) where - boring = boring :> boring - -- | Recall regular expressions, kleene star of empty regexp is epsilon! instance Absurd a => Boring [a] where boring = [] @@ -200,7 +181,6 @@ instance Absurd a => Boring (Maybe a) where boring = Nothing -#if MIN_VERSION_base(4,7,0) -- | Coercibility is 'Boring' too. instance Co.Coercible a b => Boring (Co.Coercion a b) where boring = Co.Coercion @@ -209,67 +189,23 @@ instance a ~ b => Boring (a Eq.:~: b) where boring = Eq.Refl -# if MIN_VERSION_base(4,12,0) -- | Heterogeneous type equality is 'Boring' too. instance a Eq.~~ b => Boring (a Eq.:~~: b) where boring = Eq.HRefl -# endif -#endif -------------------------------------------------------------------------------- --- vec + fin + singleton-bool -------------------------------------------------------------------------------- - -instance n ~ 'Nat.Z => Boring (Vec.Vec n a) where - boring = Vec.empty - -instance n ~ 'Nat.Z => Boring (Vec.Pull.Vec n a) where - boring = Vec.Pull.empty - -instance n ~ ('Nat.S 'Nat.Z) => Boring (Fin.Fin n) where - boring = Fin.boring - --- singletons are boring - --- | @since 0.1.2 -instance Nat.SNatI n => Boring (Nat.SNat n) where - boring = Nat.snat - --- | @since 0.1.2 -instance Bool.SBoolI b => Boring (Bool.SBool b) where - boring = Bool.sbool - --- | @since 0.1.2 -instance ZeroSucc.LE n m => Boring (ZeroSucc.LEProof n m) where - boring = ZeroSucc.leProof - --- | @since 0.1.2 -instance (ZeroSucc.LE n m, Nat.SNatI m) => Boring (ReflStep.LEProof n m) where - boring = ReflStep.fromZeroSucc ZeroSucc.leProof - -------------------------------------------------------------------------------- --- bin + ral -------------------------------------------------------------------------------- - --- | @since 0.1.3 -instance b ~ 'Bin.BZ => Boring (RAVec.RAVec b a) where - boring = RAVec.empty - --- | @since 0.1.3 -instance b ~ 'Bin.BE => Boring (PosP.PosP b) where - boring = PosP.boring +instance Typeable.Typeable a => Boring (Typeable.TypeRep a) where + boring = Typeable.typeRep --- | @since 0.1.3 -instance b ~ 'Bin.BP 'Bin.BE => Boring (Pos.Pos b) where - boring = Pos.boring +#if MIN_VERSION_base(4,18,0) +instance TypeLits.KnownChar n => Boring (TypeLits.SChar n) where + boring = TypeLits.charSing --- | @since 0.1.3 -instance Bin.SBinI b => Boring (Bin.SBin b) where - boring = Bin.sbin +instance TypeLits.KnownSymbol n => Boring (TypeLits.SSymbol n) where + boring = TypeLits.symbolSing --- | @since 0.1.3 -instance Bin.SBinPI b => Boring (Bin.SBinP b) where - boring = Bin.sbinp +instance TypeNats.KnownNat n => Boring (TypeNats.SNat n) where + boring = TypeNats.natSing +#endif ------------------------------------------------------------------------------- -- Generics @@ -296,6 +232,7 @@ instance Boring (f (g p)) => Boring ((f :.: g) p) where boring = Comp1 boring + ------------------------------------------------------------------------------- -- Absurd ------------------------------------------------------------------------------- @@ -308,6 +245,8 @@ -- so we don't have 'Absurd' instances for tuples. class Absurd a where absurd :: a -> b + default absurd :: (Generic a, GAbsurd (Rep a)) => a -> b + absurd = gabsurd . from instance Absurd V.Void where absurd = V.absurd @@ -319,9 +258,6 @@ instance Absurd a => Absurd (NonEmpty a) where absurd (x :| _) = absurd x -instance Absurd a => Absurd (Stream a) where - absurd (x :> _) = absurd x - instance Absurd a => Absurd (Identity a) where absurd = absurd . runIdentity @@ -335,31 +271,10 @@ instance Absurd b => Absurd (Const b a) where absurd = absurd . getConst +#ifdef MIN_VERSION_tagged instance Absurd a => Absurd (Tagged b a) where absurd = absurd . unTagged - -instance Absurd a => Absurd (SOP.I a) where - absurd = absurd . SOP.unI - -instance Absurd b => Absurd (SOP.K b a) where - absurd = absurd . SOP.unK - -instance n ~ 'Nat.Z => Absurd (Fin.Fin n) where - absurd = Fin.absurd - -instance (ZeroSucc.LE m n, n' ~ 'Nat.S n) => Absurd (ZeroSucc.LEProof n' m) where - absurd = ZeroSucc.leSwap' ZeroSucc.leProof - -instance (ZeroSucc.LE m n, n' ~ 'Nat.S n, Nat.SNatI n) => Absurd (ReflStep.LEProof n' m) where - absurd = ZeroSucc.leSwap' ZeroSucc.leProof . ReflStep.toZeroSucc - --- | @since 0.1.3 -instance b ~ 'Bin.BZ => Absurd (Pos.Pos b) where - absurd = Pos.absurd - --- | @since 0.1.3 -instance Absurd a => Absurd (NERAList.NERAList a) where - absurd = absurd . NERAList.head +#endif ------------------------------------------------------------------------------- -- Generics @@ -396,16 +311,6 @@ vacuous :: (Functor f, Absurd a) => f a -> f b vacuous = fmap absurd --- | If an index of 'Representable' @f@ is 'Absurd', @f a@ is 'Boring'. -boringRep :: (Representable f, Absurd (Rep f)) => f a -boringRep = tabulate absurd - --- | If an index of 'Representable' @f@ is 'Boring', @f@ is isomorphic to 'Identity'. --- --- See also @Settable@ class in @lens@. -untainted :: (Representable f, Boring (Rep f)) => f a -> a -untainted = flip index boring - -- | There is a field for every type in the 'Absurd'. Very zen. -- -- @ @@ -424,23 +329,68 @@ united f v = v <$ f boring ------------------------------------------------------------------------------- --- Dec +-- default implementatiosn ------------------------------------------------------------------------------- --- | This relies on the fact that @a@ is /proposition/ in h-Prop sense. +-- | A helper class to implement 'Generic' derivation of 'Boring'. -- --- @since 0.1.3 -instance Decidable a => Boring (Dec a) where - boring = decide - --- | 'Yes', it's 'boring'. +-- Technically we could do (avoiding @QuantifiedConstraints@): -- --- @since 0.1.3 -boringYes :: Boring a => Dec a -boringYes = Yes boring +-- @ +-- type GBoring f = (Boring (f V.Void), Functor f) +-- +-- gboring :: forall f x. GBoring f => f x +-- gboring = vacuous (boring :: f V.Void) +-- @ +-- +-- but separate class is cleaner. +-- +-- >>> data B2 = B2 () () deriving (Show, Generic) +-- >>> instance Boring B2 +-- >>> boring :: B2 +-- B2 () () +-- +class GBoring f where + gboring :: f a --- | 'No', it's 'absurd'. +instance GBoring U1 where + gboring = U1 + +instance GBoring f => GBoring (M1 i c f) where + gboring = M1 gboring + +instance (GBoring f, GBoring g) => GBoring (f :*: g) where + gboring = gboring :*: gboring + +-- There are two valid instances for GBoring (f :+: g), so we don't define +-- either of them. + +instance Boring c => GBoring (K1 i c) where + gboring = K1 boring + +-- | A helper class to implement of 'Generic' derivation of 'Absurd'. -- --- @since 0.1.3 -absurdNo :: Absurd a => Dec a -absurdNo = No absurd +-- @ +-- type GAbsurd f = (Absurd (f ()), Functor f) +-- +-- gabsurd :: forall f x y. GAbsurd f => f x -> y +-- gabsurd = absurd . void +-- @ +-- +class GAbsurd f where + gabsurd :: f a -> b + +instance GAbsurd V1 where + gabsurd x = case x of {} + +instance GAbsurd f => GAbsurd (M1 i c f) where + gabsurd (M1 x) = gabsurd x + +instance Absurd c => GAbsurd (K1 i c) where + gabsurd (K1 x) = absurd x + +instance (GAbsurd f, GAbsurd g) => GAbsurd (f :+: g) where + gabsurd (L1 x) = gabsurd x + gabsurd (R1 y) = gabsurd y + +-- There are two reasonable instances for GAbsurd (f :*: g), so we define neither