idris-lang / Idris-dev

A Dependently Typed Functional Programming Language
http://idris-lang.org
Other
3.44k stars 644 forks source link

Error(?) instantiating Monad following the tutorial: Main.return not a method of class Monad #1503

Closed fabriceleal closed 10 years ago

fabriceleal commented 10 years ago

I'm not really sure what's going on, I might be missing something.

So, following the tutorial on the "4.3 Monads and do-notation" section, I defined a Maybe clone:

data Maybe2 a =
     Nothing
     | Just a

and tried to create an instance of Monad (is this the right terminology?) with it:

instance Monad Maybe2 where
    return = Just

    Nothing >>= k = Nothing
    (Just x) >>= k = k x

however, I get:

Main.return not a method of class Monad

commenting the "return = ..." line yields the error:

When elaborating right hand side of Maybe2 instance of Prelude.Monad.Monad:
Can't resolve type class Applicative Maybe2

I needed to instantiate Applicative and Functor to make this work. Here is a full working listing:

module Main

data Maybe2 a =
     Nothing
     | Just a

instance Functor Maybe2 where
         map f Nothing = Nothing
         map f (Just a) = Just (f a)

instance Applicative Maybe2 where
         pure = Just

         Nothing  <$> a = Nothing

         (Just f) <$> Nothing = Nothing
         (Just f) <$> (Just a) = Just (f a)

instance Monad Maybe2 where
--    return = Just

    Nothing >>= k = Nothing
    (Just x) >>= k = k x
fabriceleal commented 10 years ago

version: 0.9.14.2

david-christiansen commented 10 years ago

Hello Fabrice,

The error message is actually quite accurate:

> :doc Monad
Type class Monad

Parameters:
    m

Methods:
    (>>=) : Monad m => m a -> (a -> m b) -> m b

        infixl 5

As you can see, Monad does not have a return method. This is because it should be the same thing as Applicative.pure. Indeed, we can look at the documentation for return:

> :doc return
return : a -> Eff a xs (\v => xs)

return : Monad m => a -> m a
    For compatibility with Haskell. Note that monads are not
    free to define return and pure differently!

So I'll close this as "not a bug" so far, as I think the docs are there.

fabriceleal commented 10 years ago

Ok, I see; however I think that the tutorial should be updated in this section, as it has the snippet:

instance Monad Maybe where
    return = Just
    Nothing >>= k = Nothing
    (Just x) >>= k = k x
david-christiansen commented 10 years ago

That's definitely a problem! I created https://github.com/idris-lang/idris-tutorial/issues/38 to track the issue with the tutorial. Thanks!

fabriceleal commented 10 years ago

Didn't knew about the repo for the tutorial, will post new issues there :)