线性类型允许为递归函数提供绑定解决方案

Question

线性类型的当前实现（GHC 9.0.1）存在限制，即let和中的绑定不是线性的。

到目前为止，我已经能够使用用户指南中建议的显式函数来解决这个问题。然而，当试图实现函数时（出于好奇，来自ArrowLoop），我已经用完了变通方法。没有let或where绑定，如何引入递归？

loop :: ((b,d) ⊸ (c,d)) ⊸ b ⊸ c
loop f b = let (c,d) = f (b,d) in c

编辑

chi提供了一个令人信服的论点，即上述形式的循环是不可能的。以上在基于实例的基础上

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)

另一种定义是重新定义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

这似乎也遇到了同样的问题，有点令人沮丧。箭头循环的最终可能定义为

instance ArrowLoop (FUN 'One) where
    -- loop :: ((b,d) ⊸ (c,d)) -> b ⊸ c
    loop = let (c,d) = f (b,d) in c

这只是非线性控件中箭头循环的一个实例。箭头（有趣的一个）。这也是有问题的，因为使用了b。

Answer 1

我认为这是不可能的。

它将允许您定义此实例：

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

（带序曲.线性自线性基）

因此，它基本上允许您仅通过一个函数来使用线性参数，该函数可以线性地组合该类型的两个参数。据我所知，这不是你应该被允许做的事情。