为什么不!-notation (爆炸符号)在Idris中工作？

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)

我也试过这个，没有一个托普莱尔绑定，并得到

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

Answer 1

问题的事实是如何!-notation脱糖。

当您编写1 + !x时，这基本上意味着x >>= \x' => 1 + x'。这个表达式不键入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)

但这是完美的：

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

因此，您应该添加pure以使其正常工作：

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

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

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