使用线性类型降低高阶函数

Question

我最近一直在尝试线性类型，并且一直在想是否可以进行以下转换。没有线性类型肯定是无效的。

目的是降低高阶函数自变量。这应该没问题，因为线性类型确保 HOF 仅被调用一次，因此 a 恰好存在 1 个值。问题是如何逃避 lambda 并观察 a

   lower :: ((a %1-> b) %1-> r) %1-> b %1-> (r,a)

Answer 1

编辑：您无法安全地实施 lower。正如 dfeuer 和 danidiaz 在评论中所说：如果 lower 的第一个参数是恒等函数怎么办？通过我在下面的旧答案中展示的实现，您可以这样写：

main :: IO ()
main = putStrLn (snd (lower (\x -> x) False))

这将在运行时产生错误：

Lin: Prelude.undefined
CallStack (from HasCallStack):
  error, called at libraries/base/GHC/Err.hs:74:14 in base:GHC.Err
  undefined, called at Lin.hs:25:19 in main:Main

所以线性类型没有提供足够的保证来安全地实现这个功能。

Edit2：您可以通过将签名稍微更改为：lower :: ((a %1 -> b) %1 -> Ur r) %1 -> b %1 -> (Ur r, a) 来挽救这种情况。这样就不可能在r.

中存储线性参数a %1 -> b

import Control.Exception (evaluate)

-- from Data.Unrestricted.Linear from linear-base
data Ur a where
  Ur :: a -> Ur a

lower :: ((a %1 -> b) %1 -> Ur r) %1 -> b %1 -> (Ur r, a)
lower = toLinear2 lower'

lower' :: ((a %1 -> b) %1 -> Ur r) -> b -> (Ur r, a)
lower' f b = unsafePerformIO $ do
  ref <- newIORef undefined
  r <- evaluate $ f (toLinear (\a -> unsafePerformIO $ b <$ writeIORef ref a))
  a <- readIORef ref
  pure (r, a)

旧答案

这可能不是您要找的答案，但如果您确定它是安全的，那么您可以稍微改变一下规则：

{-# LANGUAGE LinearTypes, GADTs #-}
import System.IO.Unsafe
import Data.IORef
import Unsafe.Coerce
import Control.Exception (evaluate)

-- 'coerce', 'toLinear' and 'toLinear2' are also found in Unsafe.Linear from linear-base

coerce :: forall a b. a %1-> b
coerce a =
  case unsafeEqualityProof @a @b of
    UnsafeRefl -> a
{-# INLINE coerce #-}

toLinear :: (a %p-> b) %1-> (a %1-> b)
toLinear = coerce

toLinear2 :: (a %p-> b %q-> c) %1-> (a %1-> b %1-> c)
toLinear2 = coerce

lower :: ((a %1 -> b) %1 -> r) %1 -> b %1 -> (r, a)
lower = toLinear2 lower'

lower' :: ((a %1 -> b) %1 -> r) -> b -> (r, a)
lower' f b = unsafePerformIO $ do
  ref <- newIORef undefined
  r <- evaluate $ f (toLinear (\a -> unsafePerformIO $ b <$ writeIORef ref a))
  a <- readIORef ref
  pure (r, a)

我认为线性类型的主要目的只是为了获得额外的类型级信息，所以我认为没有任何安全的原语可以让你更干净地做到这一点（虽然我不知道所有来龙去脉）。线性类型确实允许您实现一个安全的接口，下面是不安全的操作。例如，请参阅 this file from linear-base.

中使用了多少次 toLinear

也许上面的不安全位可以外包给下级库。也许类似于 promises，但随后是线性类型。

使用线性类型降低高阶函数

Lowering of higher order function with linear types

haskell

higher-order-functions

linear-types

旧答案