Data.Barbie.Constraints

Support for operating on Barbie-types with constrained functions.

Consider the following function:

showIt :: Show a => Maybe a -> Const String a
showIt = Const . show

We would then like to be able to do:

bmap showIt :: FunctorB b => b Maybe -> b (Const String)

This however doesn't work because of the (Show a) constraint in the the type of showIt.

This module adds support to overcome this problem.

Proof of instance

data DictOf c f a where

DictOf c f a is evidence that there exists an instance of c (f a).

Constructors

PackedDict :: c (f a) => DictOf c f a

Instances

Show1 (DictOf c f)

Methods

liftShowsPrec :: (Int -> a -> ShowS) -> ([a] -> ShowS) -> Int -> DictOf c f a -> ShowS

liftShowList :: (Int -> a -> ShowS) -> ([a] -> ShowS) -> [DictOf c f a] -> ShowS

Eq (DictOf c f a)

Methods

(==) :: DictOf c f a -> DictOf c f a -> Bool

(/=) :: DictOf c f a -> DictOf c f a -> Bool

Show (DictOf c f a)

Methods

showsPrec :: Int -> DictOf c f a -> ShowS

show :: DictOf c f a -> String

showList :: [DictOf c f a] -> ShowS

packDict :: c (f a) => DictOf c f a

Pack the dictionary associated with an instance.

requiringDict :: (c (f a) => r) -> DictOf c f a -> r

Turn a constrained-function into an unconstrained one that uses the packed instance dictionary instead.

Retrieving proofs

class FunctorB b => ConstraintsB b

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))

Instances

ConstraintsB b => ConstraintsB (Barbie b)

Associated Types

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

Methods

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

class (ConstraintsB b, ProductB b) => ProofB b where

Barbie-types with products have a canonical proof of instance.

There is a default bproof implementation for Generic types, so instances can derived automatically.

Methods

bproof :: ConstraintsOf c f b => b (DictOf c f)

bproof :: (CanDeriveGenericInstance b, ConstraintsOfMatchesGenericDeriv c f b, ConstraintsOf c f b) => b (DictOf c f)

Instances

ProofB b => ProofB (Barbie b)

Methods

bproof :: ConstraintsOf c f (Barbie b) => Barbie b (DictOf c f)