{-# OPTIONS_GHC -Wno-unrecognised-pragmas #-}

{-# HLINT ignore "Eta reduce" #-}

-- | implements a heterogeneous list to use for forests of heterogeneous trees
module Data.HTree.List
  ( -- * heterogeneous list
    HList ((:::), HSing, ..)

    -- * mapping
  , hcmap
  , hmap

    -- * traversing
  , htraverse
  , hctraverse

    -- * folding
  , hcFold

    -- * helpers
  , allTopHList
  , hconcat
  )
where

import Data.Functor.Identity (Identity (Identity, runIdentity))
import Data.HTree.Constraint (withDict, pattern Dict, type Dict)
import Data.HTree.Families (All, Top, type (++))
import Data.Kind (Type)

-- | A heterogeneous list
--
-- >>> "bla" `HCons` 23 `HCons` HNil :: HList Identity '[ String, Int ]
-- HCons (Identity "bla") (HCons (Identity 23) HNil)
type HList :: forall k. (k -> Type) -> [k] -> Type
data HList f ts where
  HCons :: forall f x xs. f x -> HList f xs -> HList f (x : xs)
  HNil :: forall f. HList f '[]

-- | pattern synonym for 'HCons'
--
-- >>> t = "bla" ::: 23 ::: HNil :: HList Identity '[ String, Int ]
-- >>> t
-- HCons (Identity "bla") (HCons (Identity 23) HNil)
-- >>> case t of (x ::: _) -> runIdentity x
-- "bla"
pattern (:::) :: forall f x xs. f x -> HList f xs -> HList f (x : xs)
pattern x $m::: :: forall {r} {a} {f :: a -> Type} {x :: a} {xs :: [a]}.
HList @a f ((':) @a x xs)
-> (f x -> HList @a f xs -> r) -> ((# #) -> r) -> r
$b::: :: forall {a} (f :: a -> Type) (x :: a) (xs :: [a]).
f x -> HList @a f xs -> HList @a f ((':) @a x xs)
::: xs = HCons x xs

-- | pattern that allows to construct a singleton HList
--
-- >>> HSing 42 :: HList Identity '[ Int ]
-- HCons (Identity 42) HNil
pattern HSing :: forall f a. f a -> HList f '[a]
pattern $mHSing :: forall {r} {k} {f :: k -> Type} {a :: k}.
HList @k f ((':) @k a ('[] @k)) -> (f a -> r) -> ((# #) -> r) -> r
$bHSing :: forall {k} (f :: k -> Type) (a :: k).
f a -> HList @k f ((':) @k a ('[] @k))
HSing x = HCons x HNil

-- | map with a function that maps forall f a
hmap :: forall f g xs. (forall a. f a -> g a) -> HList f xs -> HList g xs
hmap :: forall {k} (f :: k -> Type) (g :: k -> Type) (xs :: [k]).
(forall (a :: k). f a -> g a) -> HList @k f xs -> HList @k g xs
hmap forall (a :: k). f a -> g a
f HList @k f xs
l = Dict (All @k (Top @k) xs)
-> (All @k (Top @k) xs => HList @k g xs) -> HList @k g xs
forall (c :: Constraint) r. Dict c -> (c => r) -> r
withDict (HList @k f xs -> Dict (All @k (Top @k) xs)
forall {k} (f :: k -> Type) (xs :: [k]).
HList @k f xs -> Dict (All @k (Top @k) xs)
allTopHList HList @k f xs
l) ((All @k (Top @k) xs => HList @k g xs) -> HList @k g xs)
-> (All @k (Top @k) xs => HList @k g xs) -> HList @k g xs
forall a b. (a -> b) -> a -> b
$ forall {k} (c :: k -> Constraint) (f :: k -> Type) (g :: k -> Type)
       (xs :: [k]).
All @k c xs =>
(forall (a :: k). c a => f a -> g a)
-> HList @k f xs -> HList @k g xs
forall (c :: k -> Constraint) (f :: k -> Type) (g :: k -> Type)
       (xs :: [k]).
All @k c xs =>
(forall (a :: k). c a => f a -> g a)
-> HList @k f xs -> HList @k g xs
hcmap @Top @f @g f a -> g a
forall (a :: k). f a -> g a
forall (a :: k). Top @k a => f a -> g a
f HList @k f xs
l

-- | map with a constraint that holds for all elements of the  list
--
-- >>> import Data.Functor.Const
-- >>> hcmap @Show (Const . show . runIdentity) (42 `HCons` HSing "bla" :: HList Identity '[ Int, String ])
-- HCons (Const "42") (HCons (Const "\"bla\"") HNil)
hcmap :: forall c f g xs. All c xs => (forall a. c a => f a -> g a) -> HList f xs -> HList g xs
hcmap :: forall {k} (c :: k -> Constraint) (f :: k -> Type) (g :: k -> Type)
       (xs :: [k]).
All @k c xs =>
(forall (a :: k). c a => f a -> g a)
-> HList @k f xs -> HList @k g xs
hcmap forall (a :: k). c a => f a -> g a
f = Identity (HList @k g xs) -> HList @k g xs
forall a. Identity a -> a
runIdentity (Identity (HList @k g xs) -> HList @k g xs)
-> (HList @k f xs -> Identity (HList @k g xs))
-> HList @k f xs
-> HList @k g xs
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} (c :: k -> Constraint) (t :: Type -> Type)
       (f :: k -> Type) (g :: k -> Type) (xs :: [k]).
(All @k c xs, Applicative t) =>
(forall (a :: k). c a => f a -> t (g a))
-> HList @k f xs -> t (HList @k g xs)
forall (c :: k -> Constraint) (t :: Type -> Type) (f :: k -> Type)
       (g :: k -> Type) (xs :: [k]).
(All @k c xs, Applicative t) =>
(forall (a :: k). c a => f a -> t (g a))
-> HList @k f xs -> t (HList @k g xs)
hctraverse @c @Identity @f @g (g a -> Identity (g a)
forall a. a -> Identity a
Identity (g a -> Identity (g a)) -> (f a -> g a) -> f a -> Identity (g a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. f a -> g a
forall (a :: k). c a => f a -> g a
f)

-- | traverse a structure with a function
htraverse :: forall t f g xs. Applicative t => (forall a. f a -> t (g a)) -> HList f xs -> t (HList g xs)
htraverse :: forall {k} (t :: Type -> Type) (f :: k -> Type) (g :: k -> Type)
       (xs :: [k]).
Applicative t =>
(forall (a :: k). f a -> t (g a))
-> HList @k f xs -> t (HList @k g xs)
htraverse forall (a :: k). f a -> t (g a)
f HList @k f xs
l = Dict (All @k (Top @k) xs)
-> (All @k (Top @k) xs => t (HList @k g xs)) -> t (HList @k g xs)
forall (c :: Constraint) r. Dict c -> (c => r) -> r
withDict (HList @k f xs -> Dict (All @k (Top @k) xs)
forall {k} (f :: k -> Type) (xs :: [k]).
HList @k f xs -> Dict (All @k (Top @k) xs)
allTopHList HList @k f xs
l) ((All @k (Top @k) xs => t (HList @k g xs)) -> t (HList @k g xs))
-> (All @k (Top @k) xs => t (HList @k g xs)) -> t (HList @k g xs)
forall a b. (a -> b) -> a -> b
$ forall {k} (c :: k -> Constraint) (t :: Type -> Type)
       (f :: k -> Type) (g :: k -> Type) (xs :: [k]).
(All @k c xs, Applicative t) =>
(forall (a :: k). c a => f a -> t (g a))
-> HList @k f xs -> t (HList @k g xs)
forall (c :: k -> Constraint) (t :: Type -> Type) (f :: k -> Type)
       (g :: k -> Type) (xs :: [k]).
(All @k c xs, Applicative t) =>
(forall (a :: k). c a => f a -> t (g a))
-> HList @k f xs -> t (HList @k g xs)
hctraverse @Top @t @f @g f a -> t (g a)
forall (a :: k). f a -> t (g a)
forall (a :: k). Top @k a => f a -> t (g a)
f HList @k f xs
l

-- | traverse a structure such that a constraint holds; this is the workhorse of mapping and traversing
--
-- >>> import Data.Functor.Const
-- >>> hctraverse @Show (Just . Const . show . runIdentity) (42 `HCons` HSing "bla" :: HList Identity '[ Int, String ])
-- Just (HCons (Const "42") (HCons (Const "\"bla\"") HNil))
hctraverse :: forall c t f g xs. (All c xs, Applicative t) => (forall a. c a => f a -> t (g a)) -> HList f xs -> t (HList g xs)
hctraverse :: forall {k} (c :: k -> Constraint) (t :: Type -> Type)
       (f :: k -> Type) (g :: k -> Type) (xs :: [k]).
(All @k c xs, Applicative t) =>
(forall (a :: k). c a => f a -> t (g a))
-> HList @k f xs -> t (HList @k g xs)
hctraverse forall (a :: k). c a => f a -> t (g a)
_ HList @k f xs
HNil = HList @k g xs -> t (HList @k g xs)
forall a. a -> t a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure HList @k g xs
HList @k g ('[] @k)
forall {k} (f :: k -> Type). HList @k f ('[] @k)
HNil
hctraverse forall (a :: k). c a => f a -> t (g a)
f (HCons f x
x HList @k f xs
xs) = g x -> HList @k g xs -> HList @k g xs
g x -> HList @k g xs -> HList @k g ((':) @k x xs)
forall {a} (f :: a -> Type) (x :: a) (xs :: [a]).
f x -> HList @a f xs -> HList @a f ((':) @a x xs)
HCons (g x -> HList @k g xs -> HList @k g xs)
-> t (g x) -> t (HList @k g xs -> HList @k g xs)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> f x -> t (g x)
forall (a :: k). c a => f a -> t (g a)
f f x
x t (HList @k g xs -> HList @k g xs)
-> t (HList @k g xs) -> t (HList @k g xs)
forall a b. t (a -> b) -> t a -> t b
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> forall {k} (c :: k -> Constraint) (t :: Type -> Type)
       (f :: k -> Type) (g :: k -> Type) (xs :: [k]).
(All @k c xs, Applicative t) =>
(forall (a :: k). c a => f a -> t (g a))
-> HList @k f xs -> t (HList @k g xs)
forall (c :: k -> Constraint) (t :: Type -> Type) (f :: k -> Type)
       (g :: k -> Type) (xs :: [k]).
(All @k c xs, Applicative t) =>
(forall (a :: k). c a => f a -> t (g a))
-> HList @k f xs -> t (HList @k g xs)
hctraverse @c @t @f @g f a -> t (g a)
forall (a :: k). c a => f a -> t (g a)
f HList @k f xs
xs

-- | foldr for HLists.
hcFold :: forall c f b xs. All c xs => (forall a. c a => f a -> b -> b) -> b -> HList f xs -> b
hcFold :: forall {k} (c :: k -> Constraint) (f :: k -> Type) b (xs :: [k]).
All @k c xs =>
(forall (a :: k). c a => f a -> b -> b) -> b -> HList @k f xs -> b
hcFold forall (a :: k). c a => f a -> b -> b
_ b
def HList @k f xs
HNil = b
def
hcFold forall (a :: k). c a => f a -> b -> b
f b
def (f x
x `HCons` HList @k f xs
xs) = f x -> b -> b
forall (a :: k). c a => f a -> b -> b
f f x
x (b -> b) -> b -> b
forall a b. (a -> b) -> a -> b
$ forall {k} (c :: k -> Constraint) (f :: k -> Type) b (xs :: [k]).
All @k c xs =>
(forall (a :: k). c a => f a -> b -> b) -> b -> HList @k f xs -> b
forall (c :: k -> Constraint) (f :: k -> Type) b (xs :: [k]).
All @k c xs =>
(forall (a :: k). c a => f a -> b -> b) -> b -> HList @k f xs -> b
hcFold @c f a -> b -> b
forall (a :: k). c a => f a -> b -> b
f b
def HList @k f xs
xs

-- | witnesses that for all HLists, we can always derive the All Top constraint
allTopHList :: forall f xs. HList f xs -> Dict (All Top xs)
allTopHList :: forall {k} (f :: k -> Type) (xs :: [k]).
HList @k f xs -> Dict (All @k (Top @k) xs)
allTopHList HList @k f xs
HNil = Dict (() :: Constraint)
Has @Type (Charge @Type (All @k (Top @k) xs)) (Proxy @Type) ()
forall (c :: Constraint). c => Dict c
Dict
allTopHList (HCons f x
_ HList @k f xs
xs) = case HList @k f xs -> Dict (All @k (Top @k) xs)
forall {k} (f :: k -> Type) (xs :: [k]).
HList @k f xs -> Dict (All @k (Top @k) xs)
allTopHList HList @k f xs
xs of
  Dict (All @k (Top @k) xs)
Dict -> Dict (Top @k x, All @k (Top @k) xs)
Has @Type (Charge @Type (All @k (Top @k) xs)) (Proxy @Type) ()
forall (c :: Constraint). c => Dict c
Dict

-- | concats two heterogeneous lists
hconcat :: forall f xs ys. HList f xs -> HList f ys -> HList f (xs ++ ys)
hconcat :: forall {k} (f :: k -> Type) (xs :: [k]) (ys :: [k]).
HList @k f xs -> HList @k f ys -> HList @k f ((++) @k xs ys)
hconcat HList @k f xs
HNil HList @k f ys
ys = HList @k f ys
HList @k f ((++) @k xs ys)
ys
hconcat (f x
x `HCons` HList @k f xs
xs) HList @k f ys
ys = f x
x f x
-> HList @k f ((++) @k xs ys)
-> HList @k f ((':) @k x ((++) @k xs ys))
forall {a} (f :: a -> Type) (x :: a) (xs :: [a]).
f x -> HList @a f xs -> HList @a f ((':) @a x xs)
`HCons` HList @k f xs
xs HList @k f xs -> HList @k f ys -> HList @k f ((++) @k xs ys)
forall {k} (f :: k -> Type) (xs :: [k]) (ys :: [k]).
HList @k f xs -> HList @k f ys -> HList @k f ((++) @k xs ys)
`hconcat` HList @k f ys
ys

infixr 5 `HCons`

infixr 5 :::

infixr 5 `hconcat`

deriving stock instance Show (HList f '[])

deriving stock instance (Show (f x), Show (HList f xs)) => Show (HList f (x : xs))

deriving stock instance Eq (HList f '[])

deriving stock instance (Eq (f x), Eq (HList f xs)) => Eq (HList f (x : xs))