haskell - 为什么 Haskell 中箭头函数的递归绑定(bind)会无限循环？

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)

在 Add 表达式的情况下注释掉 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

有两种方法可以修复非终止:

更改 A来自 data声明 newtype宣言。

更改 first 定义中的模式匹配和 left懒惰，即:

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

这两个修复都解决了相同的根本问题。来自 another StackOverflow answer:

[With data declarations], when pattern matching against value constructors, [thunks] WILL be evaluated at least to weak head normal form (WHNF). [...] [With newtype declarations,] when pattern matching against value constructors, [thunks] WILL NOT be evaluated at all.

继续，我将解释 newtype 之间的主要区别和 data声明，然后我将解释它如何适用于您的情况。
newtype 的严格属性和 data
以下大部分内容改编自 the HaskellWiki article on the same topic .
newtype旨在引入与现有类型完全同构的类型。给定声明 newtype T1 = T1 { unpack :: Int } , 我们要 unpack . T1和 id在类型 Int -> Int 处相等，同样适用于 T1 . unpack和 id在类型 T1 -> T1 处相等.

但是为什么这对 data T2 = T2 { unpack :: Int } 来说还没有成立？ ;也就是说，为什么是 T2 . unpack与 id 不一样?原因是不终止。 T2 (unpack _|_)计算结果为 T2 _|_ ，但是 id _|_计算结果为 _|_ (我使用 _|_ 来代表非终止计算“底部”，这是惯例)。我们可以区分_|_和 T2 _|_使用以下表达式:
\x -> case x of T2 _ -> ()
将此 lambda 应用于 _|_ yield _|_ ，但将此 lambda 应用于 T2 _|_ yield () .也就是说，因为构造函数 T2可能包含一个非终止值，该语言可以区分 _|_和 T2 _|_ .
newtype声明给了我们一个可能令人惊讶的属性:T1 (unpack _|_)计算结果为 _|_ ，但是 case _|_ of T1 _ -> ()计算结果为 () !也就是说，因为 T1 _|_无意与 _|_ 区分开来，该语言不强制对 T1 类型的值进行评估当模式匹配 T1值构造器。而且，我们很快就会看到，这个属性对于递归定义很重要。

懒人模式

有一种方法可以恢复 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 program .这是它在您的程序中产生的结果:

$ 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 :

[With data declarations], when pattern matching against value constructors, [thunks] WILL be evaluated at least to weak head normal form (WHNF).

当表达式 first eval在eval的定义中遇到, 重击 eval尚未评估为 WHNF，因此当 first eval尝试评估其对 WHNF 的参数，它不会终止。

解决此问题的一种方法是更改​​ A到 newtype宣言。 (“1. 将 A 从 data 声明更改为 newtype 声明。”)然后，

...when pattern matching against value constructors, [thunks] WILL NOT be evaluated at all.

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

为什么||| 可以使用类似的解释。对于您的示例，行为并不懒惰，即使它确实用于例如(->) 的 Arrow 实例.换 left使用惰性模式匹配可以解决这个问题，或者只使用 newtype声明就足够了。