elim-sop.hs

{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}

import Data.Typeable
import qualified GHC.Generics as GHC
import Generics.SOP
import Unsafe.Coerce

type family Fun result args where
  Fun result '[] = result
  Fun result (arg : args) = arg -> Fun result args

newtype Fun' result args = Fun' (Fun result args)

type family Replace a b xs where
  Replace _ _ '[] = '[]
  Replace a b (a : xs) = b : Replace a b xs
  Replace a b (x : xs) = x : Replace a b xs

type family Replace2 a b xss where
  Replace2 _ _ '[] = '[]
  Replace2 a b (xs : xss) = Replace a b xs : Replace2 a b xss

ap :: Fun b xs -> NP I xs -> b
ap f Nil = f
ap f (I x :* xs) = ap (f x) xs

reduce :: forall a b xs. (Typeable a, All Typeable xs) => (a -> b) -> NP I xs -> NP I (Replace a b xs)
reduce f Nil = Nil
reduce f (I (x :: x) :* xs) = case eqT @a @x of
  Just Refl -> I (f x) :* reduce f xs
  Nothing -> unsafeCoerce (I x :* reduce f xs) -- a !~ b is not provided

reduce2 :: forall a b xss. (Typeable a, All2 Typeable xss) => (a -> b) -> NS (NP I) xss -> NS (NP I) (Replace2 a b xss)
reduce2 f (Z x) = Z (reduce f x)
reduce2 f (S x) = S (reduce2 f x)

elim' :: forall a b. (Generic a, Typeable a, All2 Typeable (Code a), All2 Typeable (Replace2 a b (Code a))) => NP (Fun' b) (Replace2 a b (Code a)) -> a -> b
elim' elims = go
  where
    go :: a -> b
    go = hcollapse . hliftA2 (\(Fun' f) prod -> K (ap f prod)) elims . reduce2 go . unSOP . from

data Tree a = Leaf a | Node (Tree a) (Tree a)
  deriving (GHC.Generic, Generic, Show)

main = do
  let elims = Fun' show :* Fun' (<>) :* Nil
  let value = Node (Leaf 1) (Node (Leaf 2) (Leaf 3))
  print $ elim' elims (value :: Tree Int) -- "123"

-- elim :: forall a b elims ecode. (Generic a, Typeable a, All2 Typeable (Code a), All2 Typeable (Replace2 a b (Code a)), IsProductType elims ecode, Coercible (NP I ecode) (NP (Fun' b) (Replace2 a b (Code a)))) => elims -> a -> b
-- elim elims =
--   let a = productTypeFrom elims
--    in elim' (coerce a)