[Agda] Monads in std lib

[Nils Anders Danielsson]

On 2009-10-01 22:54, Anton Setzer wrote:
> One limitations is that we can open only one class at a time, since
> we don't have any polymorphism.

By using a universe one can open several instances at the same time:

  module Class where

  open import Category.Monad
  open import Data.List as List
  open import Data.Maybe as Maybe hiding (maybe)
  open import Data.Nat
  open import Data.Product

  data U : Set where
    list  : U
    maybe : U

  El : U → (Set → Set)
  El list  = List
  El maybe = Maybe

  M : (u : U) → RawMonad (El u)
  M list  = List.monad
  M maybe = Maybe.monad

  foo : List ℕ × Maybe ℕ
  foo = (return 0 , return 0)
    where open module M {u} = RawMonad (M u)

-- 
/NAD



This message has been checked for viruses but the contents of an attachment
may still contain software viruses, which could damage your computer system:
you are advised to perform your own checks. Email communications with the
University of Nottingham may be monitored as permitted by UK legislation.