Why do I need the Identity functor in Idris

Question

Although Idris is dependently typed, where values can be used freely in types, it still differentiate function id and functor Identity. Why can't I define Functor instances on id:

Functor id where
  map = id

The type of id is id : a -> a, why can't a be unified with Type, so that map @{Functor id} has type (a -> b) -> id a -> id b, which is just (a -> b) -> a -> b

I understand that Identity is a type wrapper but why do I need a separate id at type level, just to enable the implementation of typeclass instances.

The only difference of Identity and id is that Identity a cannot be evaluated to a, but it’s still a Type -> Type function, same as id {a=Type} in type.

Answer 1

id is a function which returns its input value as the result. When you need a function that does nothing to its input except return the same value, then use id.

Identity is a simple type wrapper which wraps a type t to produce a new type Identity t, where a value of type Identity t is a record containing just one value of the original wrapped type t.

Because Identity is an algebraic data type, it can implement an interface in Idris. In particular it implements Monad.

Sometimes one can define a type constructor that constructs types which implement Monad, by first defining a monad transformer that takes a monadic type as one of its parameters. To provide an arbitrary non-monad type as a parameter to such a constructor, first wrap the non-monad type using the Identity type constructor.

For an example, see the library module Control.Monad.Writer.