This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
-- Let Sem and Union be defined as they are in polysemy. | |
data Weaving e m a where | |
Weaving :: MonadTransControlish t | |
=> e q a | |
-> (forall x. q x -> t m x) | |
-> (forall z x. Monad z => t z x -> z (StT t x)) | |
-> (StT t a -> b) | |
-> Weaving e m b | |
class ( MonadTrans t |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
module WithWeaving where | |
import Polysemy | |
import Polysemy.Internal | |
import Polysemy.Internal.Union | |
import Polysemy.Reader | |
import Control.Monad.Reader (MonadReader) | |
import qualified Control.Monad.Reader as MTL | |
data Lift' m z a where |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
runReaderInMonadReader :: (Member (Lift' m) r, MonadReader i m) | |
=> Sem (Reader i ': r) a | |
-> Sem r a | |
runReaderInMonadReader (Sem sem) = sem $ \u -> case decomp u of | |
Right (Yo e s wv ex _) -> case e of | |
Ask -> ex . (<$ s) <$> sendM' Control.Monad.Reader.ask | |
Local f m -> fmap ex $ withWeaving $ \s' wv' _ -> | |
Control.Monad.Reader.local | |
f | |
(wv' ( runReaderInMonadReader (wv (m <$ s)) <$ s')) |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
{-# LANGUAGE GADTs, RankNTypes, DeriveFunctor, DeriveFoldable, StandaloneDeriving, ScopedTypeVariables #-} | |
module CofreeTraversable where | |
import Control.Applicative | |
import Data.Traversable | |
import Data.Functor.Identity | |
import Data.Functor.Compose | |
import Data.Coerce | |
import Unsafe.Coerce | |
{- |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
{-# LANGUAGE DerivingVia, StandaloneDeriving, PolyKinds, RankNTypes #-} | |
module DerivingViaPolyKinds where | |
class Foo (f :: k -> *) | |
newtype Bar (f :: k -> *) (a :: k) = Bar (f a) | |
-- deriving Foo via f -- Works | |
-- Standalone deriving instances only work if you instantiate the polykinded variable: |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
import Data.List.NonEmpty | |
--These are the definitions I'll use in my proof: | |
fmap :: (a -> b) -> NonEmpty a -> NonEmpty b | |
fmap f (a :| as) = f a :| Prelude.fmap f as | |
extract :: NonEmpty a -> a | |
extract (a :| _) = a | |
duplicate :: NonEmpty a -> NonEmpty (NonEmpty a) |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
{-# LANGUAGE RankNTypes, ScopedTypeVariables, ConstraintKinds, KindSignatures, MagicHash, TypeFamilies, AllowAmbiguousTypes, TypeApplications, FlexibleContexts, GADTs #-} | |
module LocalInstances where | |
import Control.Applicative | |
import Data.Bifunctor | |
import Data.List.NonEmpty | |
import Control.Arrow | |
import Data.Semigroup |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
{-# LANGUAGE RankNTypes #-} | |
module Como where | |
import Control.Comonad | |
import Control.Monad.Identity | |
import Control.Monad.Trans | |
-- The dual to Mo. | |
-- Simplified (still isomorphic): ComoT { runComoT' :: forall r. (a -> m (w r)) -> m r } | |
-- ComoT w Identity ~ forall r. (a -> w r) -> r | |
-- Unlike (Mo m Identity), (ComoT w Identity) is interesting in its own right. In fact, it gives rise to some really strange monads. See below. |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
{-# LANGUAGE RankNTypes, GADTs #-} | |
module Mo where | |
import Control.Comonad | |
import Control.Comonad.Trans.Class | |
import Control.Monad | |
{- | |
The monad-to-comonad transformer. | |
Originally, Mo was defined as the simpler (and isomorphic): | |
data Mo m w a where |