[Agda] Indexed Monads

[Dan Doel]

On Monday 25 February 2008, Ulf Norell wrote:
> P.S.: If desired, I could provide the source for the delimited continuation
>
> > monad. I attempted to stick as close as possible to the format in
> > Category.Monad.State. Though it's nothing particularly complex (shift and
> > reset with a single prompt), it's another motivator for having/example of
> > indexed monads.
>
> That would be interesting.

All right. Attached is the continuation module (Continuation.agda), providing 
both a monad and a transformer. DContT and DCont could also support call/cc 
(the typing difference between it and shift/reset is similar to the 
difference between the ordinary state and indexed state monads, I believe), 
but I haven't bothered writing additional records for it.

I was going to provide an example of turning a monadic traversal of a list 
into a cursor, but Agda didn't like the usual cursor type:

  data Cursor (M : Set -> Set) (a : Set) : Set where
    done : Cursor M a
    stop : a -> M (Cursor M a) -> Cursor M a

because it has 'Cursor M a' in a negative position. So, unfortunately, at the 
moment I can only offer you the much less interesting example in 
ContTest.agda, which begins a traversal, and immediately aborts. The value of 
test is (1 ∷ []).

I've supplied as little implicit information as possible such that test has no 
unresolved metas, but most seems to be required. I do know that the '2' 
argument to shift can be elided while still yielding an answer, because it is 
arbitrary and never used. It's possible some others could be omitted with a 
similar lack of consequence, but I haven't tested such possibilities.

(My apologies if this appears at the top-level, and not in the same thread as 
the other messages. My mail client seems a bit confused about the list 
address for 'Reply to List'.)

Regards,
-- Dan
-------------- next part --------------
------------------------------------------------------------------------
-- A Delimited Continuation Monad
------------------------------------------------------------------------

module Category.Monad.Continuation where

open import Category.Applicative
open import Category.Applicative.Indexed
open import Category.Monad
open import Category.Monad.Indexed
open import Category.Monad.Identity

open import Data.Function

------------------------------------------------------------------------
-- Delimited Continuation Monads

DContT : {I : Set} -> (I -> Set) -> (Set -> Set) -> IFun I
DContT K M rق‚‚ rق‚ a = (a -> M (K rق‚)) -> M (K rق‚‚)

DCont : {I : Set} -> (I -> Set) -> IFun I
DCont K = DContT K Identity

DContTIMonad : forall {I}(K : I -> Set) {M} ->
               RawMonad M -> RawIMonad (DContT K M)
DContTIMonad K Mon = record
  { return = \a k -> k a
  ; _>>=_ = \c f k -> c (flip f k)
  }
  where open RawMonad Mon

DContIMonad : forall {I}(K : I -> Set) -> RawIMonad (DCont K)
DContIMonad K = DContTIMonad K IdentityMonad

------------------------------------------------------------------------
-- Delimited Continuation Operations

record RawIMonadDCont {I : Set} (K : I -> Set)
                      (M : I -> I -> Set -> Set) : Set1 where
  field
    monad : RawIMonad M
    reset : forall {rق‚ rق‚‚ rق‚ƒ} -> M rق‚ rق‚‚ (K rق‚‚) -> M rق‚ƒ rق‚ƒ (K rق‚)
    shift : forall {a rق‚ rق‚‚ rق‚ƒ rق‚„} -> ((a -> M rق‚ rق‚ (K rق‚‚)) -> M rق‚ƒ rق‚„ (K rق‚„)) -> M rق‚ƒ rق‚‚ a

  open RawIMonad monad public

DContTIMonadDCont : forall {I} (K : I -> Set) {M} ->
                    RawMonad M -> RawIMonadDCont K (DContT K M)
DContTIMonadDCont K Mon = record
  { monad = DContTIMonad K Mon
  ; reset = \e k -> e return >>= k
  ; shift = \e k -> e (\a k' -> (k a) >>= k') return
  }
  where
  open RawIMonad Mon

DContIMonadDCont : forall {I} (K : I -> Set) -> RawIMonadDCont K (DCont K)
DContIMonadDCont K = DContTIMonadDCont K IdentityMonad
-------------- next part --------------
module ContTest where

open import Category.Applicative.Indexed
open import Category.Monad.Indexed
open import Category.Monad.Continuation

open import Data.List
open import Data.Function
open import Data.Nat
open import Data.Product
open import Data.Unit

private
  module MonadUtil {I : Set}{M : IFun I}(Mon : RawIMonad M) where
    open RawIMonad Mon

    mapM : forall {i a b} -> (a -> M i i b) -> [ a ] -> M i i [ b ]
    mapM _ [] = return []
    mapM f (x ∷ xs) = _∷_ <$> f x <*> mapM f xs

natToType : ℕ -> Set
natToType 0 = [ ℕ ]
natToType 1 = ℕ
natToType n = ⊤

test : [ ℕ ]
test = runDCont {_} {0} natToType (reset {0} {0} {0}
                                    (mapM {0} (\a ->
                                      shift {_} {2} {0} {0} {0} (\k ->
                                        return {0} (a ∷ [])))
                                      (1 ∷ 2 ∷ 3 ∷ 4 ∷ [])))
  where
  runDCont : {I : Set}{r : I}(K : I -> Set) -> DCont K r r (K r) -> K r
  runDCont K e = e id
  open MonadUtil (DContIMonad natToType)
  open RawIMonadDCont (DContIMonadDCont natToType)