[Agda] Monads in std lib

[Wolfgang Jeltsch]

Am Donnerstag, 1. Oktober 2009 23:54:16 schrieb Anton Setzer:
> 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

The nice thing about this is that one type can have multiple instances of the 
same class. This is especially useful with very abstract classes where there 
is often more than one possible instance. For example, there are two sensible 
applicative functor instances for lists. This advantage over ordinary type 
classes makes me doubt that introducing type classes into Agda would be a good 
thing.

The downside is, of course, that we always have to say explicitely which 
instance we want, whereas Haskell chooses the one and only instance for us 
automatically.

Best wishes,
Wolfgang