(\x=>2.0*x) `map` [1..10] "Can't find implementation for Enum Double"

Question

When I type that simple expression in the Idris interpreter it results in an error:

Idris> (\x=>2.0*x) `map` [1..10]
When checking an application of function Prelude.Functor.map:
        Can't find implementation for Enum Double

What exactly is going on?

I would expect this to work as List Int would be mapped into a List Double as the type of map allows for not retaining the original type of course.

Answer 1

The type of \x => 2.0 * x is Double -> Double and [from .. to] is syntactic sugar for enumFromTo with the following type -- Enum a => a -> a -> List a hence your expression expects to build a list of doubles, but can't since (predictably) there is no enumeration of doubles.

One possible solution is to explicitly cast letting Idris figure out the source and destination types:

Idris> (\x=>2.0 * (cast x)) `map` [1..10]
[2.0, 4.0, 6.0, 8.0, 10.0, 12.0, 14.0, 16.0, 18.0, 20.0] : List Double