为什么在Haskell中箭头功能的递归绑定会无限循环？

Question

我正在通过为comm语言实现一个简单的解释器来学习如何在Haskell中使用Arrows 。

我有一个eval函数，该函数将一个表达式求值为一个值，但是当输入任何表达式时，eval会无限期地循环。

-- Interp.hs

eval :: A Expr Val
eval = proc e -> case e of
    Lit x -> returnA -< Num x
    Var s -> do
        lookup -< s
    Add e1 e2 -> do
        v1 <- eval -< e1
        v2 <- eval -< e2
        case (v1, v2) of
            (Num x, Num y) -> returnA -< Num (x + y)

在GHCI中执行此操作会导致无限循环

*Interp> unpack eval M.empty (Lit 1)

在添加表达式的情况下注释掉eval确实会导致表达式给出结果

例如

-- Interp.hs

eval :: A Expr Val
eval = proc e -> case e of
    Lit x -> returnA -< Num x
    Var s -> do
        lookup -< s
    Add e1 e2 -> do
        returnA -< Num 1
--        v1 <- eval -< e1
--        v2 <- eval -< e2
--        case (v1, v2) of
--            (Num x, Num y) -> returnA -< Num (x + y)

*Interp> unpack eval M.empty (Lit 1)
(Right (Num 1),fromList [])

这是有问题的代码。
使用的箭头是一种状态函数，在失败后会不断传递上下文。

