这个技巧如何进行类型检查？

Question

阅读这篇博文 – https://www.haskellforall.com/2021/05/the-trick-to-avoid-deeply-nested-error.html – 我意识到我不明白为什么“技巧”实际上有效这个情况：

{-# LANGUAGE NamedFieldPuns #-}

import Text.Read (readMaybe)

data Person = Person { age :: Int, alive :: Bool } deriving (Show)

example :: String -> String -> Either String Person
example ageString aliveString = do
    age <- case readMaybe ageString of
        Nothing  -> Left "Invalid age string"
        Just age -> pure age

    if age < 0
        then Left "Negative age"
        else pure ()

    alive <- case readMaybe aliveString of
        Nothing    -> Left "Invalid alive string"
        Just alive -> pure alive

    pure Person{ age, alive }

具体来说，我很难理解为什么会这样

    if age < 0
        then Left "Negative age"
        else pure ()

类型检查。

Left "Negative age" 有一种类型 Either String b

尽管

pure () 是类型 Either a ()

为什么它的工作方式如此？

---

编辑：我将代码简化并重新编写为绑定操作而不是do块，然后看到 Will 对他已经很好的答案的编辑：

    if age < 0
        then Left "Negative age"
        else pure ()

我认为这使得传递()通过绑定的“技巧”更加明显 - 值取自外部范围，而Left实际上使处理短路。

Answer 1

它类型检查因为Either String b并Either a ()成功统一，使用String ~ a和b ~ ()：

     Either String b
     Either a      ()
   ------------------
     Either String ()      a ~ String, b ~ ()

它出现在dotype的块中Either String Person，所以没关系，因为它是同一个 monad, Either，具有相同的“错误信号”类型，String。

它出现在块的中间，do没有值“提取”。所以它起到了守卫的作用。

它是这样的：如果是Right y，那么do块的翻译是

      Right y >>= (\ _ -> .....)

和计算里面继续.....与y忽略值。但如果是Left x，那么

      Left x >>= _  =  Left x

根据>>=for的定义Either。至关重要的是，Left x右侧是不相同的值Left x在左侧。左边的是 type Either String (); 右边的Either String Person确实有类型，正如do块整体的返回类型所要求的那样。

这两个Left x是两个不同的值，每个值都有自己的特定类型。该x :: String是一样的，当然。