monads - 为什么 !-notation (bang-notation) 在 Idris REPL 中不起作用？

我预计这会评估为 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)

我也在没有顶级绑定(bind)的情况下尝试了这个并得到了

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

最佳答案

! -notation 如何脱糖的问题。

当您编写 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

Idris repl 没有什么特别之处，它就是类型检查器的工作方式。这就是为什么 Idris 教程中的 pure 函数中有 m_add 的原因:

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

关于monads - 为什么 !-notation (bang-notation) 在 Idris REPL 中不起作用？，我们在Stack Overflow上找到一个类似的问题：https://stackoverflow.com/questions/42987186/