☰

GHC が関数を線形として認識しないのはなぜですか? 質問する

tag-icon • tag-icon haskell linear-types
GHC が関数を線形として認識しないのはなぜですか? 質問する

非常にシンプルなスニペットがあります:

{-# 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が線形であるとは、その結果が1回だけ使用される場合、その引数も1回だけ使用されるという条件です。直感的には、fの定義のどの分岐でも、引数xは1回だけ使用されなければならないことを意味します。これは次のように行うことができます。

  • x を変更せずに返す
  • xを線形関数に渡す
  • x に対してパターン マッチングを行い、各引数を同じ方法で 1 回だけ使用します。
  • これを関数として呼び出し、同じ方法で結果を 1 回だけ使用します。

そして私の関数はsendToPeerまさにこれを実行します - パターンマッチを行いc、その引数はd1 回使用されます - は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

しかし、エラーは同じです。

ベストアンサー1

次のような複数の問題に直面しています:

  • Prelude.pureは線形ではありません。 のlinearクラスApplicativeと関連メソッド関数を使用する必要があります。pureControl.Functor.Linearlinear-base
  • Prelude.IOは線形ではありません (つまり、線形クラスのインスタンスを持っていません)。のからApplicativelinear を使用する必要があります。IOSystem.IO.Linearlinear-base
  • (GHC バージョン 9.2 より前) caseステートメントは、現在の拡張機能では正しく機能しませんでしたLinearTypes。

最後の点に関して、GHC マニュアルには次のように記載されています。

表現caseは、その精査One時間を、あるいはMany何回も消費する場合があります。しかし、推論は依然として実験的なものであり、精査Many時間を消費するはずだと過度に熱心に推測する可能性があります。

のユーザーズガイドはlinear-baseもっと率直です。そこには、ケース文は線形ではないこれは、線形関数には使用できないことを示唆しています。

case現時点では、式の性質を保持したい場合は、を使用した式の精査を避ける必要がありますOne。GHC バージョン 9.2 以降では、この回避策は不要になりました。

以下は型チェックされているようです。考えるインポートは推奨された方法で設定しました。とpureの両方にのバージョンがあり、動作が異なることに注意してください。Data.Functor.LinearControl.Functor.Linearドキュメンテーションモジュール用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)

おすすめ記事