我最近一直在尝试线性类型,并且一直想知道是否可以进行以下转换。如果没有线性类型,它绝对是无效的。
目的是降低高阶函数参数。这应该没问题,因为线性类型确保 HOF 只被调用一次,所以 a
的值正好是 1 个。存在。问题是如何转义 lambda 并观察 a
lower :: ((a %1-> b) %1-> r) %1-> b %1-> (r,a)
最佳答案
编辑:您不能安全地实现 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)
来保存这种情况。 .这样就不可能存储线性参数 a %1 -> b
在 r
.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)
我认为线性类型的主要目的只是为了获取额外的类型级信息,所以我认为没有任何安全的原语可以让你更干净地做到这一点(虽然我不知道所有的来龙去脉) .线性类型确实允许你实现一个安全的接口(interface),下面有不安全的操作。例如看多少次toLinear
用于this file from linear-base .也许上面的不安全位可以外包给较低级别的库。也许像 promises ,但随后是线性类型。
关于haskell - 使用线性类型降低高阶函数,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/69072523/