[Agda] Some newbie questions

[Darin Morrison]

On Nov 21, 2008, at 11:58 AM, J.Burton at brighton.ac.uk wrote:

> Hi, how do I use monad instances? If I import Data.List or Data.Maybe
> then return >>= are apparently not in scope.
>

Here's a short example:

module MonadExample where

open import Category.Monad
open import Data.Maybe
open import Data.Nat

open module M = RawMonad MaybeMonad

maybeAdd : Maybe ℕ -> Maybe ℕ -> Maybe ℕ
maybeAdd x y = x >>= \ x' ->
                y >>= \ y' ->
                return (x' + y')



The key is that you need to bring the fields from the MaybeMonad  
record in the Data.Maybe module into scope.  This is explained a bit  
more here:

http://appserv.cs.chalmers.se/users/ulfn/wiki/agda.php?n=ReferenceManual.Records

> I'm confused about lambdas too...can I pattern match over their
> arguments? Here is a simplified version of something I was trying to
> do:
>
> data T ℕ : Set where
> S : ℕ -> T ℕ
>
> h : T ℕ -> ℕ
> h = \ S i -> i
>
> gives the error "ℕ != (i : _26 S) -> _27 S i of type Set
> when checking that the expression \i -> i has type ℕ"
>
> Adding brackets to get `\ (S i) -> i' doesn't help: "Parse error
> )<ERROR>
>  -> i"
>

I'm pretty sure you can't pattern match with lambdas.

Regards,
Darin