In Haskell, functions are functors and the following code works as expected:
(*3) `fmap` (+100) $ 1
The output is 303 of course. However, in Idris (with fmap -> map), it gives the following error:
Can't find implementation for
Functor (\uv => Integer -> uv)
To me this seems like functions aren't implemented as functors in Idris, at least not like they are in Haskell, but why is that?
Furthermore, what exactly does the type signature (\uv => Integer -> uv) mean? It looks like some partially applied function, and that's what would be expected from a functor implementation, but the syntax is a bit confusing, specifically what \ which is supposed to be used for a lambda/literal is doing there.
Functor is an interface. In Idris, implementations are restricted to data or type constructors, i.e. defined using the data keyword. I am not an expert in dependent types, but I believe this restriction is required—practically, at least—for a sound interface system.
When you ask for the type of \a => Integer -> a at the REPL, you get
\a => Integer -> a : Type -> Type
In Haskell we would consider this to be a real type constructor, one that can be made into an instance of type classes such as Functor. In Idris however, (->) is not a type constructor but a binder.
The closest thing to your example in Idris would be
((*3) `map` Mor (+100)) `applyMor` 1
using the Data.Morphisms module. Or step by step:
import Data.Morphisms
f : Morphism Integer Integer
f = Mor (+100)
g : Morphism Integer Integer
g = (*3) `map` f
result : Integer
result = g `applyMor` 1
This works because Morphism is a real type constructor, with a Functor implementation defined in the library.