The current implementation (GHC 9.0.1) for LinearTypes has limitations that let
and where
bindings are not linear.
Until now, I've been able to work around this using explicit functions as suggested in the user guide. However, when trying to implement function (from ArrowLoop
, for the curious), I've run out of workarounds. How does one introduce recursion without a let or where binding?
loop :: ((b,d) ⊸ (c,d)) ⊸ b ⊸ c
loop f b = let (c,d) = f (b,d) in c
EDIT
chi has provided a compelling argument that the above form of loop is impossible. The above in based on the instance
class Category a => Arrow a where
arr :: (b ⊸ c) ⊸ a b c
first :: a b c ⊸ a (b,d) (c,d)
second :: a b c ⊸ a (d,b) (d,c)
(***) :: a b c ⊸ a b' c' ⊸ a (b,b') (c,c')
(&&&) :: (Dupable b) => a b c ⊸ a b c' ⊸ a b (c,c')
class Arrow a => ArrowLoop a where
loop :: a (b,d) (c,d) ⊸ a b c
instance ArrowLoop (FUN 'One)
An alternative definition would be to redefine Arrow
class Category a => Arrow a where
arr :: (b -> c) ⊸ a b c
... as before ...
instance ArrowLoop (FUN 'Many) where
-- loop :: ((b,d) -> (c,d)) ⊸ b -> c
loop = let (c,d) = f (b,d) in c
This appears to suffer the same problem, which is a bit depressing.
The final possible definition for ArrowLoop
is
instance ArrowLoop (FUN 'One) where
-- loop :: ((b,d) ⊸ (c,d)) -> b ⊸ c
loop = let (c,d) = f (b,d) in c
which is just an instance of the ArrowLoop
from the non-linear Control.Arrow
for (FUN 'One)
. This is also problematic, because of the consumption of b
.
I don't think it is possible.
It would allow you to define this instance:
{-# LANGUAGE LinearTypes, FlexibleInstances, UndecidableInstances #-}
import qualified Prelude.Linear as L
loop :: ((b, d) %1 -> (c, d)) %1 -> b %1 -> c
loop = undefined
instance L.Semigroup a => L.Consumable a where
consume x = loop (\(y, z) -> (y, x L.<> z)) ()
(with Prelude.Linear
from linear-base
)
So, it basically allows you to consume linear arguments by only having a function that can combine two arguments of that type linearly. As far as I know, that is not something that you should be allowed to do.