Linear types let binding workaround for recursive function

Question

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.

Answer 1

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.