{-# OPTIONS_HADDOCK not-home #-}
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE BlockArguments #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-|
Module : Data.Generic.HKD.Build
Description : Construct an HKD structure with its component parameters.
Copyright : (c) Tom Harding, 2019
License : MIT
Maintainer : tom.harding@habito.com
Stability : experimental
-}
module Data.Generic.HKD.Build
( Build (..)
) where
import Data.Kind (Type)
import Data.GenericLens.Internal (HList (..))
import Data.Generic.HKD.Types (HKD (..), GHKD_)
import GHC.Generics
import Prelude hiding (uncurry)
class Fill (f :: Type -> Type) (structure :: Type) (types :: [Type])
| structure f -> types, types -> f where
fill :: HList types -> HKD structure f
class GFill (f :: Type -> Type) (xs :: [Type]) (ys :: [Type]) (rep :: Type -> Type)
| xs rep -> ys, ys f rep -> xs, xs -> f where
gfill :: HList xs -> (HList ys, GHKD_ f rep p)
instance GFill f xs ys inner
=> GFill f xs ys (M1 index meta inner) where
gfill = fmap M1 . gfill @f
instance (GFill f xs ys left, GFill f ys zs right)
=> GFill f xs zs (left :*: right) where
gfill xs = do
let (ys, left) = gfill @f xs
(zs, right) = gfill @f ys
(zs, left :*: right)
instance GFill f (f x ': xs) xs (Rec0 x) where
gfill (x :> xs) = (xs, K1 x)
instance (Generic shape, GFill f with '[] (Rep shape))
=> Fill f shape with where
fill = HKD . snd . gfill @f @_ @'[]
-- | With many HKD applications, we're working with types like 'Maybe' where it
-- makes sense for us to start with 'mempty' and add values in as we go.
--
-- This isn't always the case, however: if all the component parts of our type
-- are gathered using some 'IO' action, we'd like to construct something like
-- @HKD MyType IO@, and @IO a@ isn't a 'Monoid' for all types @a@. When this
-- happens, we need to pass in our parameters /when/ we build our structure.
--
-- The 'build' function lets us construct our type by passing explicit values
-- for each parameter:
--
-- >>> :set -XDeriveGeneric -XTypeApplications
--
-- >>> :{
-- data User
-- = User { name :: String, age :: Int, likesDogs :: Bool }
-- deriving Generic
-- :}
--
-- >>> :{
-- test :: _
-- test = build @User
-- :}
-- ...
-- ... • Found type wildcard ‘_’
-- ... standing for ‘f [Char] -> f Int -> f Bool -> HKD User f’
-- ...
--
-- Once we call the 'build' function, and indicate the type we want to build,
-- we are free to pick whichever 'f' we like and get to work!
class Build (structure :: Type) (f :: Type -> Type) (k :: Type)
| f structure -> k where
build :: k
class GBuild (f :: Type -> Type) (structure :: Type) (xs :: [Type]) (k :: Type)
| f structure xs -> k where
gbuild :: (HList xs -> HKD structure f) -> k
instance GBuild f structure xs k
=> GBuild f structure (x ': xs) (x -> k) where
gbuild k x = gbuild @_ @_ @xs \xs -> k (x :> xs)
instance GBuild f structure '[] (HKD structure f) where
gbuild k = k Nil
instance (Fill f structure xs, GBuild f structure xs k)
=> Build structure f k where
build = gbuild @f @structure @xs fill