Deeply-nested, generically-derived HKDs.

Types.hs

{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE ApplicativeDo #-}
{-# LANGUAGE BlockArguments #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE EmptyCase #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE ImportQualifiedPost #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneKindSignatures #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}

-- | A proposal for generically-derived HKDs that simultaneously supports the
-- idea of HKDs as fields within an HKD. I'm going to try to explain everything
-- throughout, so bear with me.
module Data.Generic.HKD.Types where

import Data.Generics.Product qualified as G
import Data.Generics.Internal.VL.Lens qualified as G
import Control.Lens ((^.), Iso', Lens')
import Control.Lens qualified as L
import Data.Functor.Const (Const)
import Data.Functor.Contravariant (Contravariant, phantom)
import Data.Kind (Constraint, Type)
import Data.Void (Void)
import GHC.Generics
import Unsafe.Coerce (unsafeCoerce)
import GHC.TypeLits

-- | The type of an HKD is indexed by the list of types deemed "uninteresting",
-- the structure being converted into an HKD, and the functor that wraps around
-- the leaves.
--
-- Internally, it stores the output of the @GHKD@ "function".
type HKD :: [Type] -> Type -> (Type -> Type) -> Type
data HKD xs x f where
  HKD :: forall xs o x f. GHKD xs (Rep x) f o => o Void -> HKD xs x f

-- | The list of uninteresting types for the sake of an example.
type Uninteresting :: [Type]
type Uninteresting = '[ Bool, String ]

-- | An @HKD@ with the default uninteresting types.
type HKD_ :: Type -> (Type -> Type) -> Type
type HKD_ = HKD Uninteresting

-- | Construct an @HKD@ from the inner type by wrapping all leaves either in
-- @f@ or in a further-nested @HKD@. The latter will be the case for all types
-- that /do/ have @Generic@ instances but /don't/ exist within the given list
-- of uninteresting types.
construct :: forall xs o x f. (Generic x, GHKD xs (Rep x) f o) => x -> HKD xs x f
construct = HKD . gconstruct @xs @_ @f @o . from

-- | Convert an @HKD@ to its inner type by applicatively rebuilding the
-- component fields into the original type. The same caveats apply as with
-- @construct@.
deconstruct :: forall xs o x f. (Generic x, GHKD xs (Rep x) f o) => HKD xs x f -> f x
deconstruct (HKD rep) = fmap to (gdeconstruct @xs rep)

-- | @GHKD@ is the powerhouse of this whole implementation. In short, it's in
-- charge of figuring out what the HKD's generic representation, @o@, should
-- be. It does this by walking the tree until it reaches the leaves, then
-- performing two checks to determine their types.
type GHKD :: [Type] -> (Type -> Type) -> (Type -> Type) -> (Type -> Type) -> Constraint
class (Applicative f, Phantom o) => GHKD xs rep f o where
  gconstruct :: forall v. rep v -> o v
  gdeconstruct :: forall v. o v -> f (rep v)

-- Most of these classes are the standard generic walking...

instance
    ( Applicative f
    , GHKD xs x f p
    , o ~ M1 i m p
    ) => GHKD xs (M1 i m x) f o where
  gconstruct = M1 . gconstruct @xs @x @f . unM1
  gdeconstruct = fmap M1 . gdeconstruct @xs @x @f . unM1

instance (Applicative f, o ~ Const Void) => GHKD xs V1 f o where
  gconstruct = \case
  gdeconstruct = \case

instance
    ( Applicative f
    , GHKD xs x f p
    , GHKD xs y f q
    , o ~ (p :+: q)
    ) => GHKD xs (x :+: y) f o where
  gconstruct = \case
    L1 x -> L1 (gconstruct @xs @_ @f x)
    R1 y -> R1 (gconstruct @xs @_ @f y)

  gdeconstruct = \case
    L1 x -> fmap L1 (gdeconstruct @xs x)
    R1 y -> fmap R1 (gdeconstruct @xs y)

instance (Applicative f, o ~ U1) => GHKD t U1 f o where
  gconstruct = id
  gdeconstruct = pure

instance
    ( Applicative f
    , GHKD t x f p
    , GHKD t y f q
    , o ~ (p :*: q)
    ) => GHKD t (x :*: y) f o where
  gconstruct (x :*: y) = gconstruct @t @_ @f x :*: gconstruct @t @_ @f y
  gdeconstruct (x :*: y) = do
    x' <- gdeconstruct @t @_ @f x
    y' <- gdeconstruct @t @_ @f y

    pure (x' :*: y')

-- Here's where things get exciting again: we first need to check whether the
-- leaf type exists in the "uninteresting types" list, so we compute this with
-- @Contains@ and pass the resulting boolean as an argument to the next class,
-- @IsUninteresting@.
instance
    ( Applicative f
    , b ~ Contains x xs
    , IsUninteresting b xs (Rep x) f x p
    , o ~ K1 R p
    ) => GHKD xs (K1 R x) f o where
  gconstruct = K1 . gconstructUninteresting @b @xs @(Rep x) @f . unK1
  gdeconstruct = fmap K1 . gdeconstructUninteresting @b @xs @(Rep x) @f . unK1

type family Contains x xs where
  Contains x (x ': xs) = 'True
  Contains x (y ': xs) = Contains x xs
  Contains x '[     ]  = 'False

-- | This class checks the boolean flag to detemrine whether or not to worry
-- about the given leaf field. If a type is uninteresting - i.e. we have been
-- told not to be interested in it by its presence in @xs@ field - then we
-- immediately know we want it to be a regular `f`-wrapped field. If it's /not/
-- in the list, then we need to check for a `Generic` representation.
type IsUninteresting :: Bool -> [Type] -> (Type -> Type) -> (Type -> Type) -> Type -> Type -> Constraint
class IsUninteresting b xs rep f x o where
  gconstructUninteresting :: x -> o
  gdeconstructUninteresting :: o -> f x

instance (Applicative f, o ~ f x) => IsUninteresting 'True xs rep f x o where
  gconstructUninteresting = pure
  gdeconstructUninteresting = id

instance (IsGeneric xs (Rep x) f x o) => IsUninteresting 'False xs rep f x o where
  gconstructUninteresting = gconstructIsGeneric @xs @(Rep x) @f
  gdeconstructUninteresting = gdeconstructIsGeneric @xs @(Rep x) @f

-- | We check for a `Generic` instance using some `INCOHERENT` tricks with a
-- stuck type family.
type IsGeneric :: [Type] -> (Type -> Type) -> (Type -> Type) -> Type -> Type -> Constraint
class IsGeneric xs rep f x o where
  gconstructIsGeneric :: x -> o
  gdeconstructIsGeneric :: o -> f x

instance (Generic x, GHKD xs (Rep x) f r, o ~ HKD xs x f, Phantom (Rep x))
    => IsGeneric xs (M1 e t c) f x o where
  gconstructIsGeneric x = construct @_ @r x
  gdeconstructIsGeneric x = deconstruct @_ @r x

instance {-# INCOHERENT #-} (Applicative f, o ~ f x)
    => IsGeneric xs isn't f x o where
  gconstructIsGeneric = pure
  gdeconstructIsGeneric = id

-- | Because `HKD` can't have a `Generic` rep (it's inner type is determined by
-- a constraint, and we can't use constraints to calculate the output of a type
-- family), we need an intermediate type: we can convert an `HKD` to this type,
-- and then use its `Generic` rep as a proxy.
type RepWrapper :: (Type -> Type) -> Type
newtype RepWrapper o = RepWrapper { unRepWrap :: o Void }

instance (Contravariant o, Functor o) => Generic (RepWrapper o) where
  type Rep (RepWrapper o) = o

  from (RepWrapper o) = phantom o
  to = RepWrapper . phantom

type Phantom :: (Type -> Type) -> Constraint
type Phantom f = (Contravariant f, Functor f)

-- | An `Iso` to witness the isomorphism between an `HKD` and its inner generic
-- representation. The `unsafeCoerce` here is a shame, but a necessary evil to
-- convince GHC that these things are in fact the same type - because we're not
-- explicitly annotating the `GHKD` class with a functional dependency to its
-- output, GHC is not clever enough to deduce that this /is/ indeed determined.
repWrapper :: forall xs p x f. GHKD xs (Rep x) f p => Iso' (RepWrapper p) (HKD xs x f)
repWrapper = L.iso (HKD . unRepWrap) \(HKD x) ->
  RepWrapper (unsafeCoerce @(_ Void) @(p Void) x)

-- | We can now implement a generic lens by converting the HKD into the
-- `RepWrapper`, and then running standard generic lens things on it.
field :: forall t xs x f i o r. (GHKD xs (Rep x) f o, G.HasField' t (RepWrapper o) r) => Lens' (HKD xs x f) r
field = L.from (repWrapper @xs @o) . G.field' @t

---

-- Here are some example types:
data User = User { userName :: String, userPet :: Pet } deriving Generic
data Pet = Pet { petName :: String, petAge :: Int } deriving Generic

-- `Name` is a `String`, which we deem uninteresting, so GHC deduces an `f`
-- wrapper for this type:
--
-- Found type wildcard ‘_’ standing for ‘f [Char]’
eg1 :: Applicative f => HKD_ User f -> _
eg1 u = u ^. field @"userName"

-- On the other hand, `Pet` is /not/ an uninteresting type and /does/ have a
-- `Generic` instance, so GHC infers an `HKD` wrapper for it.
--
-- Found type wildcard ‘_’ standing for ‘HKD_ Pet f’
eg2 :: Applicative f => HKD_ User f -> _
eg2 u = u ^. field @"userPet"

-- | Here, GHC infers an `HKD` wrapper for `Pet` as before, but then an `f`
-- wrapper for the `Int` /inside/ that `Pet`.
--
-- Found type wildcard ‘_’ standing for ‘f Int’
eg3 :: Applicative f => HKD_ User f -> _
eg3 u = u ^. field @"userPet" . field @"petAge"