mirror of
https://github.com/i-am-tom/higgledy.git
synced 2024-09-11 16:16:43 +03:00
Last and Position
Refactoring `position` with a proper error message. Tidied up a /lot/ of the instances using the tuple isomorphism and a change from 'Maybe' to 'Last'.
This commit is contained in:
Tom Harding
parent
3693467412
commit
a84269ab5f
@ -12,6 +12,7 @@ module Data.Partial.Build
|
||||
import Control.Applicative (liftA2)
|
||||
import Control.Lens (Prism', prism')
|
||||
import Data.Kind (Type)
|
||||
import Data.Monoid (Last (..))
|
||||
import Data.Partial.Types (Partial (..), GPartial_)
|
||||
import GHC.Generics
|
||||
|
||||
@ -52,8 +53,8 @@ instance (GHasPartial left, GHasPartial right)
|
||||
gfromPartial (l :*: r) = liftA2 (:*:) (gfromPartial l) (gfromPartial r)
|
||||
|
||||
instance GHasPartial (K1 index inner) where
|
||||
gtoPartial = K1 . Just . unK1
|
||||
gfromPartial = fmap K1 . unK1
|
||||
gtoPartial = K1 . pure . unK1
|
||||
gfromPartial = fmap K1 . getLast . unK1
|
||||
|
||||
instance (Generic structure, GHasPartial (Rep structure))
|
||||
=> HasPartial structure where
|
||||
|
||||
@ -9,6 +9,7 @@ module Data.Partial.Default
|
||||
|
||||
import Data.Kind (Type)
|
||||
import Data.Maybe (fromMaybe)
|
||||
import Data.Monoid (Last (..))
|
||||
import Data.Partial.Types (Partial (..), GPartial_)
|
||||
import GHC.Generics
|
||||
|
||||
@ -50,7 +51,7 @@ instance (GDefaults left, GDefaults right)
|
||||
|
||||
instance GDefaults (K1 index inner) where
|
||||
gdefaults (K1 inner) (K1 partial)
|
||||
= K1 (fromMaybe inner partial)
|
||||
= K1 (fromMaybe inner (getLast partial))
|
||||
|
||||
instance (Generic structure, GDefaults (Rep structure))
|
||||
=> Defaults structure where
|
||||
|
||||
@ -8,11 +8,14 @@
|
||||
{-# LANGUAGE TypeFamilies #-}
|
||||
{-# LANGUAGE TypeOperators #-}
|
||||
{-# LANGUAGE UndecidableInstances #-}
|
||||
module Data.Partial.Field where
|
||||
module Data.Partial.Field
|
||||
( HasField' (..)
|
||||
) where
|
||||
|
||||
import Control.Lens (Lens', dimap)
|
||||
import Data.Partial.Types (Partial (..), Partial_)
|
||||
import Data.Kind (Type)
|
||||
import Data.Monoid (Last (..))
|
||||
import Data.Partial.Types (Partial (..), Partial_)
|
||||
import GHC.Generics
|
||||
import GHC.TypeLits (ErrorMessage (..), Symbol, TypeError)
|
||||
|
||||
@ -45,8 +48,8 @@ class HasField' (field :: Symbol) (structure :: Type) (focus :: Type)
|
||||
-------------------------------------------------------------------------------
|
||||
|
||||
type family Field (field :: Symbol) (rep :: Type -> Type) :: Maybe Type where
|
||||
Field s (S1 (_ ('Just s) _ _ _) (_ (Maybe x))) = 'Just x
|
||||
Field s (M1 _ _ xs) = Field s xs
|
||||
Field s (S1 (_ ('Just s) _ _ _) (_ (Last x))) = 'Just x
|
||||
Field s (M1 _ _ xs) = Field s xs
|
||||
|
||||
Field s (l :*: r) = Field s l <|> Field s r
|
||||
Field _ _ = 'Nothing
|
||||
@ -63,8 +66,8 @@ instance GHasField' field inner focus
|
||||
=> GHasField' field (M1 index meta inner) focus where
|
||||
gfield = dimap unM1 (fmap M1) . gfield @field
|
||||
|
||||
instance GHasField' field (K1 index (Maybe focus)) focus where
|
||||
gfield = dimap unK1 (fmap K1)
|
||||
instance GHasField' field (K1 index (Last focus)) focus where
|
||||
gfield = dimap (getLast . unK1) (fmap (K1 . Last))
|
||||
|
||||
instance GHasFieldProduct (Field field left) field (left :*: right) focus
|
||||
=> GHasField' field (left :*: right) focus where
|
||||
|
||||
@ -8,37 +8,66 @@
|
||||
{-# LANGUAGE TypeFamilies #-}
|
||||
{-# LANGUAGE TypeOperators #-}
|
||||
{-# LANGUAGE UndecidableInstances #-}
|
||||
module Data.Partial.Position where
|
||||
module Data.Partial.Position
|
||||
( HasPosition' (..)
|
||||
) where
|
||||
|
||||
import GHC.Generics
|
||||
import Control.Lens (Lens')
|
||||
import Control.Lens (Lens', dimap)
|
||||
import Data.Kind (Type)
|
||||
import Data.Monoid (Last (..))
|
||||
import Data.Partial.Types (Partial (..), Partial_)
|
||||
import GHC.TypeLits (Nat, type (<=?), type (+), type (-))
|
||||
import GHC.Generics
|
||||
import GHC.TypeLits (ErrorMessage (..), Nat, TypeError, type (<=?), type (+), type (-))
|
||||
|
||||
-- | For types /without/ named fields, our lens must be positional. This works
|
||||
-- just the same as 'field', but we type-apply the index (starting at @1@).
|
||||
-- | Taking another cue from @generic-lens@, we can lens into partial product
|
||||
-- types whose fields /aren't/ named using a positional index.
|
||||
--
|
||||
-- >>> import Control.Lens
|
||||
-- >>> import Data.Partial.Build
|
||||
--
|
||||
-- We address the positions using a type application:
|
||||
--
|
||||
-- >>> toPartial ("Hello", True) ^. position @1
|
||||
-- Just "Hello"
|
||||
--
|
||||
-- >>> mempty @(Partial (Int, String, Bool)) ^. position @3
|
||||
-- Nothing
|
||||
--
|
||||
-- >>> toPartial ("Hello", True) ^. position @4
|
||||
-- ...
|
||||
-- ... ([Char], Bool) has no position #4!
|
||||
-- ...
|
||||
class HasPosition' (index :: Nat) (structure :: Type) (focus :: Type)
|
||||
| index structure -> focus where
|
||||
position :: Lens' (Partial structure) (Maybe focus)
|
||||
|
||||
-------------------------------------------------------------------------------
|
||||
|
||||
type family Position (index :: Nat) (rep :: Type -> Type) :: Maybe Type where
|
||||
Position 1 (K1 _ (Maybe inner)) = 'Just inner
|
||||
Position _ (K1 _ _ ) = 'Nothing
|
||||
Position 1 (K1 _ (Last x)) = 'Just x
|
||||
Position _ (K1 _ _ ) = 'Nothing
|
||||
|
||||
Position count (M1 index meta inner)
|
||||
= Position count inner
|
||||
Position n (M1 _ _ x)
|
||||
= Position n x
|
||||
|
||||
Position count (left :*: right)
|
||||
= Position_ (Count left <=? count) count left right
|
||||
Position n (l :*: r)
|
||||
= Position_ (n <=? Count l) n l r
|
||||
|
||||
type family Count (rep :: Type -> Type) :: Nat where
|
||||
Count (left :*: right) = Count left + Count right
|
||||
Count _ = 1
|
||||
|
||||
type family Position_ (isLeft :: Bool) (count :: Nat) (left :: Type -> Type) (right :: Type -> Type) :: Maybe Type where
|
||||
Position_ 'True count left _ = Position count left
|
||||
Position_ 'False count _ right = Position count right
|
||||
type family Position_
|
||||
(isLeft :: Bool)
|
||||
(count :: Nat)
|
||||
(left :: Type -> Type)
|
||||
(right :: Type -> Type) :: Maybe Type
|
||||
where
|
||||
Position_ 'True count left _
|
||||
= Position count left
|
||||
|
||||
Position_ 'False count left right
|
||||
= Position (count - Count left) right
|
||||
|
||||
class GHasPosition' (index :: Nat) (rep :: Type -> Type) (focus :: Type)
|
||||
| index rep -> focus where
|
||||
@ -46,8 +75,7 @@ class GHasPosition' (index :: Nat) (rep :: Type -> Type) (focus :: Type)
|
||||
|
||||
instance GHasPosition' count inner focus
|
||||
=> GHasPosition' count (M1 index meta inner) focus where
|
||||
gposition = go . gposition @count
|
||||
where go f = fmap M1 . f . unM1
|
||||
gposition = dimap unM1 (fmap M1) . gposition @count
|
||||
|
||||
class GHasPositionProduct
|
||||
(goal :: Maybe Type)
|
||||
@ -71,11 +99,29 @@ instance (GHasPosition' (count - Count left) right focus)
|
||||
gpositionProduct = go . gposition @(count - Count left)
|
||||
where go f (left :*: right) = fmap (left :*:) (f right)
|
||||
|
||||
instance any ~ focus => GHasPosition' 1 (K1 index (Maybe any)) focus where
|
||||
gposition f = fmap K1 . f . unK1
|
||||
instance any ~ focus => GHasPosition' 1 (K1 index (Last any)) focus where
|
||||
gposition = dimap (getLast . unK1) (fmap (K1 . Last))
|
||||
|
||||
instance (Generic structure, GHasPosition' index (Partial_ structure) focus)
|
||||
type HasPosition_ (position :: Nat) (structure :: Type)
|
||||
= AssertHasPosition position structure (Position position (Partial_ structure))
|
||||
|
||||
type family AssertHasPosition
|
||||
(position :: Nat)
|
||||
(structure :: Type)
|
||||
(goal :: Maybe Type) where
|
||||
AssertHasPosition _ _ ('Just xs) = xs
|
||||
AssertHasPosition position structure 'Nothing = TypeError
|
||||
( 'ShowType structure
|
||||
':<>: 'Text " has no position #"
|
||||
':<>: 'ShowType position
|
||||
':<>: 'Text "!"
|
||||
)
|
||||
|
||||
instance
|
||||
( Generic structure
|
||||
, GHasPosition' index (Partial_ structure) focus
|
||||
, HasPosition_ index structure ~ focus
|
||||
)
|
||||
=> HasPosition' index structure focus where
|
||||
position = go . gposition @index
|
||||
where go f (Partial inner) = fmap Partial (f inner)
|
||||
position = dimap runPartial (fmap Partial) . gposition @index
|
||||
|
||||
|
||||
@ -1,8 +1,6 @@
|
||||
{-# LANGUAGE AllowAmbiguousTypes #-}
|
||||
{-# LANGUAGE DataKinds #-}
|
||||
{-# LANGUAGE FlexibleContexts #-}
|
||||
{-# LANGUAGE FlexibleInstances #-}
|
||||
{-# LANGUAGE KindSignatures #-}
|
||||
{-# LANGUAGE FunctionalDependencies #-}
|
||||
{-# LANGUAGE ScopedTypeVariables #-}
|
||||
{-# LANGUAGE TypeApplications #-}
|
||||
@ -11,13 +9,13 @@
|
||||
{-# LANGUAGE UndecidableInstances #-}
|
||||
module Data.Partial.Types where
|
||||
|
||||
import Control.Applicative ((<|>), empty)
|
||||
import Data.Monoid (Last (..))
|
||||
import Data.Function (on)
|
||||
import Data.Kind (Type)
|
||||
import Data.Proxy (Proxy (..))
|
||||
import Data.Void (Void)
|
||||
import GHC.Generics
|
||||
import GHC.TypeLits (KnownSymbol, symbolVal)
|
||||
import Test.QuickCheck (Gen)
|
||||
import Test.QuickCheck.Arbitrary (Arbitrary (..), CoArbitrary (..))
|
||||
import Test.QuickCheck.Function (Function (..), functionMap)
|
||||
|
||||
@ -38,7 +36,7 @@ type family GPartial_ (rep :: Type -> Type) :: Type -> Type where
|
||||
= GPartial_ left :*: GPartial_ right
|
||||
|
||||
GPartial_ (K1 index value)
|
||||
= K1 index (Maybe value)
|
||||
= K1 index (Last value)
|
||||
|
||||
GPartial_ (left :+: right)
|
||||
= GPartial_ left :+: GPartial_ right
|
||||
@ -46,128 +44,27 @@ type family GPartial_ (rep :: Type -> Type) :: Type -> Type where
|
||||
GPartial_ U1 = U1
|
||||
GPartial_ V1 = V1
|
||||
|
||||
-- | Partial structures have an 'Eq' instance providing that all the
|
||||
-- parameters' types have an 'Eq' instance as well.
|
||||
class GEq (rep :: Type -> Type) where
|
||||
geq :: rep p -> rep q -> Bool
|
||||
instance (Eq tuple, Generic xs, Tuple xs tuple) => Eq (Partial xs) where
|
||||
(==) = (==) `on` toTuple
|
||||
|
||||
instance GEq inner => GEq (M1 index meta inner) where
|
||||
geq (M1 x) (M1 y) = geq x y
|
||||
instance (Ord tuple, Generic xs, Tuple xs tuple) => Ord (Partial xs) where
|
||||
compare = compare `on` toTuple
|
||||
|
||||
instance (GEq left, GEq right) => GEq (left :*: right) where
|
||||
geq (leftX :*: rightX) (leftY :*: rightY)
|
||||
= geq leftX leftY && geq rightX rightY
|
||||
instance (Semigroup tuple, Generic xs, Tuple xs tuple)
|
||||
=> Semigroup (Partial xs) where
|
||||
x <> y = fromTuple (toTuple x <> toTuple y)
|
||||
|
||||
instance Eq parameter => GEq (K1 index (Maybe parameter)) where
|
||||
geq (K1 x) (K1 y) = x == y
|
||||
instance (Monoid tuple, Generic xs, Tuple xs tuple)
|
||||
=> Monoid (Partial xs) where
|
||||
mempty = fromTuple mempty
|
||||
|
||||
instance (Generic structure, GEq (Partial_ structure))
|
||||
=> Eq (Partial structure) where
|
||||
Partial x == Partial y = geq x y
|
||||
|
||||
-- | Similarly, partial structures have an ordering if all parameters are also
|
||||
-- instances of 'Ord'. Note that an "empty" parameter is /less than/ a
|
||||
-- completed parameter due to the 'Ord' instance of 'Maybe'.
|
||||
class GEq rep => GOrd (rep :: Type -> Type) where
|
||||
gcompare :: rep p -> rep q -> Ordering
|
||||
|
||||
instance GOrd inner => GOrd (M1 index meta inner) where
|
||||
gcompare (M1 x) (M1 y) = gcompare x y
|
||||
|
||||
instance (GOrd left, GOrd right) => GOrd (left :*: right) where
|
||||
gcompare (leftX :*: rightX) (leftY :*: rightY)
|
||||
= gcompare leftX leftY <> gcompare rightX rightY
|
||||
|
||||
instance Ord parameter => GOrd (K1 index (Maybe parameter)) where
|
||||
gcompare (K1 x) (K1 y) = compare x y
|
||||
|
||||
instance (Generic structure, GOrd (Partial_ structure))
|
||||
=> Ord (Partial structure) where
|
||||
compare (Partial x) (Partial y) = gcompare x y
|
||||
|
||||
-- | Partial structures form a semigroup by taking the (right-biased) union of
|
||||
-- partial data.
|
||||
class GSemigroup (rep :: Type -> Type) where
|
||||
gmappend :: rep p -> rep q -> rep r
|
||||
|
||||
instance GSemigroup inner => GSemigroup (M1 index meta inner) where
|
||||
gmappend (M1 x) (M1 y) = M1 (gmappend x y)
|
||||
|
||||
instance (GSemigroup left, GSemigroup right)
|
||||
=> GSemigroup (left :*: right) where
|
||||
gmappend (leftX :*: rightX) (leftY :*: rightY)
|
||||
= gmappend leftX leftY :*: gmappend rightX rightY
|
||||
|
||||
instance GSemigroup (K1 index (Maybe anything)) where
|
||||
gmappend (K1 x) (K1 y) = K1 (y <|> x)
|
||||
|
||||
instance GSemigroup U1 where
|
||||
gmappend U1 U1 = U1
|
||||
|
||||
instance (Generic structure, GSemigroup (Partial_ structure))
|
||||
=> Semigroup (Partial structure) where
|
||||
Partial x <> Partial y
|
||||
= Partial (gmappend x y)
|
||||
|
||||
-- | Partial structures form a monoid if the unit element is a partial
|
||||
-- structure with no completed fields.
|
||||
class GSemigroup rep => GMonoid (rep :: Type -> Type) where
|
||||
gmempty :: rep p
|
||||
|
||||
instance (GMonoid inner, GSemigroup (M1 index meta inner))
|
||||
=> GMonoid (M1 index meta inner) where
|
||||
gmempty = M1 gmempty
|
||||
|
||||
instance (GMonoid left, GMonoid right, GSemigroup (left :*: right))
|
||||
=> GMonoid (left :*: right) where
|
||||
gmempty = gmempty :*: gmempty
|
||||
|
||||
instance GSemigroup (K1 index (Maybe anything))
|
||||
=> GMonoid (K1 index (Maybe anything)) where
|
||||
gmempty = K1 empty
|
||||
|
||||
instance GSemigroup U1 => GMonoid U1 where
|
||||
gmempty = U1
|
||||
|
||||
instance (Generic structure, GMonoid (Partial_ structure))
|
||||
=> Monoid (Partial structure) where
|
||||
mempty = Partial gmempty
|
||||
|
||||
-- | If all the components of a structure have an 'Arbitrary' instance, we can
|
||||
-- trivially create arbitrary partial structures.
|
||||
class GArbitrary (rep :: Type -> Type) where
|
||||
garbitrary :: Gen (rep p)
|
||||
|
||||
instance GArbitrary inner => GArbitrary (M1 index meta inner) where
|
||||
garbitrary = fmap M1 garbitrary
|
||||
|
||||
instance (GArbitrary left, GArbitrary right)
|
||||
=> GArbitrary (left :*: right) where
|
||||
garbitrary = (:*:) <$> garbitrary <*> garbitrary
|
||||
|
||||
instance Arbitrary inner => GArbitrary (K1 index inner) where
|
||||
garbitrary = fmap K1 arbitrary
|
||||
|
||||
instance (Generic structure, GArbitrary (Partial_ structure))
|
||||
instance (Arbitrary tuple, GToTuple (Partial_ structure) tuple)
|
||||
=> Arbitrary (Partial structure) where
|
||||
arbitrary = fmap Partial garbitrary
|
||||
arbitrary = fmap (Partial . gfromTuple) arbitrary
|
||||
|
||||
class GCoArbitrary (rep :: Type -> Type) where
|
||||
gcoarbitrary :: rep p -> Gen b -> Gen b
|
||||
|
||||
instance GCoArbitrary inner => GCoArbitrary (M1 index meta inner) where
|
||||
gcoarbitrary (M1 x) = gcoarbitrary x
|
||||
|
||||
instance (GCoArbitrary left, GCoArbitrary right)
|
||||
=> GCoArbitrary (left :*: right) where
|
||||
gcoarbitrary (left :*: right) = gcoarbitrary left . gcoarbitrary right
|
||||
|
||||
instance CoArbitrary inner => GCoArbitrary (K1 index (Maybe inner)) where
|
||||
gcoarbitrary (K1 inner) = coarbitrary inner
|
||||
|
||||
instance (Generic structure, GCoArbitrary (Partial_ structure))
|
||||
instance (CoArbitrary tuple, GToTuple (Partial_ structure) tuple)
|
||||
=> CoArbitrary (Partial structure) where
|
||||
coarbitrary (Partial x) = gcoarbitrary x
|
||||
coarbitrary (Partial x) = coarbitrary (gtoTuple x)
|
||||
|
||||
-- | For complete partial structures, the 'Show' instances should match (though
|
||||
-- there are some edge-cases around, say, rendering of negative numbers).
|
||||
@ -200,8 +97,8 @@ instance (GShow 'True inner, KnownSymbol field)
|
||||
instance GShow 'False inner => GShow 'False (S1 meta inner) where
|
||||
gshow (M1 inner) = gshow @'False inner
|
||||
|
||||
instance Show inner => GShow named (K1 R (Maybe inner)) where
|
||||
gshow (K1 x) = maybe "???" show x
|
||||
instance Show inner => GShow named (K1 R (Last inner)) where
|
||||
gshow (K1 x) = maybe "???" show (getLast x)
|
||||
|
||||
instance (Generic structure, GShow 'True (Partial_ structure))
|
||||
=> Show (Partial structure) where
|
||||
@ -226,6 +123,16 @@ instance Function inner => GToTuple (K1 index inner) inner where
|
||||
gfromTuple = K1
|
||||
gtoTuple = unK1
|
||||
|
||||
class Tuple (structure :: Type) (tuple :: Type)
|
||||
| structure -> tuple where
|
||||
toTuple :: Partial structure -> tuple
|
||||
fromTuple :: tuple -> Partial structure
|
||||
|
||||
instance (Generic structure, GToTuple (Partial_ structure) tuple)
|
||||
=> Tuple structure tuple where
|
||||
toTuple = gtoTuple . runPartial
|
||||
fromTuple = Partial . gfromTuple
|
||||
|
||||
instance (Generic structure, Function tuple, Tuple structure tuple)
|
||||
=> Function (Partial structure) where
|
||||
function = functionMap (gtoTuple . runPartial) (Partial . gfromTuple)
|
||||
function = functionMap toTuple fromTuple
|
||||
|
||||
Loading…
Reference in New Issue
Block a user