Search code examples
polymorphismtype-inferenceidris

Idris type deriving for an arithmetic operation

In the following code

Idris> :t \x => x + x
\x => x + x : Integer -> Integer

Idris derives an Integer type for an x variable where I think it should derive an interface limitation like in Haskell: 

Haskell> :t (\x y -> x + y)
(\x y -> x + y) :: Num a => a -> a -> a

Then it does not even behave like an Integer, accepting a Double type: 

Idris> (\x => x + x) 2.0 
4.0 : Double

Can someone explain that to me?

Solution

  • I think in general it can be said that inspecting type inference in the REPL of idris is a bad idea. REPL code and code which exists in Idris files behaves differently.

    Your desired function would be written as:

    addy: Num a => a -> a -> a
addy x y = x + y

    and would have a type similiar to the one you expect from Haskell. Type inference in Idris is in general very weak (because it cannot be decided for dependently typed type systems).