Deriving Applicative for sum types.. Idiomatically.

Idiomatically is used with DerivingVia to derive Applicative for types with multiple constructors.

The name comes from the original paper on Applicatives: Idioms: applicative programming with effects.

It features an extensible domain-specific language of sums with Applicative instances. Idiomatically is then passed a type-level list of applicative sums that specify how deriving should take place.

{-# Language DataKinds          #-}
{-# Language DeriveGeneric      #-}
{-# Language DerivingStrategies #-}
{-# Language DerivingVia        #-}

import Generic.Applicative

data Zip a = No | a ::: Zip a
  deriving
  stock (Show, Generic1)

  deriving (Functor, Applicative)
  via Idiomatically Zip '[RightBias Terminal]

This derives the standard behaviour of ZipList but this same "RightBias Terminal" behaviour describes the Maybe and Validation applicative as well.

pure @Zip a = a ::: a ::: a ::: ...

liftA2 (+) No       No        = No
liftA2 (+) No       (⊥:::⊥)   = No
liftA2 (+) (⊥:::⊥)  No        = No
liftA2 (+) (2:::No) (10:::No) = 12:::No

Idiomatically shares an intimate relationship with Generically1: it is defined in terms of Generically1 and they are interchangeable when there is an empty list of sums:

type Generically1 :: (k -> Type) -> (k -> Type)
type Generically1 f = Idiomatically f '[]

Based on Abstracting with Applicatives.

Deriving Applicative sums... Idiomatically!

Idiomatically is used with DerivingVia to derive Applicative for sum types. It takes as an argument a list of sum constructors that it uses to tweak the generic representation of a type.

{-# Language DataKinds          #-}
{-# Language DeriveGeneric      #-}
{-# Language DerivingStrategies #-}
{-# Language DerivingVia        #-}

import Generic.Applicative

data Maybe a = Nothing | Just a
  deriving
  stock Generic1

  deriving (Functor, Applicative)
  via Idiomatically Maybe '[RightBias Terminal]

This comes with two tagged newtypes over Sum that are biased toward the left and right constructor.

newtype LeftBias  tag l r a = LeftBias  (Sum l r a)
newtype RightBias tag l r a = RightBias (Sum l r a)

  pure = LeftBias  . InL . pure @l
  pure = RightBias . InR . pure @r

and an extensible language for type-level applicative morphisms (Idiom) used to map away from the pure constructor.

-- Applicative morphisms preserve the `Applicative` operations
--
--   idiom (pure @f a)           = pure @g a
--   idiom (liftA2 @f (·) as bs) = liftA2 @g (·) (idiom as) (idiom bs)
--
type  Idiom :: t -> (Type -> Type) -> (Type -> Type) -> Constraint
class (Applicative f, Applicative g) => Idiom tag f g where
  idiom :: f ~> g

This means for LeftBias tag l r we map from the left-to-right and that for RightBias tag l r we map from right-to-left.

instance Idiom tag l r => Applicative (LeftBias  tag l r)
instance Idiom tag r l => Applicative (RightBias tag l r)

For example, the identity applicative morphism

data Id
instance f ~ g => Idiom Id f g where
  idiom :: f ~> f
  idiom = id

can be used to derive two different instances for the same datatype by either defecting from the the left constructor (LPure) or from the right constructor (RPure).

-- >> pure @L True
-- LPure True
-- >> liftA2 (+) (LPure 1) (L 100)
-- L 101
data L a = LPure a | L a
  deriving stock (Show, Generic1)

  deriving (Functor, Applicative)
  via Idiomatically L '[LeftBias Id]

-- >> pure @R False
-- RPure False
-- >> liftA2 (+) (RPure 1) (R 100)
-- R 101
data R a = R a | RPure a
  deriving stock (Show, Generic1)

  deriving (Functor, Applicative) 
  via Idiomatically R '[RightBias Id]

More compliated descriptions are possible where we mediate between multiple constructors:

-- >> pure @Ok 10
-- Ok1 10
-- >> liftA2 (+) (Ok1 10) (Ok5 20)
-- Ok3 [Just 30]
-- >> liftA2 (+) (Ok2 [1..4]) (Ok5 20)
-- Ok3 [Just 21,Just 22,Just 23,Just 24]
-- >> liftA2 (+) (Ok2 [1..4]) (Ok4 Nothing)
-- Ok3 [Nothing,Nothing,Nothing,Nothing]
data Ok a = Ok1 a | Ok2 [a] | Ok3 [Maybe a] | Ok4 (Maybe a) | Ok5 a
  deriving
  stock (Show, Generic1)

  deriving (Functor, Applicative) 
  via Idiomatically Ok
    '[ LeftBias Initial       -- Ok1 to Ok2: pure
     , LeftBias Inner         -- Ok2 to Ok3: fmap pure
     , RightBias Outer        -- Ok4 to Ok3: pure
     , RightBias Initial      -- Ok5 to Ok4: pure
     ]

Relationship to Generically1

Generically1 was recently introduced to GHC.Generics (base 4.17.0.0) with the ability to derive Applicative for generic type constructors, among other things. Before it was added to base it was found in the generic-data package.

For Applicative in particular it uses the underlying generic representation of a type; if that representation has an Applicative instance then Applicative can be derived.

import GHC.Generics (Generically1(..))

data F a = F a String a a [[[a]]] (Int -> Maybe a)
  deriving stock Generic1

  deriving (Functor, Applicative) via Generically1 F

This works well for product types but it does not work for sum types since there is no Appliative (Sum f g) or Applicative (f :+: g) instance.

In this sense, Generically1 can be recovered by passing an empty list of sums to Idiomatically:

  Generically1  F
= Idiomatically F '[]

Idiomatically is also defined in terms of Generically1:

type Idiomatically :: (k -> Type) -> [SumKind k] -> (k -> Type)
type Idiomatically f sums = Generically1 (NewSums (Served sums) f)

The argument to Generically1 is less important, what is basically happening is that NewSums modifies the generic behaviour of f: it traverses the generic representation Rep1 f and replace every sum with an Applicative sum from type-level list.

This means we can define Idiomatically in terms of Generically1. There is an Applicative instance for Generically1 if its representation is Applicative, by tweaking the representation of its argument we have thus managed to configure Generically1 even though it has no configuration parameter!