fsfsd.idr

module Control.Monad.Codensity

import Control.Monad.Trans

import Control.Linear.LIO

public export
data Codensity : (m : Type -> Type) -> (a : Type) -> Type where
  MkCodensity : (1 _ : (forall b. (a -> m b) -> m b)) -> Codensity m a

runCodensity : Codensity m a -> (forall b. (a -> m b) -> m b)
runCodensity (MkCodensity x) = x

Functor (Codensity m) where
Applicative (Codensity m) where
Alternative (Codensity m) where
Monad (Codensity m) where
  
MonadTrans Codensity where
  lift x = MkCodensity $ (Prelude.(>>=) x)

-- Can it be done? Seems like I'd need an UnliftIO to bring my `m` down to IO so
-- I can use io_bind, or need a linear bind like the below version uses.
HasIO m => HasIO (Codensity m) where
  liftIO x = ?fsdf

-- Can be done, not sure what onus LinearIO puts on the user in practise.
-- LinearIO m => HasIO (Codensity m) where
  -- liftIO x = MkCodensity $ \1 act => bindL (liftIO x) act