i-am-tom/higgledy
1
1
Fork 0
mirror of https://github.com/i-am-tom/higgledy.git synced 2024-08-17 03:50:23 +03:00
Code Issues Projects Releases Wiki Activity

Use generic-lens directly for position/field

Browse Source 
Turns out, as @kcsongor suspected, we can use generic-lens directly by
exposing a generic rep for our HKD type. All the tests work fine, two
documentation updates. I'm very pleased!
This commit is contained in:
Tom Harding 2019-06-20 21:05:05 +01:00
parent b34a9c707e
commit 81a6ce7b67
5 changed files with 95 additions and 234 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
higgledy.cabal
View File

@ -19,9 +19,7 @@ library
exposed-modules: Data.Generic.HKD
Data.Generic.HKD.Build
Data.Generic.HKD.Construction
Data.Generic.HKD.Field
Data.Generic.HKD.Labels
Data.Generic.HKD.Position
Data.Generic.HKD.Types
-- other-modules:
-- other-extensions:

93
src/Data/Generic/HKD.hs
View File

@ -1,3 +1,9 @@
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE MonoLocalBinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-|
Module : Data.Generic.HKD
Description : A generic-based HKD decorator for ADTs.
@ -8,11 +14,94 @@ Stability : experimental
-}
module Data.Generic.HKD
( module Exports
, position
, field
) where
import Data.Generic.HKD.Build as Exports
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
import qualified Data.Generics.Internal.VL.Lens as G
import qualified Data.Generics.Product 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 -XTypeApplications
-- >>> 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 HKD User Last does not contain a field named 'oops'.
-- ...
field
:: forall field f structure inner
. G.HasField' field (HKD structure f) (f inner)
=> G.Lens' (HKD structure f) (f inner)
field
= G.field' @field
-- | 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 HKD User Last does not contain a field named 'oops'.
-- ...
position
:: forall index f structure inner
. G.HasPosition' index (HKD structure f) (f inner)
=> G.Lens' (HKD structure f) (f inner)
position
= G.position' @index

108
src/Data/Generic/HKD/Field.hs
View File

@ -1,108 +0,0 @@
{-# 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 '[] '[] _)
= ()

118
src/Data/Generic/HKD/Position.hs
View File

@ -1,118 +0,0 @@
{-# 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 qualified Data.Generics.Internal.VL.Lens as G
-- | Product types /without/ named fields can't be addressed by field name (for
-- very obvious reason), so we instead need to address them with their
-- "position" index. This is a one-indexed type-applied natural:
--
-- >>> 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 <? index && index <=? G.Size (Rep structure))
, G.GLens' (HasTotalPositionPSym index) (CRep f structure) (f focus)
, G.HasTotalPositionP index (CRep f structure) ~ 'Just (f focus)
, G.HasTotalPositionP index (CRep f (G.Indexed structure)) ~ 'Just (f' focus')
, Coercible (HKD structure f) (CRep f structure Void)
, structure ~ G.Infer structure (f' focus') (f focus)
) => 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)

8
test/Main.hs
View File

@ -11,13 +11,13 @@
module Main where
import Control.Lens (Lens', (.~), (^.))
import Data.Function ((&), on)
import Data.Generic.HKD
import Data.Monoid (Last (..))
import Data.Barbie
import Data.Barbie.Constraints (Dict)
import Data.Functor.Product (Product (..))
import Data.Function ((&), on)
import Data.Functor.Identity (Identity (..))
import Data.Functor.Product (Product (..))
import Data.Generic.HKD
import Data.Monoid (Last (..))
import GHC.Generics
import Test.DocTest
import Test.Hspec