{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE DerivingStrategies #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
module Haskus.Utils.EADT
( EADT
, (:<:)
, (:<<:)
, pattern VF
, appendEADT
, liftEADT
, popEADT
, AlterEADT
, alterEADT
, AlgEADT
, algEADT
, eadtToCont
, eadtToContM
, contToEADT
, contToEADTM
, module Haskus.Utils.Functor
, module Haskus.Utils.VariantF
)
where
import Haskus.Utils.VariantF
import Haskus.Utils.Variant
import Haskus.Utils.Functor
import Haskus.Utils.Types.List
import Haskus.Utils.Types
import Haskus.Utils.ContFlow
import GHC.Exts (Constraint)
import Control.DeepSeq
type EADT xs = Fix (VariantF xs)
deriving newtype instance NFData (VariantF xs (EADT xs)) => NFData (EADT xs)
type family f :<: xs where
f :<: xs = EADTF' f (EADT xs) xs
type family (:<<:) xs ys :: Constraint where
'[] :<<: ys = ()
(x ': xs) :<<: ys = (x :<: ys, xs :<<: ys)
type EADTF' f e cs =
( Member f cs
, Index (IndexOf (f e) (ApplyAll e cs)) (ApplyAll e cs) ~ f e
, PopVariant (f e) (ApplyAll e cs)
, KnownNat (IndexOf (f e) (ApplyAll e cs))
, Remove (f e) (ApplyAll e cs) ~ ApplyAll e (Remove f cs)
)
pattern VF :: forall e f cs.
( e ~ EADT cs
, f :<: cs
) => f (EADT cs) -> EADT cs
pattern VF x = Fix (VariantF (VSilent x))
appendEADT :: forall ys xs zs.
( zs ~ Concat xs ys
, ApplyAll (EADT zs) zs ~ Concat (ApplyAll (EADT zs) xs) (ApplyAll (EADT zs) ys)
, Functor (VariantF xs)
) => EADT xs -> EADT zs
appendEADT (Fix v) = Fix (appendVariantF @ys (fmap (appendEADT @ys) v))
liftEADT :: forall e as bs.
( e ~ Fix (VariantF bs)
, LiftVariantF as bs e
, Functor (VariantF as)
) => EADT as -> EADT bs
liftEADT = cata (Fix . liftVariantF)
popEADT :: forall f xs e.
( f :<: xs
, e ~ EADT xs
, f e :< ApplyAll e xs
) => EADT xs -> Either (VariantF (Remove f xs) (EADT xs)) (f (EADT xs))
popEADT (Fix v) = popVariantF v
type AlterEADT c xs = AlterVariantF c (EADT xs) xs
alterEADT :: forall c xs.
( AlterEADT c xs
) => (forall f. c f => f (EADT xs) -> f (EADT xs)) -> EADT xs -> EADT xs
alterEADT f (Fix v) = Fix (alterVariantF @c @(EADT xs) f v)
type AlgEADT c r xs = AlgVariantF c (EADT xs) r xs
algEADT :: forall c r xs.
( AlgEADT c r xs
) => (forall f. c f => f (EADT xs) -> r) -> EADT xs -> r
algEADT f (Fix v) = algVariantF @c @(EADT xs) @r f v
eadtToCont ::
( ContVariant (ApplyAll (Fix (VariantF xs)) xs)
) => Fix (VariantF xs) -> ContFlow (ApplyAll (Fix (VariantF xs)) xs) r
eadtToCont (Fix v) = variantFToCont v
eadtToContM ::
( ContVariant (ApplyAll (Fix (VariantF xs)) xs)
, Monad m
) => m (Fix (VariantF xs))
-> ContFlow (ApplyAll (Fix (VariantF xs)) xs) (m r)
eadtToContM f = variantFToContM (unfix <$> f)
contToEADT ::
( ContVariant (ApplyAll (Fix (VariantF xs)) xs)
) => ContFlow (ApplyAll (Fix (VariantF xs)) xs)
(V (ApplyAll (Fix (VariantF xs)) xs))
-> Fix (VariantF xs)
contToEADT c = Fix (contToVariantF c)
contToEADTM ::
( ContVariant (ApplyAll (Fix (VariantF xs)) xs)
, Monad f
) => ContFlow (ApplyAll (Fix (VariantF xs)) xs)
(f (V (ApplyAll (Fix (VariantF xs)) xs)))
-> f (Fix (VariantF xs))
contToEADTM f = Fix <$> contToVariantFM f