爲什麼不在Idris REPL中使用-notation（bang-notation）？

Question

我預計今年以評估3，但得到了一個錯誤，而不是：

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) 

我也試過這個沒有一個頂級的結合，並在事實上如何! -notation desugars了

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

Answer 1

問題。

當您編寫1 + !x這基本上意味着x >>= \x' => 1 + x'。而這個表達式不會檢查類型。

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) 

但這種完美的作品：

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

所以，你應該添加pure，使事情的工作：

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

沒什麼特別伊德里斯 REPL，它是多麼類型檢查作品。這就是爲什麼有來自伊德里斯教程pure在m_add功能：

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