Haskell程序以"循环"中止,但我认为不应该

Question

我有这个Haskell代码,当用GHC编译并运行时,检测到循环中止.

data Foo = Foo ()
 deriving (Eq,Show)

type Foop = Foo -> ((),Foo)

noOp :: Foop
noOp st = ((),st)

someOp :: Foop
someOp st@(Foo x) = ((),st)

(<+>) :: Foop -> Foop -> Foop
(<+>) f g st = let ((_,st'),(_,st'')) = ((f st),(g st')) in ((),st'')

main = print $ (noOp <+> someOp) $ Foo ()

我认为不应该,这里有一些修改.它们中的每一个都使循环消失:

• 改变data Foo以newtype Foo
• 改变(noOp <+> someOp)以(someOp <+> noOp)
• 消除解构 @(Foo x)

这是GHC中的错误还是我对评估过程缺乏了解？

Answer 1

• 模式匹配(_, _)需要WHNF (f st, g st').简单.
• 模式匹配(_, (_,_))需要WHNF g st'.这是问题所在,因为它g是严格的,因此它首先也需要st'在WHNF中.运行时st'在模式中找到((_,st'), (_,_)),因此在它实际遍历之前st'需要WHNF两个元组.因为g严格,这首先需要st'......等等.

如果您将结果g与惰性无可辩驳的模式匹配

(<+>) f g st = let ((_,st'), ~(_,st'')) = (f st, g st') in ((),st'')

然后问题消失了,因为这样评估:

• 模式匹配(_, _)需要WHNF (f st, g st').简单.
• 模式匹配(_, ~(_,_))暂时不再需要.
• 模式匹配((_,st'), ~(_,_))需要WHNF f st.幸运的是,我们可以实现这一点,因为st不依赖于模式.
• 现在我们已经满足模式匹配,运行时已经可以继续了in ((),st'').只有在这一点上才~(_,st'')强制使用无可辩驳的模式,但现在这不再st'是问题,因为这里可以使用,所以这只是一次计算的问题g.

你尝试过的修复程序都g非常严格:

消除解构 @(Foo _)

没有它,g实际上不需要查看它的参数来构造结果框架,即元组匹配(_,st'')可以在没有首先要求WHNF的情况下成功st'.

改变data Foo以newtype Foo

这会导致Foo构造函数在运行时实际上不存在,因此模式st@(Foo _)不会强制执行任何操作.

改变noOp <+> someOp以someOp <+> noOp

正如我所说,循环只是因为g严格而来.如果你把f它放在不严格的位置,那就没问题了.

Answer 2

这不是一个错误 - 你刚刚发现了懒惰模式语义的一个棘手的角落.让我提出一个更简单的案例:

> data Id a = Id a
> let Id a = undefined ; Id b = Id 3 in b
3
> let (Id a, Id b) = (undefined, Id 3) in b
*** Exception: Prelude.undefined

区别在于第一个let相当于

case undefined of
  ~(Id a) -> case Id 3  of
               ~(Id b) -> b

而第二个是

case (undefined, Id 3) of
  ~(Id a, Id b) -> b

第一个不会评估undefined除非a要求(不会发生).

对两种模式的第二意愿模式匹配Id a和Id b只要任一变量被要求,迫使这两个undefined和Id 3在过程中.

需要注意的是,因为这个问题,模式~(K1 (K2 x) (K3 y)),~(K1 ~(K2 x) (K3 y)),~(K1 (K2 x) ~(K3 y))并~(K1 ~(K2 x) ~(K3 y))有不同的语义.

要修复代码,请尝试

let (~(_,st'),~(_,st'')) = ((f st),(g st')) in ((),st'')

要么

let (_,st') = f st ; (_,st'') = g st' in ((),st'')