数据和新类型之间的惰性/严格性

Question

我很难理解为什么这两个 sn-ps 在所谓的“穷人严格分析”下会产生不同的结果。

第一个例子使用data（假设一个正确的Applicative实例）：

data Parser t a = Parser {
        getParser ::  [t] -> Maybe ([t], a) 
    }

> getParser (pure (,) <*> literal ';' <*> undefined ) "abc"
*** Exception: Prelude.undefined

第二个使用newtype。没有其他区别：

newtype Parser t a = Parser {
        getParser ::  [t] -> Maybe ([t], a) 
    }

> getParser (pure (,) <*> literal ';' <*> undefined ) "abc"
Nothing

literal x 是一个解析器，如果其参数与第一个标记匹配，则它会成功使用一个输入标记。所以在这个例子中，它失败了，因为; 不匹配a。但是，data 示例仍然看到下一个解析器未定义，而 newtype 示例没有。

我已阅读 this、this 和 this，但对它们的理解不够深入，无法理解为什么第一个示例未定义。在我看来，在这个例子中，newtype 比data 更懒惰，这与答案所说的相反。 （至少one other person 也被这个弄糊涂了）。

为什么从data 切换到newtype 会改变这个例子的定义？

---

这是我发现的另一件事：使用这个 Applicative 实例，上面的 data 解析器输出未定义：

instance Applicative (Parser s) where
  Parser f <*> Parser x = Parser h
    where
      h xs = 
        f xs >>= \(ys, f') -> 
        x ys >>= \(zs, x') ->
        Just (zs, f' x')

  pure a = Parser (\xs -> Just (xs, a))

而对于这个实例，上面的 data 解析器确实 not 输出未定义（假设 Parser s 的 Monad 实例正确）：

instance Applicative (Parser s) where
  f <*> x =
      f >>= \f' ->
      x >>= \x' ->
      pure (f' x')

  pure = pure a = Parser (\xs -> Just (xs, a))

---

完整代码sn-p：

import Control.Applicative
import Control.Monad (liftM)

data Parser t a = Parser {
        getParser ::  [t] -> Maybe ([t], a) 
    }


instance Functor (Parser s) where
  fmap = liftM

instance Applicative (Parser s) where
  Parser f <*> Parser x = Parser h
    where
      h xs = f xs >>= \(ys, f') -> 
        x ys >>= \(zs, x') ->
        Just (zs, f' x')

  pure = return


instance Monad (Parser s) where
  Parser m >>= f = Parser h
    where
      h xs =
          m xs >>= \(ys,y) ->
          getParser (f y) ys

  return a = Parser (\xs -> Just (xs, a))


literal :: Eq t => t -> Parser t t
literal x = Parser f
  where
    f (y:ys)
      | x == y = Just (ys, x)
      | otherwise = Nothing
    f [] = Nothing

Answer 1

您可能知道，data 和 newtype 之间的主要区别在于，data 的数据构造函数是惰性的，而 newtype 的数据构造函数是严格的，即给定以下类型

data    D a = D a 
newtype N a = N a

然后是D ⊥ `seq` x = x，但是N ⊥ `seq` x = ⊥。^{（其中⊥ 代表“底部”，即未定义的值或错误）}

然而，可能不太为人所知的是，当您在这些数据构造函数上进行模式匹配时， 角色是“颠倒的”，即与

constD x (D y) = x
constN x (N y) = x

然后是constD x ⊥ = ⊥（严格），但constN x ⊥ = x（懒惰）。

这就是您的示例中发生的情况。

Parser f <*> Parser x = Parser h where ...

对于data，<*> 定义中的模式匹配将立即分歧，如果 的参数是⊥，但使用newtype，构造函数被忽略，它是 就像你写的一样

f <*> x = h where

只有在需要x 时才会针对x = ⊥ 发散。

Answer 2

data 和 newtype 之间的区别在于 data 被“提升”而 newtype 不是。这意味着data 有一个额外的⊥——在这种情况下，这意味着undefined /= Parser undefined。当您的 Applicative 代码模式与 Parser x 匹配时，如果构造函数，它会强制使用 ⊥ 值。

当您在 data 构造函数上进行模式匹配时，它会被评估并拆开以确保它不是 ⊥。例如：

λ> data Foo = Foo Int deriving Show
λ> case undefined of Foo _ -> True
*** Exception: Prelude.undefined

所以data 构造函数上的模式匹配是严格的，并且会强制它。另一方面，newtype 的表示方式与其构造函数包装的类型完全相同。所以匹配 newtype 构造函数绝对没有任何作用：

λ> newtype Foo = Foo Int deriving Show
λ> case undefined of Foo _ -> True
True

可能有两种方法可以更改您的data 程序，使其不会崩溃。一种方法是在您的 Applicative 实例中使用无可辩驳的模式匹配，这将始终“成功”（但以后在任何地方使用匹配的值可能会失败）。每个newtype 匹配都表现得像一个无可辩驳的模式（因为严格来说没有可匹配的构造函数）。

λ> data Foo = Foo Int deriving Show
λ> case undefined of ~(Foo _) -> True
True

另一种方法是使用Parser undefined 而不是undefined：

λ> case Foo undefined of Foo _ -> True
True

此匹配将成功，因为 有一个有效的 Foo 值正在匹配。它恰好包含undefined，但这不相关，因为我们不使用它——我们只查看最顶层的构造函数。

---

除了您提供的所有链接之外，您可能还会发现 this article 相关。