haskell - 线性类型让递归函数的绑定(bind)解决方法

Question

LinearTypes 的当前实现 (GHC 9.0.1) let 和 where 绑定(bind)不是线性的。

到目前为止，我已经能够按照用户指南中的建议使用显式函数来解决这个问题。但是，在尝试实现功能时(出于好奇，来自 ArrowLoop)，我已经用尽了所有变通方法。如何在没有 let 或 where 绑定(bind)的情况下引入递归？

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

这次好像遇到了同样的问题，有点郁闷。ArrowLoop 的最终可能定义是

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

这只是 (FUN 'One) 的非线性 Control.Arrow 中 ArrowLoop 的一个实例。这也是有问题的，因为消耗了 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)) ()

(来自 linear-base 的 Prelude.Linear)

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