module Data.Extensible.Product (
(:*)(..)
, (<:*)
, (*++*)
, hhead
, htail
, huncons
, hmap
, hzipWith
, hzipWith3
, hfoldMap
, htraverse
, htabulate
, hlookup
, sector
, sectorAt
, Generate(..)
, Forall(..)) where
import Data.Extensible.Internal
import Data.Extensible.Internal.Rig
import Unsafe.Coerce
import Data.Typeable
import Control.Applicative
import Data.Monoid
data (h :: k -> *) :* (s :: [k]) where
Nil :: h :* '[]
Tree :: !(h x)
-> !(h :* Half xs)
-> !(h :* Half (Tail xs))
-> h :* (x ': xs)
deriving instance Typeable (:*)
instance Show (h :* '[]) where
show Nil = "Nil"
instance (Show (h :* xs), Show (h x)) => Show (h :* (x ': xs)) where
showsPrec d t = let (x, xs) = huncons t in showParen (d > 0) $
showsPrec 0 x
. showString " <:* "
. showsPrec 0 xs
hhead :: h :* (x ': xs) -> h x
hhead (Tree a _ _) = a
htail :: h :* (x ': xs) -> h :* xs
htail (Tree _ a@(Tree h _ _) b) = unsafeCoerce (Tree h) b (htail a)
htail _ = unsafeCoerce Nil
huncons :: forall h x xs. h :* (x ': xs) -> (h x, h :* xs)
huncons t@(Tree a _ _) = (a, htail t)
(<:*) :: forall h x xs. h x -> h :* xs -> h :* (x ': xs)
a <:* Tree b c d = Tree a (lemmaHalfTail (Proxy :: Proxy (Tail xs)) $! b <:* d) c
a <:* Nil = Tree a Nil Nil
infixr 0 <:*
hmap :: (forall x. g x -> h x) -> g :* xs -> h :* xs
hmap t (Tree h a b) = Tree (t h) (hmap t a) (hmap t b)
hmap _ Nil = Nil
(*++*) :: h :* xs -> h :* ys -> h :* (xs ++ ys)
(*++*) Nil ys = ys
(*++*) xs'@(Tree x _ _) ys = let xs = htail xs' in x <:* (xs *++* ys)
infixr 0 *++*
hzipWith :: (forall x. f x -> g x -> h x) -> f :* xs -> g :* xs -> h :* xs
hzipWith t (Tree f a b) (Tree g c d) = Tree (t f g) (hzipWith t a c) (hzipWith t b d)
hzipWith _ Nil _ = Nil
hzipWith _ _ Nil = Nil
hzipWith3 :: (forall x. f x -> g x -> h x -> i x) -> f :* xs -> g :* xs -> h :* xs -> i :* xs
hzipWith3 t (Tree f a b) (Tree g c d) (Tree h e f') = Tree (t f g h) (hzipWith3 t a c e) (hzipWith3 t b d f')
hzipWith3 _ Nil _ _ = Nil
hzipWith3 _ _ Nil _ = Nil
hzipWith3 _ _ _ Nil = Nil
hfoldMap :: Monoid a => (forall x. h x -> a) -> h :* xs -> a
hfoldMap f (Tree h a b) = f h <> hfoldMap f a <> hfoldMap f b
hfoldMap _ Nil = mempty
htraverse :: Applicative f => (forall x. h x -> f (h x)) -> h :* xs -> f (h :* xs)
htraverse f (Tree h a b) = Tree <$> f h <*> htraverse f a <*> htraverse f b
htraverse _ Nil = pure Nil
hlookup :: Position xs x -> h :* xs -> h x
hlookup = view . sectorAt
htabulate :: forall g h xs. (forall x. Position xs x -> g x -> h x) -> g :* xs -> h :* xs
htabulate f = go id where
go :: (forall x. Position t x -> Position xs x) -> g :* t -> h :* t
go k (Tree g a b) = Tree (f (k here) g) (go (k . navL) a) (go (k . navR) b)
go _ Nil = Nil
instance Forall (ClassComp Eq h) xs => Eq (h :* xs) where
(==) = (aggr.) . hzipWith3 (\pos -> (Const' .) . unwrapEq (view (sectorAt pos) dic))
(generateFor c id) where
dic = generateFor c $ const $ WrapEq (==)
aggr = getAll . hfoldMap (All . getConst')
c = Proxy :: Proxy (ClassComp Eq h)
instance (Forall (ClassComp Eq h) xs, Forall (ClassComp Ord h) xs) => Ord (h :* xs) where
compare = (aggr.) . hzipWith3 (\pos -> (Const' .) . unwrapOrd (view (sectorAt pos) dic))
(generateFor c id) where
dic = generateFor c $ const $ WrapOrd compare
aggr = hfoldMap getConst'
c = Proxy :: Proxy (ClassComp Ord h)
newtype WrapEq h x = WrapEq { unwrapEq :: h x -> h x -> Bool }
newtype WrapOrd h x = WrapOrd { unwrapOrd :: h x -> h x -> Ordering }
sector :: (Functor f, x ∈ xs) => (h x -> f (h x)) -> h :* xs -> f (h :* xs)
sector = sectorAt membership
sectorAt :: forall h x xs f. (Functor f) => Position xs x -> (h x -> f (h x)) -> h :* xs -> f (h :* xs)
sectorAt pos0 f = go pos0 where
go :: forall t. Position t x -> h :* t -> f (h :* t)
go pos (Tree h a b) = case navigate pos of
Here -> fmap (\h' -> Tree h' a b) (f h)
NavL p -> fmap (\a' -> Tree h a' b) $ go p a
NavR p -> fmap (\b' -> Tree h a b') $ go p b
go _ Nil = error "Impossible"
class Generate (xs :: [k]) where
generate :: (forall x. Position xs x -> h x) -> h :* xs
instance Generate '[] where
generate _ = Nil
instance (Generate (Half xs), Generate (Half (Tail xs))) => Generate (x ': xs) where
generate f = Tree (f here) (generate (f . navL)) (generate (f . navR))
class Forall c (xs :: [k]) where
generateFor :: proxy c -> (forall x. c x => Position xs x -> h x) -> h :* xs
instance Forall c '[] where
generateFor _ _ = Nil
instance (c x, Forall c (Half xs), Forall c (Half (Tail xs))) => Forall c (x ': xs) where
generateFor proxy f = Tree (f here) (generateFor proxy (f . navL)) (generateFor proxy (f . navR))