[Agda] monad in Set

[Darin Morrison]

On Wed, Jun 17, 2009 at 5:05 AM, Dan Licata<drl at cs.cmu.edu> wrote:
> Hi everyone,
>
> Is there a way to describe the syntax of a monad, whose result type is
> an arbitrary Agda Set, without using Set1?  E.g.
>
>  data Comp (C : Set) : Set where
>    Return : C -> Comp C
>    Bind   : {A : Set} -> (A -> Comp C) -> (Comp A -> Comp C)
>
> doesn't work because of the A argument to Bind.

If you only need this because of the Comp monad, it might be easier to
instead avoid this problem by adapting your code to use the Delay
monad described by Capretta, Altenkirch, and Uustalu.

If you like I can show you some Agda modules for this monad along with
an example of how to use it to give a denotational interpreter for a
variant of PCF.

There's also some code in the Category.Monad.Partiality module in the
standard library that might be of interest.

-- 
Darin