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

html5 • • 问答

阅读这篇博文 – 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实际上使处理短路。

回答

它类型检查因为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是一样的，当然。

  • @larek, yes, but the two `if` branches still have to match. And here they do, because one can have anything on the left, and the other can have anything on the right.
以上是这个技巧如何进行类型检查？的全部内容。
THE END
分享
二维码
< <上一篇
下一篇>>