Data.Barbie.Internal.Constraints

Documentation

class FunctorB b => ConstraintsB b where

Instances of this class provide means to talk about constraints, both at compile-time, using ConstraintsOf and at run-time, in the form of class instance dictionaries, via adjProof.

A manual definition would look like this:

data T f = A (f Int) (f String) | B (f Bool) (f Int)

instance ConstraintsB T where
  type ConstraintsOf c f T
    = (c (f Int), c (f String), c (f Bool))

  adjProof t = case t of
    A x y -> A (Pair (packDict x) (packDict y))
    B z w -> B (Pair (packDict z) (packDict w))

There is a default implementation of ConstraintsOf for Generic types, so in practice one will simply do:

derive instance Generic T
instance ConstraintsB T

Associated Types

type ConstraintsOf (c :: * -> Constraint) (f :: * -> *) b :: Constraint

ConstraintsOf c f b should contain a constraint c (f x) for each f x occurring in b. E.g.:

ConstraintsOf Show f Barbie = (Show (f String), Show (f Int))

Methods

adjProof :: forall c f. ConstraintsOf c f b => b f -> b (Product (DictOf c f) f)

Adjoint a proof-of-instance to a barbie-type.

adjProof :: forall c f. (CanDeriveGenericInstance b, ConstraintsOfMatchesGenericDeriv c f b, ConstraintsOf c f b) => b f -> b (Product (DictOf c f) f)

Adjoint a proof-of-instance to a barbie-type.

Instances

ConstraintsB b => ConstraintsB (Barbie b)

Defined in Data.Barbie.Internal.Instances

Associated Types

type ConstraintsOf c f (Barbie b) :: Constraint

Methods

adjProof :: ConstraintsOf c f (Barbie b) => Barbie b f -> Barbie b (Product (DictOf c f) f)

type CanDeriveGenericInstance b = (Generic (b (Target F)), Generic (b (Target PxF)), GAdjProof (ClassifyBarbie b) b (RecRep (b (Target F))), Rep (b (Target PxF)) ~ Repl' (Target F) (Target PxF) (RecRep (b (Target F))))

Intuivively, the requirements to have ConstraintsB B derived are:

• There is an instance of Generic (B f) for every f
• If f is used as argument to some type in the definition of B, it is only on a Barbie-type with a ConstraintsB instance.

type ConstraintsOfMatchesGenericDeriv c f b = (ConstraintsOf c f b ~ GConstraintsOf c f (RecRep (b (Target F))), ConstraintsOf c f b ~ ConstraintByType (ClassifyBarbie b) c f (RecRep (b (Target F))))

type GConstraintsOf c f r = ConstraintByType (GClassifyBarbie r) c f r

class GAdjProof (bt :: BarbieType) b rep

Minimal complete definition

gadjProof

Instances

GAdjProof bt b (U1 :: * -> *)

Defined in Data.Barbie.Internal.Constraints

Methods

gadjProof :: (ConstraintByType bt c f U1, GConstraintsOf c f (RecRep (b (Target F)))) => Proxy (c (b f)) -> Proxy bt -> U1 x -> Repl' (Target F) (Target PxF) U1 x

GAdjProof bt b (V1 :: * -> *)

Defined in Data.Barbie.Internal.Constraints

Methods

gadjProof :: (ConstraintByType bt c f V1, GConstraintsOf c f (RecRep (b (Target F)))) => Proxy (c (b f)) -> Proxy bt -> V1 x -> Repl' (Target F) (Target PxF) V1 x

(GAdjProof bt b l, GAdjProof bt b r) => GAdjProof bt b (l :+: r)

Defined in Data.Barbie.Internal.Constraints

Methods

gadjProof :: (ConstraintByType bt c f (l :+: r), GConstraintsOf c f (RecRep (b (Target F)))) => Proxy (c (b f)) -> Proxy bt -> (l :+: r) x -> Repl' (Target F) (Target PxF) (l :+: r) x

(GAdjProof bt b l, GAdjProof bt b r) => GAdjProof bt b (l :*: r)

Defined in Data.Barbie.Internal.Constraints

Methods

gadjProof :: (ConstraintByType bt c f (l :*: r), GConstraintsOf c f (RecRep (b (Target F)))) => Proxy (c (b f)) -> Proxy bt -> (l :*: r) x -> Repl' (Target F) (Target PxF) (l :*: r) x

GAdjProof bt b x => GAdjProof bt b (M1 _i _c x)

Defined in Data.Barbie.Internal.Constraints

Methods

gadjProof :: (ConstraintByType bt c f (M1 _i _c x), GConstraintsOf c f (RecRep (b (Target F)))) => Proxy (c (b f)) -> Proxy bt -> M1 _i _c x x0 -> Repl' (Target F) (Target PxF) (M1 _i _c x) x0

gadjProofDefault :: forall b c f. (CanDeriveGenericInstance b, ConstraintsOfMatchesGenericDeriv c f b, ConstraintsOf c f b) => b f -> b (Product (DictOf c f) f)

Default implementation of adjProof based on Generic.

type family ConstraintByType bt (c :: * -> Constraint) (f :: * -> *) r :: Constraint where ...

Equations

ConstraintByType bt c f (M1 _i _c x) = ConstraintByType bt c f x

ConstraintByType bt c f V1 = ()

ConstraintByType bt c f U1 = ()

ConstraintByType bt c f (l :*: r) = (ConstraintByType bt c f l, ConstraintByType bt c f r)

ConstraintByType bt c f (l :+: r) = (ConstraintByType bt c f l, ConstraintByType bt c f r)

ConstraintByType WearBarbie c f (K1 R (NonRec (Target (W F) a))) = (c (Wear f a), Wear f a ~ f a)

ConstraintByType NonWearBarbie c f (K1 R (NonRec (Target F a))) = c (f a)

ConstraintByType bt c f (K1 R (NonRec (b (Target F)))) = ConstraintsOf c f b

ConstraintByType bt c f (K1 R (RecUsage (b (Target F)))) = ()

ConstraintByType bt c f (K1 _i _c) = ()