syntax - 一元计算中的短路 "uninteresting"情况

标签 syntax pattern-matching monads agda

我有一个使用 Data.Maybe.monad 的函数,如下所示:

typeCheck ν (f · e) =
  typeCheck ν e >>= λ { (u , e′) →
  typeCheck ν f >>= λ { (u′ ▷ t , f′) →
  u !≡ₜ u′      >>= λ { refl →
  pure (, (f′ · e′)) };
  _ → nothing }}

有没有办法消除 _ → Nothing 情况,或者至少将其进一步向上移动(类似于 Idris)以获得类似于以下内容的内容:

typeCheck ν (f · e) =
  typeCheck ν e >>= λ { (u , e′) →
  typeCheck ν f >>= λ { _ → nothing; (u′ ▷ t , f′) →
  u ≡!ₜ u′      >>= λ { refl →
  pure (, (f′ · e′)) }}}

最佳答案

Agda 现在有 do-notation 。文档中的示例:

infer Γ (app e e₁) = do
  s ofType A => B ← infer Γ e
    where _ ofType nat → typeError "numbers cannot be applied to arguments"
  t ofType A₁     ← infer Γ e₁
  refl            ← A =?= A₁
  pure (app s t ofType B)

关于syntax - 一元计算中的短路 "uninteresting"情况,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/47375388/

相关文章:

python - python语法的正则表达式

c++ - 这两者在c++中有什么区别吗?

html - 用于定义特定站点内容/部分的 CSS3 方法

java - 从字符串中提取子字符串(包含动态部分)?

functional-programming - 如何使 `fun [x] -> x` 详尽无遗?

haskell - 将具有有效功能空间(如 ML)的语言核心嵌入到 Haskell 中有多实用?

algorithm - IBM 研究论文中的未知语法

haskell - 为什么 monad 类型类中应该存在 fail 方法?

haskell - 如何让 do block 提前返回?

haskell - 如何从属于产品 monad 的状态 monad 获取 `get` 当前状态?