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.

I'm not an Idris expert, but it should be the eta-expanded version of (->) Integer. Here, (->) is partially applied, but in \uv => (->) Integer uv it is fully applied. Both are eta-convertible. — chi
@chi ah right that makes sense. thanks. I think it confused me because I don't interpret types as first-order intuitively yet — corazza
Is it due to Idris functions being total? I don't know Idris well enough to come up with a good example, but it seems like the composition of two total functions is not, itself, guaranteed to be total. (My first try was something like (10.0 /) . (10.0 - ), although that function applied to 10 evaluates to Infinity.) — chepner
@chepner I could be wrong but I don't think Idris is a total language. It's turing-complete, and for example isn't 10.0 / not total itself? — corazza
@chepner The composition of two total functions is total, if it is well-typed at all. — Daniel Wagner

Jeroen Noels Jeroen Noels · Accepted Answer · 2018-05-10T10:30:43

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.

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

1 Answers