Why doesn't !-notation (bang-notation) work in Idris REPL?

3
votes

I expected this to evaluate to 3, but got an error instead:

Idris> :let x = Just 2
Idris> 1 + !x
(input):1:3-4:When checking an application of function Prelude.Interfaces.+:
        Type mismatch between
                Integer (Type of (_bindApp0))
        and
                Maybe b (Expected type)

I also tried this without a toplevel binding and got

Idris> let y = Just 2 in !y + 1
Maybe b is not a numeric type
1
monadsidris

1 Answers

4
votes

Problem in the fact how !-notation desugars.

When you write 1 + !x this basically means x >>= \x' => 1 + x'. And this expression doesn't type check.

Idris> :let x = Just 2
Idris> x >>= \x' => 1 + x'
(input):1:16-17:When checking an application of function Prelude.Interfaces.+:
        Type mismatch between
                Integer (Type of x')
        and
                Maybe b (Expected type)

But this works perfectly:

Idris> x >>= \x' => pure (1 + x')
Just 3 : Maybe Integer

So you should add pure to make things work:

Idris> pure (1 + !x)
Just 3 : Maybe Integer

Nothing special in Idris repl, it is just how type checker works. That's why there is pure in m_add functions from Idris tutorial:

m_add : Maybe Int -> Maybe Int -> Maybe Int
m_add x y = pure (!x + !y)