Why doesn't (*3) `map` (+100) work in Idris?

Question

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.

Answer 1

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.