[Agda] Monads in std lib

[Anton Setzer]

Nils Anders Danielsson wrote:
> On 2009-10-01 12:07, Jim Burton wrote:
>> Tips?
>
> module MonadExample where
>
> open import Category.Monad
> open import Data.Maybe as Maybe
> open import Data.Nat
>
> maybeAdd : Maybe ℕ → Maybe ℕ → Maybe ℕ
> maybeAdd x y = x >>= λ x' →
>               y >>= λ y' →
>               return (x' + y')
>  where open RawMonad Maybe.monad
>
That's nice.

So essentially we can simulate classes from Haskell
so some extent in Agda as follows:

Define

record MyClass (A : Set) : Set where
    field
        op1
        op2
        ...
   op 3     {- derivable operation -}

-- Now define a set
Myset : Set
Myset = ?

-- show that it is an instnace of MyClass
mySetIsMyClass : MyClass Myset
mySetIsMyClass = record {
        op1 = ...
        ; op2 = ...   }

-- Now we can use this as follows
f : A -> B
f a = t
         where open MyClass mySetIsMyClass

And in t we can use op1 op2 op3

One limitations is that we can open only one class at a time, since
we don't have any polymorphism.
And, as in the Monad example. the parameters of MyClass can be arbitrary,
in case of Monad it is Set -> Set.

Anton

-- 
---------------------------------------
Anton Setzer
Department of Computer Science
Swansea University
Singleton Park
Swansea SA2 8PP
UK

Telephone:
(national)        (01792) 513368
(international) +44 1792  513368
Fax:
(national)        (01792) 295708
(international) +44 1792  295708
Visiting address:
Faraday Building,
Computer Science Dept.
2nd floor, room 211.
Email: a.g.setzer at swan.ac.uk
WWW:
http://www.cs.swan.ac.uk/~csetzer/
---------------------------------------