为什么 GHC 无法识别该函数为线性函数？

Question

我有一个非常简单的代码片段：

{-# LANGUAGE LinearTypes #-}

module Lib where

data Peer st = Peer { data :: String } deriving Show

data Idle
data Busy

sendToPeer :: Peer Idle %1-> Int -> IO (Peer Busy)
sendToPeer c n = case c of Peer d -> pure $ Peer d

我正在使用resolver: ghc-9.0.1。

根据文档：

一个函数 f 是线性的，如果：当其结果恰好被消耗一次时，它的参数也恰好被消耗一次。直觉上，这意味着在 f 的定义的每个分支中，其参数 x 必须恰好使用一次。这可以通过以下方式实现：

• 返回未修改的 x
• 将 x 传递给线性函数
• 对 x 进行模式匹配，并以相同方式使用每个参数仅一次。
• 作为函数调用，并以相同方式使用结果仅一次。

而我的 sendToPeer 函数正是这样做的——在 c 上进行模式匹配，其参数 d 仅在 Peer d 中被使用一次，这是线性的：

默认情况下，代数数据类型中的所有字段都是线性的（即使没有打开 -XLinearTypes）。

但是我收到了一个错误：

• Couldn't match type ‘'Many’ with ‘'One’
        arising from multiplicity of ‘c’
• In an equation for ‘sendToPeer’:
          sendToPeer c n = case c of { Peer d -> pure $ Peer d }
   |
11 | sendToPeer c n =
   |            ^

没有 pure:

sendToPeer :: Peer Idle %1-> Int -> Peer Busy
sendToPeer c n = case c of Peer d -> Peer d

但是错误依旧存在。

- RandomB

---

也许它认为“纯粹”并非线性的？ - md2perpe

我删除了 pure 并且不会返回 Peer Busy，而是返回 IO (Peer Busy) - 错误相同。 - RandomB

Answer 1

你正面临多个问题：

- Prelude.pure 不是线性的。你需要使用线性的 Applicative 类和相关的方法函数 pure，来自 linear-base 的 Control.Functor.Linear。 - Prelude.IO 不是线性的（即没有线性的 Applicative 类的实例）。你需要使用 linear-base 的 System.IO.Linear 中的线性 IO。 - （在 GHC 版本早于 9.2 的情况下）case 语句与当前的 LinearTypes 扩展不兼容。

关于最后一点，GHC 手册中提到： > case 表达式可以消耗它的判断表达式一次，或多次。但推断仍然是实验性的，并且可能过于急切地猜测它应该多次消耗判断表达式。 linear-base的用户指南更加直接。其中包含一个名为Case statements are not linear的部分，建议您不能将其用于线性函数。

目前，如果您想保留其Oneness，就必须避免使用case来详细检查表达式。在GHC版本9.2或更新版本中，这种解决方法不再必要。

以下内容似乎可以通过类型检查。我认为我已按照推荐的方式设置了导入项。请注意，Data.Functor.Linear和Control.Functor.Linear中都有pure的版本，并且它们的工作方式不同。请参阅Data.Functor.Linear模块的文档顶部的注释。

{-# LANGUAGE LinearTypes #-}

module Lib where

import Prelude.Linear
import Control.Functor.Linear as Control
import qualified Prelude as NonLinear
import qualified System.IO.Linear as Linear

data Peer st = Peer String deriving Show

data Idle
data Busy

sendToPeer :: Peer Idle %1-> Int -> Linear.IO (Peer Busy)
sendToPeer (Peer d) n = Control.pure (Peer d)

- K. A. Buhr

Answer 2

请使用Control.Functor.Linear中的pure以及System.IO.Linear中的IO，因为Prelude中的内容并没有被声明为线性的。请注意，即使是这个更简单的例子也无法编译。

sendToPeer :: Peer Idle %1-> IO (Peer Idle)
sendToPeer c = pure c

---

"没有纯"版本的问题对我来说看起来非常可疑，我认为这是一个错误，因为如果在参数级别进行模式匹配，它似乎可以工作：

sendToPeer :: Peer Idle %1-> Int -> Peer Busy
sendToPeer (Peer d) n = Peer d

- radrow

---

无法找到模块“Control.Functor.Linear”。这个模块是否来自linear-base？ - RandomB

是的，stack install linear-base 或者 cabal 等价命令。如果出现“隐藏模块”错误，请记得将其添加到项目的相关配置文件中。 - radrow

尝试使用以下解析器之一：https://www.stackage.org/package/linear-base/snapshots - radrow

我认为case的问题在9.2中已经解决了，但我不确定。 - dfeuer

如果我正确理解线性，那么let和where应该是相同的。 - RandomB