haskell - 为什么 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 .
来自 documentation :

A function f is linear if: when its result is consumed exactly once, then its argument is consumed exactly once. Intuitively, it means that in every branch of the definition of f, its argument x must be used exactly once. Which can be done by

• Returning x unmodified
• Passing x to a linear function
• Pattern-matching on x and using each argument exactly once in the same fashion.
• Calling it as a function and using the result exactly once in the same fashion.

和我的函数 sendToPeer正是这样做的 - c 上的模式匹配及其论点d使用一次 - 在 Peer d这是线性的:

By default, all fields in algebraic data types are linear (even if -XLinearTypes is not turned on).

但我得到一个错误:

• 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

但错误是一样的。

Answer 1

您遇到了多个问题:

Prelude.pure不是线性的。您需要使用线性 Applicative类和相关方法函数pure来自 Control.Functor.Linear在 linear-base .

Prelude.IO不是线性的(即没有线性 Applicative 类的实例)。您需要使用线性 IO来自 System.IO.Linear在 linear-base .

case语句根本无法与当前的 LinearTypes 一起正常工作扩大。

关于最后一点，GHC 手册指出:

A case expression may consume its scrutinee One time, or Many times. But the inference is still experimental, and may over-eagerly guess that it ought to consume the scrutinee Many times.

linear-base 的用户指南是直言不讳。它包括一个标题为 Case statements are not linear 的部分这表明您不能将它们用于线性函数。
现在，您必须避免使用 case 仔细检查表达式。如果你想保留它是One尼斯。
以下似乎是类型检查。我想我已经按照推荐的方式设置了导入。注意有 pure 的版本。在这两个 Data.Functor.Linear和 Control.Functor.Linear ，并且它们的工作方式不同。查看 documentation 顶部的评论对于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)