{- |
Module: Control.Bidirectional
Description: All you need to use bidirectional instances
Copyright: Lev Dvorkin (c) 2022
License: MIT
Maintainer: lev_135@mail.ru
Stability: experimental
This module provides class wrapper for instances that should be bidirectional,
i. e. lets GHC know that from instance
> instance (A a, B b) => C (Foo a b)
not only @forall a b. (A a, B b) => C (Foo a b)@, but also
@forall a b. C (Foo a b) => A a@ and @forall a b. C (Foo a b) => B b@
can be deduced. This is correct, provided that there are no overlapping
instances for @C (Foo a b)@.
=== __Example 1: showing @GADT@__
Suppose we want to write @Show@ instance for the following GADT type:
> data Term :: Type -> Type where
> Con :: a -> Term a
> Tup :: Term b -> Term c -> Term (b, c)
It's a bit tricky, because an obvious declaration
> instance Show a => Show (Term a) where
> show (Con x) = show x
> show (Tup x y) = unwords ["(", show x, ",", show y, ")"]
fails to typecheck, because in the second equation we apply @show@ function
to @x@, so we need @Show@ instance for @b@ (from GADT constructor).
But we only have @Show a@ where @a ~ (b, c)@. So we need to deduce
@Show (b, c) => Show b@ and GHC fails to do this. This package provides
a solution for this problem:
First of all, we need to make instance @Show (b, c)@ bidirectional.
Maybe sometime in the future it will be declared in @Prelude@, but now we
need to make it manually. TH functions from this module can help to reduce
boilerplate:
> makeBidirectionalInstances [d|
> instance (Show b, Show c) => Show (b, c)
> |]
After bidirectional instance has been declared, we can use our previous
@Show (Term a)@ declaration with a small change: changing constraint
from @Show a@ to @BidirectionalRec Show a@.
> instance BidirectionalRec Show a => Show (Term a) where
> show (Con x) = show x
> show (Tup x y) = unwords ["(", show x, ",", show y, ")"]
Why we need 'BidirectionalRec' constraint, but not simple 'Bidirectional'?
It's so because we may have nested tuples: @(Tup (Tup x y) z)@ and for showing
@(Tup x y)@ we also need bidirectional @Show@ instance. So GHC must infer
@BidirectionalRec Show (b, c) => BidirectionalRec Show b@ and
@Bidirectional Show (b, c) => Show b@ is not enough.
=== __Example 2: mapping error type for @ErrorT@ preserving MonadState constraint__
Suppose we want to change @e@ type for @ExceptT@ transformer preserving
knowledge of @MonadState s@ instance for composed monad. So we want to infer
@MonadState s (ExceptT e m) => MonadState s (ExceptT e' m)@.
Using bidirectional instances it can be done this way:
> Bidirectional (MonadState s) (ExceptT e m)
> => MonadState s ExceptT e m
> => Bidirectional (MonadSTate s) EXceptT e m
Thus, the following is well-typed:
> makeBidirectionalInstances [d|
> instance Monad m => MonadState s (StateT s m)
> instance MonadState s m => MonadState s (ExceptT e m)
> |]
>
> class (forall s e m e'. Bidirectional (MonadState s) (ExceptT e m) =>
> Bidirectional (MonadState s) (ExceptT e' m)) => W'
> instance W'
== Interaction with overlapping instances
As was mentioned above backward implication is sound only when we have
no overlapping instances for.
However, solution from this package /can/ work with overlapping instances,
provided that only one of them is selected to use in backward direction.
Selected instance should be passed to
`makeBidirectionalInstances`/`decBidirectionalInstances`.
For example this code is correct:
> data A a = A a
>
> decBidirectionalInstances [d|
> instance Show a => Show (A a) where
> show (A a) = "A " ++ show a
> |]
>
> instance {-# OVERLAPS #-} Show (A Int) where
> show (A a) = "Integral A: " ++ show (toInteger a)
-}
module Control.Bidirectional (
Bidirectional (..),
BidirectionalRec (..),
decBidirectionalInstances,
makeBidirectionalInstances
) where
import Control.Bidirectional.Class (Bidirectional(..), BidirectionalRec(..))
import Control.Bidirectional.TH (makeBidirectionalInstances, decBidirectionalInstances)