我最近一直在嘗試使用線性型別，并且一直在想下面的轉換是否可行。如果沒有線性型別，它肯定是不成立的。
目的是降低高階函式引數。
目的是為了降低高階函式的引數。這應該是可以的，因為線性型別確保HOF被精確呼叫一次，所以a的值正好存在。問題是如何擺脫lambda并觀察a
lower :: ((a %1-> b) %1-> r) %1-> b %1-> （r,a
uj5u.com熱心網友回復：
編輯：你不能安全地實作lower。正如dfeuer和danidiaz在評論中所說：如果lower的第一個引數是身份函式怎么辦？通過我在下面的舊答案中展示的實作，你可以寫道：
main :: IO ()
main = putStrLn (snd (lower (x -> x) False)
這將在運行時產生一個錯誤：
Lin: Prelude.undefined
CallStack（來自HasCallStack）。
error, called at libraries/base/GHC/Err.hs:74:14 in base:GHC.Err
未定義，在 Lin.hs:25:19 in main:Main 中被呼叫。
因此，線性型別沒有提供足夠的保證，使其安全地實作這個函式。
編輯2：你可以通過稍微改變簽名來挽救這種情況。lower :: ((a %1 -> b) %1 -> Ur r) %1 -> b %1 -> (Ur r, a)/code>。這樣，就不可能將線性引數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 <- 評估 $ f (toLinear (a -> unsafePerformIO $ b <$ writeIORef ref a))
a <- readIORef ref
pure (r, a)
舊答案
這可能不是你要找的答案，但是如果你確定它是安全的，那么你可以稍微彎曲一下規則：這可能不是你要找的答案，但是如果你確定它是安全的，那么你可以稍微彎曲一下規則：
import System.IO.unsafe
import Data.IORef
import Unsafe.Coerce
import Control.Exception (evaluate)
-- 'coerce'、'toLinear'和'toLinear2'也可以在線性基礎的Unsafe.Linear中找到。
coerce :: forall a b. a %1-> b
coerce a =
case unsafeEqualityProof @a @bof
UnsafeRefl -> a
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 <- 評估 $ f (toLinear (a -> unsafePerformIO $ b <$ writeIORef ref a))
a <- readIORef ref
pure (r, a)
我認為線性型別的主要目的只是為了獲得額外的型別級資訊，所以我不認為有任何安全的基元可以讓你更干凈地做到這一點（盡管我不知道所有的內涵和外延）。線性型別確實允許你在不安全的操作下實作一個安全的介面。例如，請看這個來自線性基礎的檔案中使用了多少次toLinear。
也許上面的不安全位可以外包給一個較低級別的庫。也許像promises這樣的東西，但是要用線性型別。
轉載請註明出處，本文鏈接：https://www.uj5u.com/qianduan/316928.html
標籤：