Documentation

A FunctorB with application, providing operations to:

• embed an "empty" value (bpure)
• align and combine values (bprod)

It should satisfy the following laws:

Naturality of bprod

bmap ((Pair a b) -> Pair (f a) (g b)) (u `bprod` v) = bmap f u `bprod` bmap g v

Left and right identity

bmap ((Pair _ b) -> b) (bpure e `bprod` v) = v
bmap ((Pair a _) -> a) (u `bprod` bpure e) = u

Associativity

bmap ((Pair a (Pair b c)) -> Pair (Pair a b) c) (u `bprod` (v `bprod` w)) = (u `bprod` v) `bprod` w

It is to FunctorB in the same way as Applicative relates to Functor. For a presentation of Applicative as a monoidal functor, see Section 7 of Applicative Programming with Effects.

There is a default implementation of bprod and bpure based on Generic. Intuitively, it works on types where the value of bpure is uniquely defined. This corresponds rougly to record types (in the presence of sums, there would be several candidates for bpure), where every field is either a Monoid or covered by the argument f.

Instances of this class provide means to talk about constraints, both at compile-time, using AllB, and at run-time, in the form of Dict, via baddDicts.

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 AllB c T = (c Int, c String, c Bool)

  baddDicts t = case t of
    A x y -> A (Pair Dict x) (Pair Dict y)
    B z w -> B (Pair Dict z) (Pair Dict w)

Now, when we given a T f, if we need to use the Show instance of their fields, we can use:

baddDicts :: AllB Show b => b f -> b (Dict Show `Product` f)

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

derive instance Generic (T f)
instance ConstraintsB T

Barbie-types that can be mapped over. Instances of FunctorB should satisfy the following laws:

bmap id = id
bmap f . bmap g = bmap (f . g)

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

Barbie-types that can be traversed from left to right. Instances should satisfy the following laws:

 t . btraverse f   = btraverse (t . f)  -- naturality
btraverse Identity = Identity           -- identity
btraverse (Compose . fmap g . f) = Compose . fmap (btraverse g) . btraverse f -- composition

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

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 HKD
... ([Char], Bool) f does not contain a field at position 4
...

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'.
...