Why doesn't GHC recognize the function as linear?

Question

I have a very simple snippet:

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

I am on resolver: ghc-9.0.1.

From the 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.

and my function sendToPeer does exactly this - pattern-matches on c and its argument d is used once - in Peer d which is linear:

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

but I got an error:

• 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 =
   |            ^

Without pure:

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

but the error is the same.

Kirstiekirstin

Perhaps it thinks that pure is not linear? – Starlike

I removed pure and not do return Peer Busy, not IO (Peer Busy) - the error is same – Kirstiekirstin

Answer 1

You are bumping up against multiple problems:

• Prelude.pure isn't linear. You need to use the linear Applicative class and associated method function pure from Control.Functor.Linear in linear-base.
• Prelude.IO isn't linear (i.e., doesn't have an instance of the linear Applicative class). You need to use the linear IO from System.IO.Linear in linear-base.
• (In GHC versions older than 9.2) case statements simply didn't work properly with the current LinearTypes extension.

With respect tot the last point, the GHC manual states:

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.

The User's Guide for linear-base is blunter. It includes a section titled Case statements are not linear which suggests that you just can't use them for linear functions.

For now, you have to avoid scrutinizing an expression with case if you want to retain it's Oneness. On GHC version 9.2 or newer this workaround is no longer necessary.

The following appears to type-check. I think I've got the imports set up in the recommended manner. Note that there are versions of pure in both Data.Functor.Linear and Control.Functor.Linear, and they work differently. See the comments at the top of the documentation for the Data.Functor.Linear module.

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

Karyolymph

Answer 2

Use pure from Control.Functor.Linear instead, as well as the IO from System.IO.Linear, because contents of Prelude are simply not declared as linear.

Note that this even simpler example does not compile too:

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

---

The issue for the "without pure" version looks quite suspicious to me and I think it's a bug, because it seems to work if the pattern matching is done at the argument level:

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

Categorical

` Could not find module ‘Control.Functor.Linear’` Is it from linear-base? – Kirstiekirstin

Yes, stack install linear-base or the cabal equivalent. Remember to add it to the relevant config file in your project if you get errors about "hidden modules". – Categorical

On my configuration it seems to conflict with base, so be prepared to choose a proper resolver – Categorical

I removed pure at all from the shown code - the error is the same – Kirstiekirstin

also: Unknown package: linear-base on stack install linear-base. – Kirstiekirstin

Try one of these resolvers: stackage.org/package/linear-base/snapshots – Categorical

I think the case thing is fixed in 9.2, but I'm not sure. – Sunk

the same with let and where if I understand linearity rightly – Kirstiekirstin