为什么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

我在解析器上：ghc-9.0.1。

从文件中：

函数f是线性的，如果：当它的结果只消耗一次，那么它的参数只消耗一次。直观地说，这意味着在f定义的每一个分支中，它的参数x必须只使用一次。这可以通过

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

我的函数sendToPeer就是这样做的——模式匹配于c，它的参数d在对等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 =
   |            ^

没有纯：

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

但错误是一样的。

Answer 1

使用Control中的纯代码。函数。线性代替，以及系统中的IO。IO. Linear，因为前奏的内容根本没有声明为线性。

请注意，这个更简单的示例也不会编译：

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

“withoutpure”版本的问题在我看来非常可疑，我认为这是一个bug，因为如果在参数级别进行模式匹配，它似乎会起作用：

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

Answer 2

你遇到了多个问题：

• 前奏曲。纯不是线性的。您需要使用控件中的线性Applicative类和相关方法函数pure。函子。线性在线性基中

关于最后一点，GHC手册规定：

一个案例表达式可能会消耗它的scrutinee一次，或多次。但是这个推论仍然是实验性的，可能会过于急切地猜测它应该消耗scrutinee很多次。

线性基的用户指南更直截了当。它包括一个标题为Case statements not linear的部分，这表明你不能将它们用于线性函数。

现在，如果您想保留表达式的One特性，您必须避免检查带有case的表达式。

下面显示的是类型检查。我想我已经按照推荐的方式设置了进口。请注意，两种数据中都有pure的版本。函子。线性和控制。函子。线性，它们的工作方式不同。有关数据，请参见文档顶部的注释。函子。线性模块。

{-# 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)