线性类型让递归函数的绑定解决方法

Question

LinearTypes 的当前实施 (GHC 9.0.1) 存在限制，即 let 和 where 绑定不是线性的。

到目前为止，我已经能够按照用户指南中的建议使用显式函数来解决这个问题。但是，在尝试实现功能时（出于好奇，来自 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

这个好像也是一样的问题，有点郁闷。 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)) ()

（Prelude.Linear 来自 linear-base）

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

线性类型让递归函数的绑定解决方法

Linear types let binding workaround for recursive function

haskell

linear-types