diff --git a/CHANGELOG.md b/CHANGELOG.md new file mode 100644 --- /dev/null +++ b/CHANGELOG.md @@ -0,0 +1,5 @@ +# Revision history for partial-structures + +## 0.1.0.0 -- YYYY-mm-dd + +* First version. Released on an unsuspecting world. diff --git a/LICENSE b/LICENSE new file mode 100644 --- /dev/null +++ b/LICENSE @@ -0,0 +1,20 @@ +Copyright (c) 2019 Tom Harding + +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,275 @@ +# Higgledy 📚 + +Higher-kinded data via generics: all\* the benefits, but none\* of the +boilerplate. + +## Introduction + +When we work with [higher-kinded +data](https://reasonablypolymorphic.com/blog/higher-kinded-data), we find +ourselves writing types like: + +```haskell +data User f + = User + { name :: f String + , age :: f Int + , ... + } +``` + +This is good - we can use `f ~ Maybe` for partial data, `f ~ Identity` for +complete data, etc - but it introduces a fair amount of noise, and we have a +lot of boilerplate deriving to do. Wouldn't it be nice if we could get back to +writing simple types as we know and love them, and get all this stuff for +_free_? + +```haskell +data User + = User + { name :: String + , age :: Int + , ... + } + deriving Generic + +-- HKD for free! +type UserF f = HKD User f +``` + +As an added little bonus, any `HKD`-wrapped object is automatically an instance +of all the [Barbie](http://hackage.haskell.org/package/barbies) classes, so no +need to derive anything more than `Generic`! + +## API + +All examples below were compiled with the following extensions, modules, and +example data types: + +```haskell +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE DeriveGeneric #-} +{-# LANGUAGE TypeApplications #-} +module Example where + +import Control.Lens ((.~), (^.), (&), Const (..), Identity, anyOf) +import Data.Generic.HKD +import Data.Maybe (isJust, isNothing) +import Data.Monoid (Last (..)) +import GHC.Generics (Generic) + +-- An example of a record (with named fields): +data User + = User + { name :: String + , age :: Int + , likesDogs :: Bool + } + deriving (Generic, Show) + +user :: User +user = User "Tom" 25 True + +-- An example of a product (without named fields): +data Triple + = Triple Int () String + deriving (Generic, Show) + +triple :: Triple +triple = Triple 123 () "ABC" +``` + +### The HKD type constructor + +The `HKD` type takes two parameters: your model type, and the functor in which +we want to wrap all our inputs. By picking different functors for the second +parameter, we can recover various behaviours: + +```haskell +type Partial a = HKD a Last -- Fields may be missing. +type Bare a = HKD a Identity -- All must be present. +type Labels a = HKD a (Const String) -- Every field holds a string. +``` + +### Fresh objects + +When we want to start working with the `HKD` interface, we have a couple of +options, depending on the functor in question. The first option is to use +`mempty`: + +```haskell +eg0 :: Partial User +eg0 = mempty +-- User +-- { name = Last {getLast = Nothing} +-- , age = Last {getLast = Nothing} +-- , likesDogs = Last {getLast = Nothing} +-- } +``` + +Other 'Alternative'-style functors lead to very different results: + +```haskell +eg1 :: Labels Triple +eg1 = mempty +-- Triple +-- Const "" +-- Const "" +-- Const "" +``` + +Of course, this method requires every field to be monoidal. If we try with +`Identity`, for example, we're in trouble if all our fields aren't themselves +monoids: + +```haskell +eg2 :: Bare Triple +eg2 = mempty +-- error: +-- • No instance for (Monoid Int) arising from a use of ‘mempty’ +``` + +The other option is to `deconstruct` a complete object. This effectively lifts +a type into the `HKD` structure with `pure` applied to each field: + +```haskell +eg3 :: Bare User +eg3 = deconstruct user +-- User +-- { name = Identity "Tom" +-- , age = Identity 25 +-- , likesDogs = Identity True +-- } +``` + +This approach works with any applicative we like, so we can recover the other +behaviours: + +```haskell +eg4 :: Partial Triple +eg4 = deconstruct @Last triple +-- Triple +-- Last {getLast = Just 123} +-- Last {getLast = Just ()} +-- Last {getLast = Just "ABC"} +``` + +There's also `construct` for when we want to escape our `HKD` wrapper, and +attempt to _construct_ our original type: + +```haskell +eg5 :: Last Triple +eg5 = construct eg4 +-- Last {getLast = Just (Triple 123 () "ABC")} +``` + +### Field Access + +The `field` lens, when given a type-applied field name, allows us to focus on +fields within a record: + +```haskell +eg6 :: Last Int +eg6 = eg0 ^. field @"age" +-- Last {getLast = Nothing} +``` + +As this is a true `Lens`, it also means that we can _set_ values within our +record (note that these set values will _also_ need to be in our functor of +choice): + +```haskell +eg7 :: Partial User +eg7 = eg0 & field @"name" .~ pure "Evil Tom" + & field @"likesDogs" .~ pure False +-- User +-- { name = Last {getLast = Just "Evil Tom"} +-- , age = Last {getLast = Nothing} +-- , likesDogs = Last {getLast = Just False} +-- } +``` + +This also means, for example, we can check whether a particular value has been +completed for a given partial type: + +```haskell +eg8 :: Bool +eg8 = anyOf (field @"name") (isJust . getLast) eg0 +-- False +``` + +Finally, thanks to the fact that this library exploits some of the internals of +`generic-lens`, we'll also get a nice type error when we mention a field that +doesn't exist in our type: + +```haskell +eg9 :: Identity () +eg9 = eg3 ^. field @"oops" +-- error: +-- • The type User does not contain a field named 'oops'. +``` + +### Position Access + +Just as with field names, we can use positions when working with non-record +product types: + +```haskell +eg10 :: Labels Triple +eg10 = mempty & position @1 .~ Const "hello" + & position @2 .~ Const "world" +-- Triple +-- Const "hello" +-- Const "world" +-- Const "" +``` + +Again, this is a `Lens`, so we can just as easily _set_ values: + +```haskell +eg11 :: Partial User +eg11 = eg7 & position @2 .~ pure 25 +-- User +-- { name = Last {getLast = Just "Evil Tom"} +-- , age = Last {getLast = Just 25} +-- , likesDogs = Last {getLast = Just False} +-- } +``` + +Similarly, the internals here come to us courtesy of `generic-lens`, so the +type errors are a delight: + +```haskell +eg9 :: Identity () +eg9 = deconstruct @Identity triple ^. position @4 +-- error: +-- • The type Triple does not contain a field at position 4 +``` + +### Labels + +One neat trick we can do - thanks to the generic representation - is get the +names of the fields into the functor we're using. The `label` function gives us +this interface: + +```haskell +eg10 :: Labels User +eg10 = label eg11 +-- User +-- { name = Const "name" +-- , age = Const "age" +-- , likesDogs = Const "likesDogs" +-- } +``` + +By combining this with some of the +[Barbies](http://hackage.haskell.org/package/barbies) interface (the entirety +of which is available to any `HKD`-wrapped type) such as `bprod` and `bmap`, we +can implement functions such as `labelsWhere`, which returns the names of all +fields whose values satisfy some predicate: + +```haskell +eg13 :: [String] +eg13 = labelsWhere (isNothing . getLast) eg7 +-- ["age"] +``` 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/higgledy.cabal b/higgledy.cabal new file mode 100644 --- /dev/null +++ b/higgledy.cabal @@ -0,0 +1,44 @@ +cabal-version: 2.4 + +name: higgledy +version: 0.1.0.0 +synopsis: Partial types as a type constructor. +description: Use the generic representation of an ADT to get a higher-kinded data-style interface automatically. +homepage: https://github.com/i-am-tom/higgledy +-- bug-reports: +license: MIT +license-file: LICENSE +author: Tom Harding +maintainer: tom.harding@habito.com +-- copyright: +category: Data +extra-source-files: CHANGELOG.md + , README.md + +library + exposed-modules: Data.Generic.HKD + Data.Generic.HKD.Construction + Data.Generic.HKD.Field + Data.Generic.HKD.Labels + Data.Generic.HKD.Position + Data.Generic.HKD.Types + -- other-modules: + -- other-extensions: + build-depends: base ^>=4.12.0.0 + , barbies ^>=1.1.0.0 + , generic-lens ^>=1.1.0.0 + , QuickCheck ^>=2.13.0 + hs-source-dirs: src + default-language: Haskell2010 + +test-suite test + build-depends: base + , doctest ^>=0.16.0 + , higgledy + , hspec ^>=2.7.0 + , lens ^>=4.17 + , QuickCheck + main-is: Main.hs + type: exitcode-stdio-1.0 + hs-source-dirs: test + default-language: Haskell2010 diff --git a/src/Data/Generic/HKD.hs b/src/Data/Generic/HKD.hs new file mode 100644 --- /dev/null +++ b/src/Data/Generic/HKD.hs @@ -0,0 +1,17 @@ +{-| +Module : Data.Generic.HKD +Description : A generic-based HKD decorator for ADTs. +Copyright : (c) Tom Harding, 2019 +License : MIT +Maintainer : tom.harding@habito.com +Stability : experimental +-} +module Data.Generic.HKD + ( module Exports + ) where + +import Data.Generic.HKD.Construction as Exports +import Data.Generic.HKD.Field as Exports +import Data.Generic.HKD.Labels as Exports +import Data.Generic.HKD.Position as Exports +import Data.Generic.HKD.Types as Exports diff --git a/src/Data/Generic/HKD/Construction.hs b/src/Data/Generic/HKD/Construction.hs new file mode 100644 --- /dev/null +++ b/src/Data/Generic/HKD/Construction.hs @@ -0,0 +1,78 @@ +{-# OPTIONS_HADDOCK not-home #-} + +{-# LANGUAGE AllowAmbiguousTypes #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE KindSignatures #-} +{-# LANGUAGE MonoLocalBinds #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TypeApplications #-} +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE UndecidableInstances #-} + +{-| +Module : Data.Generic.HKD.Construction +Description : Convert to and from the generic HKD structure. +Copyright : (c) Tom Harding, 2019 +License : MIT +Maintainer : tom.harding@habito.com +Stability : experimental +-} +module Data.Generic.HKD.Construction where + +import Data.Generic.HKD.Types (HKD (..), GHKD_) +import Data.Kind (Type) +import GHC.Generics + +-- | When working with the HKD representation, it is useful to have a way to +-- convert to and from our original type. To do this, we can: +-- +-- * @construct@ the original type from our HKD representation, and +-- +-- * @deconstruct@ the original type /into/ our HKD representation. +-- +-- As an example, we can try (unsuccessfully) to construct an @(Int, Bool)@ +-- tuple from an unpopulated partial structure. +-- +-- >>> :set -XTypeApplications +-- >>> import Data.Monoid (Last) +-- +-- >>> construct (mempty @(HKD (Int, Bool) Last)) +-- Last {getLast = Nothing} +-- +-- We can also /deconstruct/ a tuple into a partial structure: +-- +-- >>> deconstruct @[] ("Hello", True) +-- (,) ["Hello"] [True] +-- +-- These two methods also satisfy the round-tripping property: +-- +-- prop> construct (deconstruct x) == [ x :: (Int, Bool, String) ] +class Construct (f :: Type -> Type) (structure :: Type) where + construct :: HKD structure f -> f structure + deconstruct :: structure -> HKD structure f + +class GConstruct (f :: Type -> Type) (rep :: Type -> Type) where + gconstruct :: GHKD_ f rep p -> f (rep p) + gdeconstruct :: rep p -> GHKD_ f rep p + +instance (Functor f, GConstruct f inner) + => GConstruct f (M1 index meta inner) where + gconstruct = fmap M1 . gconstruct . unM1 + gdeconstruct = M1 . gdeconstruct @f . unM1 + +instance (Applicative f, GConstruct f left, GConstruct f right) + => GConstruct f (left :*: right) where + gconstruct (l :*: r) = (:*:) <$> gconstruct l <*> gconstruct r + gdeconstruct (l :*: r) = gdeconstruct @f l :*: gdeconstruct @f r + +instance Applicative f => GConstruct f (K1 index inner) where + gconstruct (K1 x) = fmap K1 x + gdeconstruct (K1 x) = K1 (pure x) + +instance (Functor f, Generic structure, GConstruct f (Rep structure)) + => Construct f structure where + construct = fmap to . gconstruct . runHKD + deconstruct = HKD . gdeconstruct @f . from diff --git a/src/Data/Generic/HKD/Field.hs b/src/Data/Generic/HKD/Field.hs new file mode 100644 --- /dev/null +++ b/src/Data/Generic/HKD/Field.hs @@ -0,0 +1,108 @@ +{-# OPTIONS_HADDOCK not-home #-} + +{-# LANGUAGE AllowAmbiguousTypes #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE FunctionalDependencies #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TypeApplications #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE UndecidableInstances #-} + +{-| +Module : Data.Generic.HKD.Field +Description : Manipulate HKD structures using field names. +Copyright : (c) Tom Harding, 2019 +License : MIT +Maintainer : tom.harding@habito.com +Stability : experimental +-} +module Data.Generic.HKD.Field + ( HasField' (..) + ) where + +import Data.Coerce (coerce) +import Data.Generic.HKD.Types (HKD (..), HKD_) +import Data.Kind (Constraint, Type) +import Data.Void (Void) +import GHC.TypeLits (ErrorMessage (..), Symbol, TypeError) +import qualified Data.GenericLens.Internal as G +import qualified Data.Generics.Internal.VL.Lens as G + +-- | When we work with records, all the fields are named, and we can refer to +-- them using these names. This class provides a lens from our HKD structure to +-- any @f@-wrapped field. +-- +-- >>> :set -XDataKinds -XDeriveGeneric +-- >>> import Control.Lens ((&), (.~)) +-- >>> import Data.Monoid (Last) +-- >>> import GHC.Generics +-- +-- >>> data User = User { name :: String, age :: Int } deriving (Generic, Show) +-- >>> type Partial a = HKD a Last +-- +-- We can create an empty partial @User@ and set its name to "Tom" (which, in +-- this case, is @pure "Tom" :: Last String@): +-- +-- >>> mempty @(Partial User) & field @"name" .~ pure "Tom" +-- User {name = Last {getLast = Just "Tom"}, age = Last {getLast = Nothing}} +-- +-- Thanks to some @generic-lens@ magic, we also get some pretty magical type +-- errors! If we create a (complete) partial user: +-- +-- >>> import Data.Generic.HKD.Construction (deconstruct) +-- >>> total = deconstruct @Last (User "Tom" 25) +-- +-- ... and then try to access a field that isn't there, we get a friendly +-- message to point us in the right direction: +-- +-- >>> total & field @"oops" .~ pure () +-- ... +-- ... error: +-- ... • The type User does not contain a field named 'oops'. +-- ... +class HasField' + (field :: Symbol) + (f :: Type -> Type) + (structure :: Type) + (focus :: Type) + | field f structure -> focus where + field :: G.Lens' (HKD structure f) (f focus) + +data HasTotalFieldPSym :: Symbol -> (G.TyFun (Type -> Type) (Maybe Type)) +type instance G.Eval (HasTotalFieldPSym sym) tt = G.HasTotalFieldP sym tt + +instance + ( ErrorUnless field structure (G.CollectField field (HKD_ f structure)) + , G.GLens' (HasTotalFieldPSym field) (HKD_ f structure) (f focus) + ) => HasField' field f structure focus where + field = coerced . G.ravel (G.glens @(HasTotalFieldPSym field)) + where + coerced :: G.Lens' (HKD structure f) (HKD_ f structure Void) + coerced f = fmap coerce . f . coerce + +-- We'll import this from actual generic-lens as soon as possible: + +type family ErrorUnless (field :: Symbol) (s :: Type) (stat :: G.TypeStat) :: Constraint where + ErrorUnless field s ('G.TypeStat _ _ '[]) + = TypeError + ( 'Text "The type " + ':<>: 'ShowType s + ':<>: 'Text " does not contain a field named '" + ':<>: 'Text field ':<>: 'Text "'." + ) + + ErrorUnless field s ('G.TypeStat (n ': ns) _ _) + = TypeError + ( 'Text "Not all constructors of the type " + ':<>: 'ShowType s + ':$$: 'Text " contain a field named '" + ':<>: 'Text field ':<>: 'Text "'." + ':$$: 'Text "The offending constructors are:" + ':$$: G.ShowSymbols (n ': ns) + ) + + ErrorUnless _ _ ('G.TypeStat '[] '[] _) + = () diff --git a/src/Data/Generic/HKD/Labels.hs b/src/Data/Generic/HKD/Labels.hs new file mode 100644 --- /dev/null +++ b/src/Data/Generic/HKD/Labels.hs @@ -0,0 +1,94 @@ +{-# LANGUAGE BlockArguments #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE FunctionalDependencies #-} +{-# LANGUAGE KindSignatures #-} +{-# LANGUAGE MonoLocalBinds #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TypeApplications #-} +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE UndecidableInstances #-} +module Data.Generic.HKD.Labels where + +import Data.Barbie (ProductB (..), TraversableB (..)) +import Data.Functor.Const (Const (..)) +import Data.Functor.Product (Product (..)) +import Data.Generic.HKD.Types (HKD (..), GHKD_) +import Data.Kind (Type) +import Data.Proxy (Proxy (..)) +import GHC.Generics +import GHC.TypeLits (ErrorMessage (..), KnownSymbol, TypeError, symbolVal) + +-- | For any record type, we can extract the labels generically using the +-- `Const` functor. +-- +-- >>> import Data.Generic.HKD +-- >>> import Data.Functor.Identity (Identity (..)) +-- +-- >>> data User = User { name :: String, age :: Int } deriving Generic +-- >>> label (deconstruct @Identity (User "Tom" 25)) +-- User {name = Const "name", age = Const "age"} +class Label (structure :: Type) where + label :: HKD structure f -> HKD structure (Const String) + +class GLabels (rep :: Type -> Type) where + glabel :: GHKD_ f rep p -> GHKD_ (Const String) rep p + +instance GLabels inner => GLabels (D1 meta inner) where + glabel = M1 . glabel . unM1 + +instance GLabels inner + => GLabels (C1 ('MetaCons name fixity 'True) inner) where + glabel = M1 . glabel . unM1 + +instance TypeError ('Text "You can't collect labels for a non-record type!") + => GLabels (C1 ('MetaCons name fixity 'False) inner) where + glabel = undefined + +instance KnownSymbol name + => GLabels (S1 ('MetaSel ('Just name) i d c) (K1 index inner)) where + glabel _ = M1 (K1 (Const (symbolVal (Proxy @name)))) + +instance (GLabels left, GLabels right) => GLabels (left :*: right) where + glabel (left :*: right) = glabel left :*: glabel right + +instance (Generic structure, GLabels (Rep structure)) => Label structure where + label = HKD . glabel . runHKD + +-- | Because all HKD types are valid barbies, and we have the above mechanism +-- for extracting field names, we can ask some pretty interesting questions. +-- +-- >>> import Control.Lens +-- >>> import Data.Maybe (isNothing) +-- >>> import Data.Monoid (Last (..)) +-- >>> import Data.Generic.HKD +-- +-- Let's imagine, for example, that we're half way through filling in a user's +-- details: +-- +-- >>> data User = User { name :: String, age :: Int } deriving Generic +-- >>> test = mempty @(HKD User Last) & field @"name" .~ pure "Tom" +-- +-- We want to send a JSON response back to the client containing the fields +-- that have yet to be finished. All we need to do is pick the fields where the +-- values are @Last Nothing@: +-- +-- >>> labelsWhere (isNothing . getLast) test +-- ["age"] +labelsWhere + :: forall structure f + . ( Label structure + , ProductB (HKD structure) + , TraversableB (HKD structure) + ) + => (forall a. f a -> Bool) + -> HKD structure f + -> [String] + +labelsWhere p xs + = getConst (btraverse go (label xs `bprod` xs)) + where + go :: Product (Const String) f a -> (Const [String]) (Maybe a) + go (Pair (Const key) value) = Const if p value then [key] else [] diff --git a/src/Data/Generic/HKD/Position.hs b/src/Data/Generic/HKD/Position.hs new file mode 100644 --- /dev/null +++ b/src/Data/Generic/HKD/Position.hs @@ -0,0 +1,119 @@ +{-# OPTIONS_HADDOCK not-home #-} + +{-# LANGUAGE AllowAmbiguousTypes #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE FunctionalDependencies #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TypeApplications #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE UndecidableInstances #-} + +{-| +Module : Data.Generic.HKD.Position +Description : Manipulate HKD structures using positional indices. +Copyright : (c) Tom Harding, 2019 +License : MIT +Maintainer : tom.harding@habito.com +Stability : experimental +-} +module Data.Generic.HKD.Position + ( HasPosition' (..) + ) where + +import Data.Coerce (Coercible, coerce) +import Data.Type.Bool (type (&&)) +import Data.Void (Void) +import GHC.Generics +import Data.Generic.HKD.Types (HKD (..), HKD_) +import Data.Kind (Constraint, Type) +import GHC.TypeLits (ErrorMessage (..), Nat, type (+), type (<=?), TypeError) +import qualified Data.GenericLens.Internal as G +import Data.GenericLens.Internal (type (>> import Control.Lens ((^.)) +-- +-- >>> :t mempty @(HKD (Int, String) []) ^. position @1 +-- mempty @(HKD (Int, String) []) ^. position @1 :: [Int] +-- +-- As we're using the wonderful @generic-lens@ library under the hood, we also +-- get some beautiful error messages when things go awry: +-- +-- >>> import Data.Generic.HKD.Construction +-- >>> deconstruct ("Hello", True) ^. position @4 +-- ... +-- ... error: +-- ... • The type ([Char], Bool) does not contain a field at position 4 +-- ... +class HasPosition' (index :: Nat) (f :: Type -> Type) (structure :: Type) (focus :: Type) + | index f structure -> focus where + position :: G.Lens' (HKD structure f) (f focus) + +data HasTotalPositionPSym :: Nat -> (G.TyFun (Type -> Type) (Maybe Type)) +type instance G.Eval (HasTotalPositionPSym t) tt = G.HasTotalPositionP t tt + +instance + ( Generic structure + , ErrorUnless index structure (0 HasPosition' index f structure focus where + position = coerced . glens + where + glens :: G.Lens' (CRep f structure Void) (f focus) + glens = G.ravel (G.glens @(HasTotalPositionPSym index)) + + coerced :: G.Lens' (HKD structure f) (CRep f structure Void) + coerced f = fmap coerce . f . coerce + +-- Again: to be imported from generic-lens. + +type family ErrorUnless (i :: Nat) (s :: Type) (hasP :: Bool) :: Constraint where + ErrorUnless i s 'False + = TypeError + ( 'Text "The type " + ':<>: 'ShowType s + ':<>: 'Text " does not contain a field at position " + ':<>: 'ShowType i + ) + + ErrorUnless _ _ 'True + = () + +type CRep (f :: Type -> Type) (structure :: Type) + = Fst (Traverse (HKD_ f structure) 1) + +type family Fst (p :: (a, b)) :: a where + Fst '(a, b) = a + +type family Traverse (a :: Type -> Type) (n :: Nat) :: (Type -> Type, Nat) where + Traverse (M1 mt m s) n + = Traverse1 (M1 mt m) (Traverse s n) + Traverse (l :+: r) n + = '(Fst (Traverse l n) :+: Fst (Traverse r n), n) + Traverse (l :*: r) n + = TraverseProd (:*:) (Traverse l n) r + Traverse (K1 _ p) n + = '(K1 (G.Pos n) p, n + 1) + Traverse U1 n + = '(U1, n) + +type family Traverse1 (w :: (Type -> Type) -> (Type -> Type)) (z :: (Type -> Type, Nat)) :: (Type -> Type, Nat) where + Traverse1 w '(i, n) = '(w i, n) + +type family TraverseProd (c :: (Type -> Type) -> (Type -> Type) -> (Type -> Type)) (a :: (Type -> Type, Nat)) (r :: Type -> Type) :: (Type -> Type, Nat) where + TraverseProd w '(i, n) r = Traverse1 (w i) (Traverse r n) diff --git a/src/Data/Generic/HKD/Types.hs b/src/Data/Generic/HKD/Types.hs new file mode 100644 --- /dev/null +++ b/src/Data/Generic/HKD/Types.hs @@ -0,0 +1,317 @@ +{-# OPTIONS_HADDOCK not-home #-} + +{-# LANGUAGE AllowAmbiguousTypes #-} +{-# LANGUAGE ConstraintKinds #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE FunctionalDependencies #-} +{-# LANGUAGE InstanceSigs #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TypeApplications #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE TypeFamilyDependencies #-} +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE UndecidableInstances #-} + +{-| +Module : Data.Generic.HKD.Types +Description : Type declarations for the HKD structure. +Copyright : (c) Tom Harding, 2019 +License : MIT +Maintainer : tom.harding@habito.com +Stability : experimental +-} +module Data.Generic.HKD.Types + ( HKD (..) + + , HKD_ + , GHKD_ + ) where + +import Data.Barbie (ConstraintsB (..), FunctorB (..), ProductB (..), ProductBC (..), TraversableB (..)) +import Data.Barbie.Constraints (Dict (..)) +import Data.Function (on) +import Data.Functor.Product (Product (..)) +import Data.Kind (Constraint, Type) +import Data.Proxy (Proxy (..)) +import Data.Void (Void) +import GHC.Generics +import GHC.TypeLits (KnownSymbol, symbolVal) +import Test.QuickCheck.Arbitrary (Arbitrary (..), CoArbitrary (..)) +import Test.QuickCheck.Function (Function (..), functionMap) + +-- | Higher-kinded data (HKD) is the design pattern in which every field in our +-- type is wrapped in some functor @f@: +-- +-- @ +-- data User f +-- = User +-- { name :: f String +-- , age :: f Int +-- } +-- @ +-- +-- Depending on the functor, we can get different behaviours: with 'Maybe', we +-- get a partial structure; with 'Validation', we get a piecemeal validator; +-- and so on. The @HKD@ newtype allows us to lift any type into an HKD-style +-- API via its generic representation. +-- +-- >>> :set -XDeriveGeneric -XTypeApplications +-- >>> :{ +-- data User +-- = User { name :: String, age :: Int } +-- deriving Generic +-- :} +-- +-- The @HKD@ type is indexed by our choice of functor and the structure we're +-- lifting. In other words, we can define a synonym for our behaviour: +-- +-- >>> import Data.Monoid (Last (..)) +-- >>> type Partial a = HKD a Last +-- +-- ... and then we're ready to go! +-- +-- >>> mempty @(Partial User) +-- User {name = Last {getLast = Nothing}, age = Last {getLast = Nothing}} +-- +-- >>> mempty @(HKD (Int, Bool) []) +-- (,) [] [] +newtype HKD (structure :: Type) (f :: Type -> Type) + = HKD { runHKD :: HKD_ f structure Void } + +------------------------------------------------------------------------------- + +-- | Calculate the "partial representation" of a type. +type HKD_ (f :: Type -> Type) (structure :: Type) + = GHKD_ f (Rep structure) + +-- | Calculate the "partial representation" of a generic rep. +type family GHKD_ (f :: Type -> Type) (rep :: Type -> Type) + = (output :: Type -> Type) | output -> f rep where + GHKD_ f (M1 index meta inner) = M1 index meta (GHKD_ f inner) + GHKD_ f (left :*: right) = GHKD_ f left :*: GHKD_ f right + GHKD_ f (K1 index value) = K1 index (f value) + GHKD_ f (left :+: right) = GHKD_ f left :+: GHKD_ f right + +------------------------------------------------------------------------------- + +instance (Eq tuple, Generic xs, Tuple f xs tuple) + => Eq (HKD xs f) where + (==) = (==) `on` toTuple + +instance (Ord tuple, Generic xs, Tuple f xs tuple) + => Ord (HKD xs f) where + compare = compare `on` toTuple + +instance (Semigroup tuple, Generic xs, Tuple f xs tuple) + => Semigroup (HKD xs f) where + x <> y = fromTuple (toTuple x <> toTuple y) + +instance (Monoid tuple, Generic xs, Tuple f xs tuple) + => Monoid (HKD xs f) where + mempty = fromTuple mempty + +------------------------------------------------------------------------------- + +instance (Arbitrary tuple, GToTuple (HKD_ f structure) tuple) + => Arbitrary (HKD structure f) where + arbitrary = fmap (HKD . gfromTuple) arbitrary + +instance (CoArbitrary tuple, GToTuple (HKD_ f structure) tuple) + => CoArbitrary (HKD structure f) where + coarbitrary (HKD x) = coarbitrary (gtoTuple x) + +instance (Generic structure, Function tuple, Tuple f structure tuple) + => Function (HKD structure f) where + function = functionMap toTuple fromTuple + +------------------------------------------------------------------------------- + +class GShow (named :: Bool) (rep :: Type -> Type) where + gshow :: rep p -> String + +instance GShow named inner => GShow named (D1 meta inner) where + gshow = gshow @named . unM1 + +instance (GShow 'True inner, KnownSymbol name) + => GShow any (C1 ('MetaCons name fixity 'True) inner) where + gshow (M1 x) = symbolVal (Proxy @name) <> " {" <> gshow @'True x <> "}" + +instance (GShow 'False inner, KnownSymbol name) + => GShow any (C1 ('MetaCons name fixity 'False) inner) where + gshow (M1 x) = symbolVal (Proxy @name) <> " " <> gshow @'False x + +instance (GShow 'True left, GShow 'True right) + => GShow 'True (left :*: right) where + gshow (left :*: right) = gshow @'True left <> ", " <> gshow @'True right + +instance (GShow 'False left, GShow 'False right) + => GShow 'False (left :*: right) where + gshow (left :*: right) = gshow @'False left <> " " <> gshow @'False right + +instance (GShow 'True inner, KnownSymbol field) + => GShow 'True (S1 ('MetaSel ('Just field) i d c) inner) where + gshow (M1 inner) = symbolVal (Proxy @field) <> " = " <> gshow @'True inner + +instance GShow 'False inner => GShow 'False (S1 meta inner) where + gshow (M1 inner) = gshow @'False inner + +instance (Show (f inner)) => GShow named (K1 R (f inner)) where + gshow (K1 x) = show x + +instance (Generic structure, GShow 'True (HKD_ f structure)) + => Show (HKD structure f) where + show (HKD x) = gshow @'True x + +------------------------------------------------------------------------------- + +class Tuple (f :: Type -> Type) (structure :: Type) (tuple :: Type) + | f structure -> tuple where + toTuple :: HKD structure f -> tuple + fromTuple :: tuple -> HKD structure f + +class Function tuple => GToTuple (rep :: Type -> Type) (tuple :: Type) + | rep -> tuple where + gfromTuple :: tuple -> rep p + gtoTuple :: rep p -> tuple + +instance GToTuple inner tuple + => GToTuple (M1 index meta inner) tuple where + gfromTuple = M1 . gfromTuple + gtoTuple = gtoTuple . unM1 + +instance (GToTuple left left', GToTuple right right') + => GToTuple (left :*: right) (left', right') where + gfromTuple (x, y) = gfromTuple x :*: gfromTuple y + gtoTuple (x :*: y) = (gtoTuple x, gtoTuple y) + +instance Function inner => GToTuple (K1 index inner) inner where + gfromTuple = K1 + gtoTuple = unK1 + +instance (Generic structure, GToTuple (HKD_ f structure) tuple) + => Tuple f structure tuple where + toTuple = gtoTuple . runHKD + fromTuple = HKD . gfromTuple + +------------------------------------------------------------------------------- + +class GFunctorB (rep :: Type -> Type) where + gbmap :: (forall a. f a -> g a) -> GHKD_ f rep p -> GHKD_ g rep p + +instance GFunctorB inner => GFunctorB (M1 index meta inner) where + gbmap f = M1 . gbmap @inner f . unM1 + +instance (GFunctorB left, GFunctorB right) + => GFunctorB (left :*: right) where + gbmap f (left :*: right) = gbmap @left f left :*: gbmap @right f right + +instance GFunctorB (K1 index inner) where + gbmap f (K1 x) = K1 (f x) + +instance GFunctorB (Rep structure) => FunctorB (HKD structure) where + bmap f = HKD . gbmap @(Rep structure) f . runHKD + +------------------------------------------------------------------------------- + +class GTraversableB (rep :: Type -> Type) where + gbtraverse + :: Applicative t + => (forall a. f a -> t (g a)) + -> GHKD_ f rep p -> t (GHKD_ g rep p) + +instance GTraversableB inner => GTraversableB (M1 index meta inner) where + gbtraverse f = fmap M1 . gbtraverse @inner f . unM1 + +instance (GTraversableB left, GTraversableB right) + => GTraversableB (left :*: right) where + gbtraverse f (left :*: right) + = (:*:) <$> gbtraverse @left f left + <*> gbtraverse @right f right + +instance GTraversableB (K1 index inner) where + gbtraverse f (K1 x) = fmap K1 (f x) + +instance (FunctorB (HKD structure), GTraversableB (Rep structure)) + => TraversableB (HKD structure) where + btraverse f = fmap HKD . gbtraverse @(Rep structure) f . runHKD + +------------------------------------------------------------------------------- + +class GProductB (rep :: Type -> Type) where + gbprod :: GHKD_ f rep p -> GHKD_ g rep p -> GHKD_ (f `Product` g) rep p + gbuniq :: (forall a. f a) -> GHKD_ f rep p + +instance GProductB inner => GProductB (M1 index meta inner) where + gbprod (M1 x) (M1 y) = M1 (gbprod @inner x y) + gbuniq zero = M1 (gbuniq @inner zero) + +instance (GProductB left, GProductB right) + => GProductB (left :*: right) where + gbprod (leftX :*: rightX) (leftY :*: rightY) + = gbprod @left leftX leftY :*: gbprod @right rightX rightY + + gbuniq zero + = gbuniq @left zero :*: gbuniq @right zero + +instance GProductB (K1 index inner) where + gbprod (K1 x) (K1 y) = K1 (Pair x y) + gbuniq zero = K1 zero + +instance (FunctorB (HKD structure), GProductB (Rep structure)) + => ProductB (HKD structure) where + bprod (HKD x) (HKD y) = HKD (gbprod @(Rep structure) x y) + buniq zero = HKD (gbuniq @(Rep structure) zero) + +------------------------------------------------------------------------------- + +class GConstraintsB (rep :: Type -> Type) where + type GAllB (c :: Type -> Constraint) rep :: Constraint + + gbaddDicts :: GAllB c rep => GHKD_ f rep p -> GHKD_ (Dict c `Product` f) rep p + +instance GConstraintsB inner => GConstraintsB (M1 index meta inner) where + type GAllB c (M1 index meta inner) = GAllB c inner + + gbaddDicts (M1 x) = M1 (gbaddDicts @inner x) + +instance (GConstraintsB left, GConstraintsB right) + => GConstraintsB (left :*: right) where + type GAllB c (left :*: right) = (GAllB c left, GAllB c right) + + gbaddDicts (left :*: right) + = gbaddDicts @left left :*: gbaddDicts @right right + +instance c inner => GConstraintsB (K1 index inner) where + type GAllB c (K1 index inner) = c inner + + gbaddDicts (K1 x) + = K1 (Pair Dict x) + +instance (FunctorB (HKD structure), GConstraintsB (Rep structure)) + => ConstraintsB (HKD structure) where + type AllB c (HKD structure) = GAllB c (Rep structure) + baddDicts (HKD x) = HKD (gbaddDicts @(Rep structure) x) + +------------------------------------------------------------------------------- + +class GProductBC (rep :: Type -> Type) where + gbdicts :: GAllB c rep => GHKD_ (Dict c) rep p + +instance GProductBC inner => GProductBC (M1 index meta inner) where + gbdicts = M1 gbdicts + +instance (GProductBC left, GProductBC right) + => GProductBC (left :*: right) where + gbdicts = gbdicts :*: gbdicts + +instance GProductBC (K1 index inner) where + gbdicts = K1 Dict + +instance + ( ProductB (HKD structure) + , ConstraintsB (HKD structure) + , GProductBC (Rep structure) + ) => ProductBC (HKD structure) where + bdicts = HKD gbdicts diff --git a/test/Main.hs b/test/Main.hs new file mode 100644 --- /dev/null +++ b/test/Main.hs @@ -0,0 +1,195 @@ +{-# LANGUAGE AllowAmbiguousTypes #-} +{-# LANGUAGE BlockArguments #-} +{-# LANGUAGE ConstraintKinds #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE DeriveGeneric #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE MonoLocalBinds #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TypeApplications #-} +module Main where + +import Control.Lens (Lens', (.~), (^.)) +import Data.Function ((&), on) +import Data.Functor.Identity (Identity (..)) +import Data.Generic.HKD +import Data.Monoid (Last (..)) +import GHC.Generics +import Test.DocTest +import Test.Hspec +import Test.QuickCheck +import Test.QuickCheck.Arbitrary + +type Partial a = HKD a Last +type WTF a = HKD a [] + +main :: IO () +main = do + doctest ["src", "test"] + + hspec do + describe "Unnamed" do + eq @(Partial Triple) + ord @(Partial Triple) + semigroup @(Partial Triple) + idempotent @(Partial Triple) + monoid @(Partial Triple) + + eq @(WTF Triple) + ord @(WTF Triple) + semigroup @(WTF Triple) + monoid @(WTF Triple) + + lens @(Partial Triple) (position @1) + lens @(Partial Triple) (position @2) + lens @(Partial Triple) (position @3) + + lens @(WTF Triple) (position @1) + lens @(WTF Triple) (position @2) + lens @(WTF Triple) (position @3) + + describe "Named" do + eq @(Partial Person) + ord @(Partial Person) + semigroup @(Partial Person) + idempotent @(Partial Person) + monoid @(Partial Person) + + eq @(WTF Person) + ord @(WTF Person) + semigroup @(WTF Person) + monoid @(WTF Person) + + lens @(WTF Person) (position @1) + lens @(WTF Person) (position @2) + lens @(WTF Person) (position @3) + + lens @(Partial Person) (field @"name") + lens @(Partial Person) (field @"age") + lens @(Partial Person) (field @"likesDogs") + + lens @(WTF Person) (field @"name") + lens @(WTF Person) (field @"age") + lens @(WTF Person) (field @"likesDogs") + +------------------------------------------------------------------------------- + +data Person + = Person + { name :: String + , age :: Int + , likesDogs :: Bool + } + deriving (Eq, Generic, Ord, Show) + +data Triple + = Triple String Bool () + deriving (Eq, Generic, Ord, Show) + +instance Arbitrary Person where + arbitrary = Person <$> arbitrary <*> arbitrary <*> arbitrary + +instance CoArbitrary Person +instance Function Person + +instance Arbitrary Triple where + arbitrary = Triple <$> arbitrary <*> arbitrary <*> arbitrary + +instance CoArbitrary Triple +instance Function Triple + +------------------------------------------------------------------------------- + +eq + :: forall a. (Arbitrary a, CoArbitrary a, Eq a, Function a, Show a) + => SpecWith () + +eq = describe "Eq" do + it "is reflexive" $ property \(x :: a) -> + x == x + + it "is symmetric" $ property \(x :: a) y -> + (x == y) == (y == x) + + it "is transitive" $ property \(x :: a) y z -> + not (x == y && y == z) || (x == z) + + it "substitutes" $ property \(x :: a) y (Fun _ f :: Fun a Int) -> + not (x == y) || (f x == f y) + +ord :: forall a. (Arbitrary a, Ord a, Show a) => SpecWith () +ord = describe "Ord" do + it "is transitive" $ property \(x :: a) y z -> + not (x <= y && y <= z) || (x <= z) + + it "is reflexive" $ property \(x :: a) -> + x <= x + + it "is antisymmetric" $ property \(x :: a) y -> + not (x <= y && y <= x) || (x == y) + +semigroup :: forall a. (Arbitrary a, Eq a, Semigroup a, Show a) => SpecWith () +semigroup = describe "Semigroup" do + it "is associative" $ property \(x :: a) y z -> + x <> (y <> z) == (x <> y) <> z + +idempotent :: forall a. (Arbitrary a, Eq a, Semigroup a, Show a) => SpecWith () +idempotent = describe "Idempotence" do + it "has right idempotence" $ property \(x :: a) y -> + x <> y <> y == x <> y + +monoid :: forall a. (Arbitrary a, Eq a, Monoid a, Show a) => SpecWith () +monoid = describe "Monoid" do + it "has left identity" $ property \(x :: a) -> mempty <> x == x + it "has right identity" $ property \(x :: a) -> x <> mempty == x + +lens + :: forall s a + . ( Arbitrary s, Arbitrary a + , Show s, Show a + , Eq a, Eq s + ) + => Lens' s a + -> SpecWith () + +lens l = describe "Lens laws" do + it "- get l . set l x == x" $ property \(s :: s) (a :: a) -> + (s & l .~ a) ^. l == a + + it "- set l (get l s) == s" $ property \(s :: s) -> + (s & l .~ (s ^. l)) == s + + it "- set l b . set l a == set l b" $ property \(s :: s) (a :: a) (b :: a) -> + (s & l .~ a & l .~ b) == (s & l .~ b) + +------------------------------------------------------------------------------- + +partials + :: forall a + . ( Arbitrary a + , Show a + , Ord a + , Generic a + , Construct Last a + , Construct [] a + , Ord (Partial a) + , Ord (WTF a) + ) + => SpecWith () + +partials = describe "HKD" do + describe "Eq" do + it "is monotonic with respect to ordering (Partial)" + $ property \(x :: a) y -> (x <= y) == ((<=) `on` deconstruct @Last) x y + + it "is monotonic with respect to ordering (WTF)" + $ property \(x :: a) y -> (x <= y) == ((<=) `on` deconstruct @[]) x y + + it "round-trips" + $ property \(x :: a) -> + construct (deconstruct @Last x) == pure x + + it "round-trips" + $ property \(x :: a) -> + construct (deconstruct @[] x) == pure x