destroy.hs

{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE NoStarIsType #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}

-- base
import Data.Kind (Type)
import GHC.Generics (Generic)

-- generics-sop
import Generics.SOP hiding (Generic)
import Generics.SOP.GGP (GCode, GFrom, gfrom)


type family Selectors (selectors :: [Type]) (o :: Type) :: Type where
  Selectors '[] o = o
  Selectors (a ': as) o = a -> Selectors as o


type family Constructors (constructors :: [[Type]]) (i :: Type) (o :: Type) :: Type where
  Constructors '[] i o = i -> o
  Constructors (a ': as) i o = Selectors a o -> Constructors as i o


newtype F a rep = F (Selectors rep a)


gpdestroy :: Selectors rep b -> NP I rep -> b
gpdestroy b Nil = b
gpdestroy f (I a :* as) = gpdestroy (f a) as


gsdestroy :: NP (F b) rep -> NS (NP I) rep -> b
gsdestroy (F f :* _) (Z a) = gpdestroy f a
gsdestroy (_ :* fs) (S a) = gsdestroy fs a


gdestroy :: forall a b xs rep. Shape xs -> (NP (F b) xs -> NP (F b) rep) -> (a -> SOP I rep) -> Constructors xs a b
gdestroy ShapeNil = \fs g -> gsdestroy (fs Nil) . unSOP . g
gdestroy (ShapeCons as) = \fs g f -> gdestroy as (fs . (F f :*)) g


type Destructable a = (Generic a, GFrom a, SListI (GCode a))


type Destructor a b = Constructors (GCode a) a b


destroy :: forall a b. Destructable a => Destructor a b
destroy = gdestroy @a @b shape id gfrom