Why not? -notation (bang-notation) works in the Idris REPL?
I was expecting this to evaluate to 3, but it gets 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 toplevel binding and got
Idris> let y = Just 2 in !y + 1
Maybe b is not a numeric type
+3
source to share
1 answer
The problem is how !
-notation desugars.
When you write 1 + !x
, it basically means x >>= \x' => 1 + x'
. And this expression does not print the 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 great:
Idris> x >>= \x' => pure (1 + x')
Just 3 : Maybe Integer
So, you have to add pure
in order for everything to work:
Idris> pure (1 + !x)
Just 3 : Maybe Integer
Nothing special about Idris's line, this is how type checking works. That's why in the textbook Idris has pure
in m_add
:
m_add : Maybe Int -> Maybe Int -> Maybe Int
m_add x y = pure (!x + !y)
+4
source to share