Add Monad instance for Prelude.id

[madman-bob]

While Identity is better for most cases, you can occasionally get away with id instead. This has the benefit of not needing to wrap/unwrap your result.

[stefan-hoeck]

It would be nice if you could add some documentation about when to use this and when Identity would be the better choice, mabe with a concrete example. We should really try and have proper documentation in the standard libs.

[gallais]

The manual says:

Only one implementation of an interface can be given for a type — implementations may not overlap.

but this immediately creates overlapping definitions with every single implementation:
T a is just Prelude.id (T a) .

So I don't think this should get in.

[madman-bob]

As an example, consider defining State in terms of StateT. At the moment, we have wrapper functions for State, in terms of StateT, such as:

mapState : ((s, a) -> (s, b)) -> State s a -> State s b
mapState f = mapStateT $ \(Id p) => Id (f p)

Note that we wrap/unwrap the Id constructors.

If we were to use id instead of Identity, this could instead be

mapState : ((s, a) -> (s, b)) -> State s a -> State s b
mapState = mapStateT {m = id} {n = id}

Indeed, m and n are only written here for clarity, and in most cases you could simply use mapStateT instead of mapState.

The only cases were you couldn't would be when Idris needs to use the type of the function to determine the monad for StateT.

That said, we shouldn't change any of the existing transformers, for backwards compatibility.

With regards to overlapping definitions, I don't think Idris will detect any overlap, as an applied id will reduce to its argument. The only time Idris will detect this as a valid monad is when id is not applied to anything, such as in monad transformers. In this case, this is the monad we want.

That said, I can certainly understand the problem from a purity perspective. Would you prefer they be named implementations?

[buzden]

this immediately creates overlapping definitions with every single implementation

With regards to overlapping definitions, I don't think Idris will detect any overlap

At first, I also thought that claims of overlapping definitions are viable. But then I realised that it does not seem right. Functor (\a => a) is not the same as Functor a, which definitely creates an overlap.

I experimented with it shortly, and quick look indeed does not show any detected overlap:

interface X (0 m : Type -> Type) where
  h : m a -> m a

X List where
  h = id

X Prelude.id where
  h = id

f : List a -> List a
f = h

f' : a -> a
f' = h {m=id}

But what I can see here that X Prelude.id implementation is not found automatically anyway, which means that probably currently it's more convenient to use it as a named instance anyway.

Additionally, I thought if inability to find such an implementation is related to #2522

[madman-bob]

The benefit comes when using transformers.

To extend your example, consider types YT and Y, where YT is a Y transformer.

record YT (m : Type -> Type) (a : Type) where
    constructor MkYT
    y : m a

Y : Type -> Type
Y = YT id

g : X m => m a -> YT m a
g y = MkYT $ h y

g' : a -> Y a
g' = g

In the last line, the X Prelude.id instance is picked up automatically, as Y is short for YT id.

[gallais]

I'll just close this as it goes against the explicitly stated intentions behind interfaces.