{-# LANGUAGE Arrows #-}
{-# OPTIONS_GHC -Wall #-}
module Interp where

import Prelude hiding (lookup, fail)

import qualified Data.Map as M
import Control.Arrow
import Control.Category

data Expr
    = Lit Int
    | Var String
    | Add Expr Expr
    deriving (Show, Eq)

data Val
    = Num Int
    deriving (Show, Eq)

type Env = M.Map String Val

data A b c = A { unpack :: (Env -> b -> (Either String c, Env)) }

instance Category A where
    id = A (\env b -> (Right b, env))
    A g . A f = A $ \env b -> case f env b of
        (Left err, env') -> (Left err, env')
        (Right c, env') -> g env' c

instance Arrow A where
    arr f = A $ \env b -> (Right (f b), env)
    first (A f) = A $ \env (b, d) -> case f env b of
        (Left err, env') -> (Left err, env')
        (Right c, env') -> (Right (c, d), env')

instance ArrowChoice A where
    left (A f) = A $ \env e -> case e of
        Left b -> case f env b of
            (Left err, env') -> (Left err, env')
            (Right c, env') -> (Right (Left c), env')
        Right d -> (Right (Right d), env)

lookup :: A String Val
lookup = A $ \env k -> case M.lookup k env of
    Nothing -> (Left "Variable not bound", env)
    Just v -> (Right v, env)

eval :: A Expr Val
eval = proc e -> case e of
    Lit x -> returnA -< Num x
    Var s -> do
        lookup -< s
    Add e1 e2 -> do
        v1 <- eval -< e1
        v2 <- eval -< e2
        case (v1, v2) of
            (Num x, Num y) -> returnA -< Num (x + y)

Answer 1

有两种方法可以解决非终止问题：

1. A从data声明变为newtype声明。

2. first将和 的定义中的模式匹配改为left惰性的，即：

   first ~(A f) = A $ ...same as before...
   left ~(A f) = A $ ...same as before...
   

这两个修复都解决了相同的根本问题。来自StackOverflow 的另一个答案：

[使用data声明]，当与值构造函数进行模式匹配时，[thunks] 将至少被评估为弱头范式（WHNF）。[...] [使用newtype声明，] 当与值构造函数进行模式匹配时， [thunks] 根本不会被评估。

接下来，我将解释newtype和data声明之间的主要区别，然后我将解释它如何适用于您的案例。

newtype和的严格性质data

以下大部分内容是对同一主题的 HaskellWiki 文章进行释义和改编的。

newtype旨在引入与现有类型完全同构的类型。给定一个声明newtype T1 = T1 { unpack :: Int }，我们希望unpack . T1和id在类型上相等Int -> Int，同样 forT1 . unpack和id在类型上相等T1 -> T1。

但为什么这还没有成立data T2 = T2 { unpack :: Int }？也就是说，为什么T2 . unpack不一样id？原因是不可终止。T2 (unpack _|_)计算结果为T2 _|_，但id _|_计算结果为_|_（按照惯例，我用它_|_来代表非终止计算“底部”）。我们可以用下面的表达式来区分_|_和：T2 _|_

\x -> case x of T2 _ -> ()

将此 lambda 应用于_|_Yields _|_，但将此 lambda 应用于T2 _|_Yields ()。也就是说，因为构造函数T2可能保存非终止值，所以该语言可以区分_|_和T2 _|_。

该newtype声明给了我们一个也许令人惊讶的属性：T1 (unpack _|_)计算结果为_|_，但case _|_ of T1 _ -> ()计算结果为()! 也就是说，因为T1 _|_不旨在与 区分开，所以当与值构造函数进行模式匹配时，_|_语言不会强制评估类型的值。而且，正如我们很快就会看到的，这个属性对于递归定义很重要。T1T1

懒惰模式

有一种方法可以恢复data声明的类似 newtype 的行为：使用惰性模式匹配。给定一个如下函数：

f x = case x of ~(T2 y) -> \() -> y

你会发现 和 都f (T2 _|_)计算出一个值（即，一旦应用于参数就会发散的f _|_类型的函数）。Unit -> Int这是因为惰性模式匹配与该函数相同：

f = \x -> case x of t -> \() -> unpack t

因此 thunk 的求值以x“延迟”的方式传递，因为它仅unpack t在 lambda 主体中的求值时才求值\() -> unpack t。

示例中的 Newtype 与数据声明

我现在将对示例中的箭头符号进行脱糖，然后确定非终止的来源。

为了对箭头符号进行脱糖，我使用了该arrowp程序。这就是你的程序产生的结果：

$ arrowp-ext interp.hs
eval :: A Expr Val
eval
       = (arr
       (\ e ->
          case e of
              Lit x -> (Left) (x)
              Var s -> (Right) ((Left) (s))
              Add e1 e2 -> (Right) ((Right) ((e1, e2))))
       >>>
       (((arr (\ x -> Num x)) >>> (returnA)) |||
          (((arr (\ s -> s)) >>> (lookup)) |||
             (((first ((arr (\ e1 -> e1)) >>> (eval))) >>>
                 (arr (\ (v1, e2) -> (e2, v1))))
                >>>
                (first ((arr (\ e2 -> e2)) >>> (eval))) >>>
                  (arr
                     (\ (v2, v1) ->
                        case
                          case (v1, v2) of
                              (Num x, Num y) -> (x, y)
                          of
                            (x, y) -> Num (x + y)))
                    >>> (returnA)))))

您发现，eval当应用于参数时，它不会终止，但问题比这更严重：eval发散，句号。这可以在 ghci 中观察到：

*Interp> eval `seq` 0

不终止的最接近原因是表达式first ((arr (\ e1 -> e1)) >>> (eval))，它与 相同first eval。定义中的第一个参数first涉及与值构造函数 ( ) 的严格模式匹配first (A f)，并且A源自数据声明，因此，重新引用@wonder.mice：

[使用数据声明]，当与值构造函数进行模式匹配时，[thunks] 将至少被评估为弱头范式 (WHNF)。

当first eval在 的定义中遇到表达式时eval，thunk foreval尚未计算为 WHNF，因此当first eval尝试将其参数计算为 WHNF 时，它不会终止。

解决此问题的一种方法是更改A​​为newtype声明。（“1.A从data声明改为newtype声明。”）然后，

...当与值构造函数进行模式匹配时， [thunks] 根本不会被评估。

解决此问题的另一种方法是使用惰性模式匹配而不是严格匹配（“2. 将和 的first定义中的模式匹配更改为惰性模式”）。这将产生使模式匹配的行为与 newtype 声明相同的最终效果，其中“thunk 根本不会被评估”。firstleft

可以使用类似的解释来解释为什么|||在您的示例中没有以懒惰的方式表现，即使它对于例如 的 Arrow 实例也是如此(->)。更改left为使用惰性模式匹配将解决此问题，或者仅使用newtype声明就足够了。