diff --git a/CHANGELOG.md b/CHANGELOG.md new file mode 100644 --- /dev/null +++ b/CHANGELOG.md @@ -0,0 +1,4 @@ +## 0.1.1 (2024-04-04) +Initial release. + + * extracted from generic-data-functions diff --git a/LICENSE b/LICENSE new file mode 100644 --- /dev/null +++ b/LICENSE @@ -0,0 +1,20 @@ +Copyright (c) 2024 Ben Orchard (@raehik) + +Permission is hereby granted, free of charge, to any person obtaining +a copy of this software and associated documentation files (the +"Software"), to deal in the Software without restriction, including +without limitation the rights to use, copy, modify, merge, publish, +distribute, sublicense, and/or sell copies of the Software, and to +permit persons to whom the Software is furnished to do so, subject to +the following conditions: + +The above copyright notice and this permission notice shall be included +in all copies or substantial portions of the Software. + +THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, +EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF +MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. +IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY +CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, +TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION WITH THE +SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. diff --git a/README.md b/README.md new file mode 100644 --- /dev/null +++ b/README.md @@ -0,0 +1,19 @@ +[gdf-hackage]: https://hackage.haskell.org/package/generic-data-functions + +# generic-data-asserts +Structural assertions on the generic data representations (`GHC.Generic.Rep a`). + +Sometimes, we want to write generics that only work on certain data types with a +certain shape e.g. non-sum types (single constructor). Achieving this is fairly +straightforward if we add a `TypeError` constraint on the relevant generic +representation unwrapping instance (here, the `(:+:)` constructor sum type). + +This library effectively pulls those checks out of generic code and runs them by +separately. This way, we can simplify our generics, and make them more flexible +(e.g. a user may choose whether to permit void types at compile time or not). + +This began as a minor feature in my [generic-data-functions][gdf-hackage] +library. + +## License +Provided under the MIT license. See `LICENSE` for license text. diff --git a/generic-data-asserts.cabal b/generic-data-asserts.cabal new file mode 100644 --- /dev/null +++ b/generic-data-asserts.cabal @@ -0,0 +1,73 @@ +cabal-version: 1.12 + +-- This file has been generated from package.yaml by hpack version 0.35.2. +-- +-- see: https://github.com/sol/hpack + +name: generic-data-asserts +version: 0.1.1 +synopsis: Structural assertions on generic data representations. +description: Please see README.md. +category: Data, Serialization +homepage: https://github.com/raehik/generic-rep-asserts#readme +bug-reports: https://github.com/raehik/generic-rep-asserts/issues +author: Ben Orchard +maintainer: Ben Orchard +license: MIT +license-file: LICENSE +build-type: Simple +extra-source-files: + README.md + CHANGELOG.md + +source-repository head + type: git + location: https://github.com/raehik/generic-rep-asserts + +library + exposed-modules: + Generic.Data.Rep.Assert + other-modules: + Paths_generic_data_asserts + hs-source-dirs: + src + default-extensions: + LambdaCase + NoStarIsType + DerivingVia + DeriveAnyClass + GADTs + RoleAnnotations + DefaultSignatures + TypeFamilies + DataKinds + MagicHash + ghc-options: -Wall + build-depends: + base >=4.14 && <5 + default-language: GHC2021 + +test-suite spec + type: exitcode-stdio-1.0 + main-is: Main.hs + other-modules: + Paths_generic_data_asserts + hs-source-dirs: + test + default-extensions: + LambdaCase + NoStarIsType + DerivingVia + DeriveAnyClass + GADTs + RoleAnnotations + DefaultSignatures + TypeFamilies + DataKinds + MagicHash + ghc-options: -Wall + build-depends: + base >=4.14 && <5 + , generic-data-asserts + , type-spec >=0.4.0.0 && <0.5 + default-language: GHC2021 diff --git a/src/Generic/Data/Rep/Assert.hs b/src/Generic/Data/Rep/Assert.hs new file mode 100644 --- /dev/null +++ b/src/Generic/Data/Rep/Assert.hs @@ -0,0 +1,62 @@ +{-# LANGUAGE UndecidableInstances #-} -- for IsEnum + +-- | Structural assertions on generic data representation. + +module Generic.Data.Rep.Assert where + +import GHC.Generics +import GHC.TypeError +import GHC.TypeLits ( type Symbol ) +import Data.Kind ( type Constraint ) + +type GAssertError :: k -> Symbol -> Constraint +type GAssertError a msg = TypeError + ('Text "Assertion on generic representation failed for type: " + :<>: 'ShowType a + :$$: 'Text "Message: " :<>: 'Text msg) + +type family StripD1 a where StripD1 (D1 _ a) = a + +-- | Type is not void i.e. has at least one constructor. +type GAssertNotVoid a = Assert (IsNotVoid (StripD1 (Rep a))) + (GAssertError a "not non-void type (>=1 constructor)") +type family IsNotVoid a where + IsNotVoid V1 = False + IsNotVoid _ = True + +-- | Type is not a sum type i.e. has at most one constructor. +-- +-- Permits void types. +type GAssertNotSum a = Assert (IsNotSum (StripD1 (Rep a))) + (GAssertError a "not non-sum type (1 constructor)") +type family IsNotSum a where + IsNotSum (_ :+: _) = False + IsNotSum _ = True + +-- | Type is a sum type i.e. has >=2 constructors. +-- +-- Permits void types. +type GAssertSum a = Assert (IsSum (StripD1 (Rep a))) + (GAssertError a "not sum type (>=2 constructors)") +type family IsSum a where + IsSum (C1 _ _) = False + IsSum _ = True + +-- | Type has only empty constructors. +-- +-- Permits void types. +type GAssertEnum a = Assert (IsEnum (StripD1 (Rep a))) + (GAssertError a "not enum type (all empty constructors)") +type family IsEnum a where + IsEnum V1 = True + IsEnum (C1 _ a) = ConsIsEmpty a + IsEnum (l :+: r) = IsEnum l `And` IsEnum r + +type family ConsIsEmpty a where + ConsIsEmpty U1 = True + ConsIsEmpty _ = False + +-- | Type level boolean AND. +type family And l r where + And True True = True + And _ _ = False diff --git a/test/Main.hs b/test/Main.hs new file mode 100644 --- /dev/null +++ b/test/Main.hs @@ -0,0 +1,27 @@ +module Main where + +import Test.TypeSpec +import GHC.Generics +import Generic.Data.Rep.Assert +import Data.Kind + +data DSum = DSum1 () | DSum2 deriving stock Generic +data DEnum = DEnum1 | DEnum2 | DEnum3 deriving stock Generic +data DNonSum = DNonSum () () deriving stock Generic +data DVoid deriving stock Generic + +main :: IO () +main = print spec + +spec + :: Expect '[ AssertPasses (GAssertNotVoid DSum) + , AssertPasses (GAssertSum DSum) + , AssertPasses (GAssertNotSum DNonSum) + , AssertPasses (GAssertEnum DEnum) + ] +spec = Valid + +type AssertPasses a = Is a (() :: Constraint) + +-- can't write this because GHC finds the TypeError before type-spec +--type AssertFails a = Isn't a (() :: Constraint)