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

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 对他已经非常出色的答案的编辑：

{-# LANGUAGE NamedFieldPuns #-}

import           Text.Read (readMaybe)

newtype Person = Person { age :: Int} deriving (Show)

example :: String -> Either String Person
example ageString =
    getAge ageString
    >>= (\age -> checkAge age
        >>= (\()-> createPerson age))

getAge :: Read b => String -> Either [Char] b
getAge ageString = case readMaybe ageString of
       Nothing  -> Left "Invalid age string"
       Just age -> pure age

checkAge :: (Ord a, Num a) => a -> Either [Char] ()
checkAge a = if a < 0
       then Left "Negative age"
       else pure ()

createPerson :: Applicative f => Int -> f Person
createPerson a = pure Person { age = a }

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

Answer 1

因为Either String b 和Either a () 统一成功，所以会进行类型检查，String ~ a 和b ~ ()：

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

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

它出现在do 块的中间，并且没有“提取”值。所以它作为一个守卫。

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

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

然后计算在..... 内部继续，y 值被忽略。但如果是Left x，那么

      Left x >>= _  =  Left x

根据>>= 的定义为Either。至关重要的是，右侧的 Left x 与左侧的 Left x 的值不相同。左边的类型为Either String ()；右边的确实有 Either String Person 类型，这是 do 块整体的返回类型所要求的。

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