ymdryo
commented
11 months ago new version interface idea
infixr 4 !!
infixr 3 !
-- `Effectful` monads for general purposes.
type (!!) = EffEK :: SigClass -> InsClass -> Type -> Type
type (!) = EffFEK :: InsClass -> Type -> Type
toF :: NopS !! f ~> (!) f
toF = ...
class HeftiaEff (he :: SigClass -> InsClass -> Type -> Type) where ...
class FreerEff (fr :: InsClass -> Type -> Type) where ...
instance (Heftia he, Union uh, UnionF uf) => HeftiaEff (Eff uh uf he)
instance (Heftia he, UnionF uf) => FreerEff (Eff uh uf he NopS)
instance (Freer fr, UnionF u) => FreerEff (EffF u fr)
-- | A common monad wrapper data type for representing effectful programs.
newtype Eff (uh :: [SigClass] -> SigClass) (uf :: [InsClass] -> InsClass) heftia hs fs =
Eff { unEff :: Effectful heftia (AsUnion uh (SumToList hs)) (AsUnionF uf (SumToListF fs)) }
type EffE = Eff ExtensibleUnion ExtensibleUnionF
type EffEK = EffE HeftiaChurch
type EffETree = EffE HeftiaTree
type Effectful heftia h f = heftia (h :+: LiftIns f) :: Type -> Type
type EffectfulK = Effectful HeftiaChurch
type EffectfulTree = Effectful HeftiaTree
newtype EffF (u :: [InsClass] -> InsClass) freer fs = EffF { unEffF :: freer (AsUnionF u (SumToListF fs)) }
type EffFE = Eff ExtensibleUnionF
type EffFEK = EffFE FreerChurch
type EffFETree = EffFE FreerTree
type InsClass = Type -> Type
type SigClass = (Type -> Type) -> Type -> Type
infixr 5 +, :+:
data f + g = ... -- Functor sum
data h1 :+: h2 = ... -- HFunctor sum
data NopI (a :: Type)
type NopS = LiftIns NopI
data ExtensibleUnionF :: [InsClass] -> InsClass
data ExtensibleUnion :: [SigClass] -> SigClass
-- Enclose the sums as a linear list in the right-associative direction.
type family SumToListF f :: InsClass -> [InsClass] where
SumToListF (f + g) = f ': SumToListF g
SumToListF NopI = '[]
SumToListF f = '[f]
type family SumToList h :: SigClass -> [SigClass] where
SumToList (h1 :+: h2) = h1 ': SumToList h2
SumToList NopS = '[]
SumToList h = '[h]
type family AsUnionF u fs :: ([InsClass] -> InsClass) -> [InsClass] -> InsClass where
AsUnionF u '[] = NopI
AsUnionF u '[f] = f
AsUnionF u fs = u fs
type family AsUnion u hs :: ([SigClass] -> SigClass) -> [SigClass] -> SigClass where
AsUnion u '[] = NopS
AsUnion u '[h] = h
AsUnion u hs = u hs
By using the interface, we can expect to be able to write as follows:
saveLogChunk ::
forall h f.
( LogChunkS <<| h
, LogI <| f
, FileSystemI <| f
, TimeI <| f
, HFunctor h
) =>
LogChunkS :+: h !! LogI + f ~> h !! LogI + fteletypeToIO :: IO <| r => (!) (TeletypeS + r) ~> (!) r
or
teletypeToIO :: IO <| r => TeletypeS + r ! a -> r ! ainstead of:
saveLogChunk ::
forall es es' m.
( LogChunkS <<| es
, LogI <| es'
, FileSystem (Fre es' m)
, Time (Fre es' m)
, Monad m
, ForallHFunctor es
) =>
Hef (LogChunkS ': es) (Fre (LogI ': es') m) ~> Hef es (Fre (LogI ': es') m)teletypeToIO :: (IO <: Fre es m, Monad m) => Fre (TeletypeI ': es) m ~> Fre es mNote that for the paper, the left and right sides of the ! and !! operators are swapped.
Keeping these as separate data types or interfaces doesn’t seem to be very convenient.