packages feed

pure-borrow (empty) → 0.0.0.0

raw patch · 54 files changed

+7233/−0 lines, 54 filesdep +arraydep +basedep +bytestring

Dependencies added: array, base, bytestring, cassava, containers, deepseq, directory, doctest-parallel, falsify, file-embed, hybrid-vectors, linear-base, linear-generics, monoidal-containers, optparse-applicative, process, pure-borrow, random, stm, tasty, tasty-bench, tasty-expected-failure, tasty-hunit, template-haskell, temporary, text, transformers, unordered-containers, vector, vector-algorithms

Files

+ CHANGELOG.md view
@@ -0,0 +1,12 @@+# Revision history for pure-borrow++## 0.0.0.0 -- 2026-05-05++This is the first release on Hackage :tada:+Please refer to our paper for details.+Besides the parts covered by the paper, we are providing the following experimental features:++- Bulk borrows by `Borrows` heterogeneous list.+- `Reborrowable` type class for abstraction over reborrowable borrow-like objects.+- Looping structure.+- Record splitting.
+ LICENSE view
@@ -0,0 +1,29 @@+Copyright (c) 2025-2026, Yusuke Matsushita and Hiromi Ishii+++Redistribution and use in source and binary forms, with or without+modification, are permitted provided that the following conditions are met:++    * Redistributions of source code must retain the above copyright+      notice, this list of conditions and the following disclaimer.++    * Redistributions in binary form must reproduce the above+      copyright notice, this list of conditions and the following+      disclaimer in the documentation and/or other materials provided+      with the distribution.++    * Neither the name of the copyright holder nor the names of its+      contributors may be used to endorse or promote products derived+      from this software without specific prior written permission.++THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS+"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT+LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR+A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT+HOLDER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,+SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT+LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,+DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY+THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT+(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE+OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+ README.md view
@@ -0,0 +1,22 @@+# pure-borrow: Pure realization of Rust-style borrows in Linear Haskell++This is `pure-borrow`, a library that realizes Rust-style borrows in Linear+Haskell in a pure manner.+See the haddock or publication below for the more information.++## Supported GHC Versions++We support GHC 9.10.2+, but we recommend GHC 9.12.4+, due to subtle compiler bug in older GHC.++## Known Issues++Due to the bug of linear types in GHC <9.12.3, some program segfaults when evaluated in *interpreter* with older GHCs (see https://gitlab.haskell.org/ghc/ghc/-/issues/26565#note_645783).+Compiled programs just work as expected with GHC 9.10.2+, so this issue will only affect you are trying to use GHCi or Eval Plugin of Haskell Language Server.+If you want to use interpreters, +use GHC 9.12.3+.++## Publication(s)++- Y. Matsushita and H. Ishii, *Pure Borrow: Linear Haskell Meets Rust-Style Borrowing*, 2026. +  To appear in: PLDI 2026. Boulder, Colorado, USA, June 15-19. DOI: [10.1145/3808259](https://doi.org/10.1145/3808259). Extended Version: [arxiv:2604.15290](https://arxiv.org/abs/2604.15290).+- Y. Matsushita and H. Ishii, *Artifact for PLDI 2026 "Pure Borrow: Linear Haskell Meets Rust-Style Borrowing"*, 2026. Zenodo: https://zenodo.org/records/19622061.
+ app/artifact-runner.hs view
@@ -0,0 +1,238 @@+{-# LANGUAGE GHC2021 #-}+{-# LANGUAGE BlockArguments #-}+{-# LANGUAGE DerivingStrategies #-}+{-# LANGUAGE DerivingVia #-}+{-# LANGUAGE DuplicateRecordFields #-}+{-# LANGUAGE LambdaCase #-}+{-# LANGUAGE OverloadedRecordDot #-}+{-# LANGUAGE OverloadedStrings #-}+{-# LANGUAGE RecordWildCards #-}+{-# LANGUAGE TemplateHaskell #-}+{-# LANGUAGE NoFieldSelectors #-}+{-# OPTIONS_GHC -Wno-incomplete-uni-patterns #-}++module Main (main) where++import Control.Applicative+import Control.Concurrent (getNumCapabilities, setNumCapabilities)+import Control.Exception (throwIO, try)+import Control.Monad (forM_)+import Control.Monad.Trans.Writer.CPS (execWriter, tell)+import Data.ByteString qualified as BS+import Data.ByteString.Builder qualified as BB+import Data.ByteString.Lazy qualified as LBS+import Data.Csv (FromNamedRecord (..), decodeByName, (.:))+import Data.FileEmbed+import Data.Foldable (fold)+import Data.Foldable1 (fold1)+import Data.Functor+import Data.IntMap.Monoidal.Strict (MonoidalIntMap)+import Data.IntMap.Monoidal.Strict qualified as MIM+import Data.IntSet qualified as IS+import Data.List qualified as List+import Data.List.NonEmpty (NonEmpty (..))+import Data.Map.Monoidal.Strict (MonoidalMap)+import Data.Map.Monoidal.Strict qualified as MonoidalMap+import Data.Monoid (First (..))+import Data.Semigroup qualified as Semi+import Data.Set qualified as Set+import Data.Text qualified as T+import Data.Text.Encoding qualified as TE+import GHC.Generics+import Options.Applicative qualified as Opts+import PureBorrow.Demo.QSort qualified as QS+import PureBorrow.Internal.Bench.QSort (BenchOpts)+import PureBorrow.Internal.Bench.QSort qualified as Bench+import System.Directory (canonicalizePath, findExecutable)+import System.Environment (withArgs)+import System.Exit (ExitCode)+import System.IO (hClose, hFlush)+import System.IO.Temp (withSystemTempFile)+import System.Process (readProcess)+import Text.Read (readEither)++data Cmd = Bench BenchOpts | QuickBench | QSortDemo QS.CLIOpts+  deriving (Show, Eq, Ord, Generic)++optionsP :: Int -> Opts.ParserInfo Cmd+optionsP numCapa =+  Opts.info (p <**> Opts.helper) $+    Opts.fullDesc+      <> Opts.progDesc "Artifact runner for qsort benchmarks and demos"+  where+    p = cmds <|> Bench <$> Bench.rawOptsP+    cmds =+      Opts.hsubparser $+        fold1 $+          Opts.command "bench" (Bench <$> Bench.optionsP)+            :| [ Opts.command "demo" $ QSortDemo <$> QS.optionsP numCapa+               , Opts.command "quick" $+                   Opts.info (pure QuickBench) $+                     Opts.progDesc $+                       "Run quick benchmarks with numcpu = 4 for sizes 0 and " <> show Bench.kMAX_SIZE+               ]++main :: IO ()+main = do+  numCap <- getNumCapabilities+  Opts.customExecParser (Opts.prefs Opts.subparserInline) (optionsP numCap) >>= \case+    Bench benchOpts -> runBench benchOpts+    QuickBench -> runBench Bench.BenchOpts {numThreads = 4, sampleSize = 2}+    QSortDemo cliOpts -> QS.defaultMainWith cliOpts++runBench :: BenchOpts -> IO ()+runBench benchOpts = do+  let rawDest = "qsort-raw.csv"+  void $ try @ExitCode $ withArgs ["--csv", rawDest, "-j1", "--time-mode=wall", "-t", "10s"] do+    setNumCapabilities benchOpts.numThreads+    Bench.defaultMainWith benchOpts++  putStrLn "Processing results..."+  (_, rawRows) <- either (throwIO . userError) pure . decodeByName =<< LBS.readFile rawDest+  let sd = foldMap fromRawRow rawRows+      builder = buildOutput sd+  csvDest <- canonicalizePath "qsort.csv"+  BB.writeFile csvDest builder++  mgp <- findExecutable "gnuplot"+  forM_ mgp \gnuplot -> withSystemTempFile "plot.gp" \tmp h -> do+    putStrLn $ "Gnuplot found: " <> gnuplot+    pngDest <- canonicalizePath "qsort.png"+    BS.hPutStr h gnuplotScript+    hFlush h+    hClose h+    !_ <- readProcess gnuplot ["-e", "input='" <> csvDest <> "'; output='" <> pngDest <> "'", tmp] ""+    putStrLn $ "Plot generated: " <> pngDest++gnuplotScript :: BS.ByteString+gnuplotScript =+  $(embedFile "scripts/genplot.gnuplot")++buildOutput :: Statistics -> BB.Builder+buildOutput sd = execWriter do+  let (hdrs, targets) = toHeaders sd++  putLine $+    fold $+      List.intersperse "," $+        map (BB.byteString . TE.encodeUtf8) hdrs+  forM_ (MIM.toAscList sd) \(size, ps) -> do+    let row =+          BB.intDec size+            : concatMap+              ( \t ->+                  maybe (replicate 5 mempty) (\p -> map BB.doubleDec [p.mean, p.stddev, p.alloc, p.copied, p.peak]) $+                    lookupStat t ps+              )+              targets+    putLine $ fold $ List.intersperse "," row+  where+    crlf = tell "\r\n"+    putLine = (>> crlf) . tell++data RawRow = RawRow+  { size :: !Int+  , name :: !T.Text+  , mean :: !Int+  , stddev :: !Int+  , alloc :: !Int+  , copied :: !Int+  , peak :: !Int+  }+  deriving (Show, Eq, Ord, Generic)++instance FromNamedRecord RawRow where+  parseNamedRecord r = do+    fullName <- r .: "Name"+    let ~(sz : name : _) = drop 2 $ T.splitOn "." fullName+    size <- either fail pure $ readEither $ T.unpack sz+    mean <- r .: "Mean (ps)"+    stddev <- r .: "2*Stdev (ps)" <&> (`quot` 2)+    alloc <- r .: "Allocated"+    copied <- r .: "Copied"+    peak <- r .: "Peak Memory"+    pure RawRow {..}++data Performance = Performance+  { mean :: !Double+  , stddev :: !Double+  , alloc :: !Double+  , copied :: !Double+  , peak :: !Double+  }+  deriving (Show, Eq, Ord, Generic)+  deriving (Semigroup) via Semi.First Performance++toPerformance :: RawRow -> Performance+toPerformance RawRow {..} =+  Performance+    { mean = fromIntegral mean * 1e-9+    , stddev = fromIntegral stddev * 1e-9+    , alloc = fromIntegral alloc * 1e-6+    , copied = fromIntegral copied * 1e-6+    , peak = fromIntegral peak * 1e-6+    }++data PerformanceSet = PerformanceSet+  { intro :: !(First Performance)+  , sequential :: !(First Performance)+  , parallel :: !(MonoidalIntMap Performance)+  , worksteal :: !(MonoidalIntMap Performance)+  , others :: !(MonoidalMap T.Text Performance)+  }+  deriving (Show, Eq, Ord, Generic)+  deriving (Semigroup, Monoid) via Generically PerformanceSet++type Statistics = MonoidalIntMap PerformanceSet++data Target = Intro | Sequential | Parallel Int | Worksteal Int | Other T.Text+  deriving (Show, Eq, Ord, Generic)++lookupStat :: Target -> PerformanceSet -> Maybe Performance+lookupStat t ps =+  case t of+    Intro -> getFirst ps.intro+    Sequential -> getFirst ps.sequential+    Parallel n -> MIM.lookup n ps.parallel+    Worksteal n -> MIM.lookup n ps.worksteal+    Other name -> MonoidalMap.lookup name ps.others++toHeaders :: Statistics -> ([T.Text], [Target])+toHeaders stats =+  (headers, targets)+  where+    headers = "size" : [cat <> metric | cat <- categories, metric <- metrics]+    targets = Intro : Sequential : [Parallel n | n <- IS.toList parallels] ++ [Worksteal n | n <- IS.toList worksteals] ++ [Other name | name <- Set.toList miscs]+    (parallels, worksteals, miscs) =+      foldMap+        ( \ps ->+            ( MIM.keysSet ps.parallel+            , MIM.keysSet ps.worksteal+            , MonoidalMap.keysSet ps.others+            )+        )+        stats+    categories =+      "intro"+        : "sequential"+        : [T.pack $ "parallel" <> show n | n <- IS.toList parallels]+        ++ [T.pack $ "workSteal" <> show n | n <- IS.toList worksteals]+        ++ [name | name <- Set.toList miscs]++    metrics = ["Mean", "Stddev", "Alloc", "Copied", "Peak"]++fromRawRow :: RawRow -> Statistics+fromRawRow r@RawRow {..} = MIM.singleton size $+  case name of+    "intro" -> mempty {intro = First (Just $ toPerformance r)}+    "sequential" -> mempty {sequential = First (Just $ perf)}+    inp+      | Just rest <- T.stripPrefix "parallel (budget =" inp+      , [(n, _)] <- reads (T.unpack rest) ->+          mempty {parallel = MIM.singleton n perf}+      | Just rest <- T.stripPrefix "worksteal (workers =" inp+      , [(n, _)] <- reads (T.unpack rest) ->+          mempty {worksteal = MIM.singleton n perf}+    _ -> mempty {others = MonoidalMap.singleton name perf}+  where+    perf = toPerformance r
+ app/convert-qsort-bench-csv.hs view
@@ -0,0 +1,179 @@+{-# LANGUAGE BlockArguments #-}+{-# LANGUAGE DeriveAnyClass #-}+{-# LANGUAGE DeriveGeneric #-}+{-# LANGUAGE DerivingStrategies #-}+{-# LANGUAGE DerivingVia #-}+{-# LANGUAGE OverloadedStrings #-}+{-# LANGUAGE RecordWildCards #-}+{-# LANGUAGE TypeApplications #-}+{-# OPTIONS_GHC -Wno-incomplete-uni-patterns #-}+{-# OPTIONS_GHC -Wno-orphans #-}++module Main (main) where++import Control.Applicative ((<**>))+import Control.Exception (throwIO)+import Data.ByteString.Char8 qualified as BS8+import Data.ByteString.Lazy qualified as LBS+import Data.Coerce (coerce)+import Data.Csv+import Data.Functor+import Data.HashMap.Strict qualified as HM+import Data.IntMap.Monoidal.Strict (MonoidalIntMap)+import Data.IntMap.Monoidal.Strict qualified as MIM+import Data.Maybe (fromMaybe)+import Data.Monoid (Sum (..))+import Data.Text qualified as T+import Data.Vector qualified as V+import GHC.Generics+import Options.Applicative qualified as Opts+import Text.Read (readEither)++data CLIOptions = CLIOptions+  { inputFile :: FilePath+  , outputFile :: FilePath+  }+  deriving (Show, Eq, Ord)++cliOptionsP :: Opts.ParserInfo CLIOptions+cliOptionsP =+  Opts.info (p <**> Opts.helper) $+    Opts.fullDesc+      <> Opts.progDesc "Convert a CSV file for qsort benchmark"+  where+    p :: Opts.Parser CLIOptions+    p =+      CLIOptions+        <$> Opts.strOption+          ( Opts.long "input"+              <> Opts.short 'i'+              <> Opts.metavar "INPUT_FILE"+              <> Opts.help "Input CSV file"+          )+        <*> Opts.strOption+          ( Opts.long "output"+              <> Opts.short 'o'+              <> Opts.metavar "OUTPUT_FILE"+              <> Opts.help "Output CSV file"+          )++data RawRow = RawRow+  { size :: !Int+  , name :: !T.Text+  , mean :: !Int+  , stddev :: !Int+  , alloc :: !Int+  , copied :: !Int+  , peak :: !Int+  }+  deriving (Show, Eq, Ord, Generic)++instance FromNamedRecord RawRow where+  parseNamedRecord r = do+    fullName <- r .: "Name"+    let ~(sz : name : _) = drop 2 $ T.splitOn "." fullName+    size <- either fail pure $ readEither $ T.unpack sz+    mean <- r .: "Mean (ps)"+    stddev <- r .: "2*Stdev (ps)" <&> (`quot` 2)+    alloc <- r .: "Allocated"+    copied <- r .: "Copied"+    peak <- r .: "Peak Memory"+    pure RawRow {..}++type SizeDataMap = MonoidalIntMap SizeData++fromRawRow :: RawRow -> SizeDataMap+fromRawRow RawRow {..} = fromMaybe mempty do+  dat <- case name of+    "intro" -> pure mempty {introMean = Sum (fromIntegral mean * 1e-9), introStddev = Sum (fromIntegral stddev * 1e-9), introAlloc = Sum (fromIntegral alloc * 1e-6), introCopied = Sum (fromIntegral copied * 1e-6), introPeak = Sum (fromIntegral peak * 1e-6)}+    "sequential" -> pure mempty {sequentialMean = Sum (fromIntegral mean * 1e-9), sequentialStddev = Sum (fromIntegral stddev * 1e-9), sequentialAlloc = Sum (fromIntegral alloc * 1e-6), sequentialCopied = Sum (fromIntegral copied * 1e-6), sequentialPeak = Sum (fromIntegral peak * 1e-6)}+    "parallel (budget = 4)" -> pure mempty {parallel4Mean = Sum (fromIntegral mean * 1e-9), parallel4Stddev = Sum (fromIntegral stddev * 1e-9), parallel4Alloc = Sum (fromIntegral alloc * 1e-6), parallel4Copied = Sum (fromIntegral copied * 1e-6), parallel4Peak = Sum (fromIntegral peak * 1e-6)}+    "parallel (budget = 8)" -> pure mempty {parallel8Mean = Sum (fromIntegral mean * 1e-9), parallel8Stddev = Sum (fromIntegral stddev * 1e-9), parallel8Alloc = Sum (fromIntegral alloc * 1e-6), parallel8Copied = Sum (fromIntegral copied * 1e-6), parallel8Peak = Sum (fromIntegral peak * 1e-6)}+    "parallel (budget = 16)" -> pure mempty {parallel16Mean = Sum (fromIntegral mean * 1e-9), parallel16Stddev = Sum (fromIntegral stddev * 1e-9), parallel16Alloc = Sum (fromIntegral alloc * 1e-6), parallel16Copied = Sum (fromIntegral copied * 1e-6), parallel16Peak = Sum (fromIntegral peak * 1e-6)}+    "parallel (budget = 32)" -> pure mempty {parallel32Mean = Sum (fromIntegral mean * 1e-9), parallel32Stddev = Sum (fromIntegral stddev * 1e-9), parallel32Alloc = Sum (fromIntegral alloc * 1e-6), parallel32Copied = Sum (fromIntegral copied * 1e-6), parallel32Peak = Sum (fromIntegral peak * 1e-6)}+    "worksteal (workers = 2)" -> pure mempty {workSteal2Mean = Sum (fromIntegral mean * 1e-9), workSteal2Stddev = Sum (fromIntegral stddev * 1e-9), workSteal2Alloc = Sum (fromIntegral alloc * 1e-6), workSteal2Copied = Sum (fromIntegral copied * 1e-6), workSteal2Peak = Sum (fromIntegral peak * 1e-6)}+    "worksteal (workers = 4)" -> pure mempty {workSteal4Mean = Sum (fromIntegral mean * 1e-9), workSteal4Stddev = Sum (fromIntegral stddev * 1e-9), workSteal4Alloc = Sum (fromIntegral alloc * 1e-6), workSteal4Copied = Sum (fromIntegral copied * 1e-6), workSteal4Peak = Sum (fromIntegral peak * 1e-6)}+    "worksteal (workers = 6)" -> pure mempty {workSteal6Mean = Sum (fromIntegral mean * 1e-9), workSteal6Stddev = Sum (fromIntegral stddev * 1e-9), workSteal6Alloc = Sum (fromIntegral alloc * 1e-6), workSteal6Copied = Sum (fromIntegral copied * 1e-6), workSteal6Peak = Sum (fromIntegral peak * 1e-6)}+    "worksteal (workers = 8)" -> pure mempty {workSteal8Mean = Sum (fromIntegral mean * 1e-9), workSteal8Stddev = Sum (fromIntegral stddev * 1e-9), workSteal8Alloc = Sum (fromIntegral alloc * 1e-6), workSteal8Copied = Sum (fromIntegral copied * 1e-6), workSteal8Peak = Sum (fromIntegral peak * 1e-6)}+    "worksteal (workers = 10)" -> pure mempty {workSteal10Mean = Sum (fromIntegral mean * 1e-9), workSteal10Stddev = Sum (fromIntegral stddev * 1e-9), workSteal10Alloc = Sum (fromIntegral alloc * 1e-6), workSteal10Copied = Sum (fromIntegral copied * 1e-6), workSteal10Peak = Sum (fromIntegral peak * 1e-6)}+    _ -> Nothing+  pure (MIM.singleton size dat)++data SizeData = SizeData+  { introMean :: !(Sum Double)+  , introStddev :: !(Sum Double)+  , introAlloc :: !(Sum Double)+  , introCopied :: !(Sum Double)+  , introPeak :: !(Sum Double)+  , sequentialMean :: !(Sum Double)+  , sequentialStddev :: !(Sum Double)+  , sequentialAlloc :: !(Sum Double)+  , sequentialCopied :: !(Sum Double)+  , sequentialPeak :: !(Sum Double)+  , parallel4Mean :: !(Sum Double)+  , parallel4Stddev :: !(Sum Double)+  , parallel4Alloc :: !(Sum Double)+  , parallel4Copied :: !(Sum Double)+  , parallel4Peak :: !(Sum Double)+  , parallel8Mean :: !(Sum Double)+  , parallel8Stddev :: !(Sum Double)+  , parallel8Alloc :: !(Sum Double)+  , parallel8Copied :: !(Sum Double)+  , parallel8Peak :: !(Sum Double)+  , parallel16Mean :: !(Sum Double)+  , parallel16Stddev :: !(Sum Double)+  , parallel16Alloc :: !(Sum Double)+  , parallel16Copied :: !(Sum Double)+  , parallel16Peak :: !(Sum Double)+  , parallel32Mean :: !(Sum Double)+  , parallel32Stddev :: !(Sum Double)+  , parallel32Alloc :: !(Sum Double)+  , parallel32Copied :: !(Sum Double)+  , parallel32Peak :: !(Sum Double)+  , workSteal2Mean :: !(Sum Double)+  , workSteal2Stddev :: !(Sum Double)+  , workSteal2Alloc :: !(Sum Double)+  , workSteal2Copied :: !(Sum Double)+  , workSteal2Peak :: !(Sum Double)+  , workSteal4Mean :: !(Sum Double)+  , workSteal4Stddev :: !(Sum Double)+  , workSteal4Alloc :: !(Sum Double)+  , workSteal4Copied :: !(Sum Double)+  , workSteal4Peak :: !(Sum Double)+  , workSteal6Mean :: !(Sum Double)+  , workSteal6Stddev :: !(Sum Double)+  , workSteal6Alloc :: !(Sum Double)+  , workSteal6Copied :: !(Sum Double)+  , workSteal6Peak :: !(Sum Double)+  , workSteal8Mean :: !(Sum Double)+  , workSteal8Stddev :: !(Sum Double)+  , workSteal8Alloc :: !(Sum Double)+  , workSteal8Copied :: !(Sum Double)+  , workSteal8Peak :: !(Sum Double)+  , workSteal10Mean :: !(Sum Double)+  , workSteal10Stddev :: !(Sum Double)+  , workSteal10Alloc :: !(Sum Double)+  , workSteal10Copied :: !(Sum Double)+  , workSteal10Peak :: !(Sum Double)+  }+  deriving (Show, Eq, Ord, Generic)+  deriving anyclass (ToNamedRecord, DefaultOrdered)+  deriving (Semigroup, Monoid) via Generically SizeData++newtype ODP = ODP (Int, SizeData)++instance DefaultOrdered ODP where+  headerOrder _ = "size" `V.cons` headerOrder (undefined :: SizeData)++instance ToNamedRecord ODP where+  toNamedRecord (ODP (sz, r)) = HM.insert "size" (BS8.pack $ show sz) $ toNamedRecord r++instance (ToField a) => ToField (Sum a) where+  toField (Sum x) = toField x++main :: IO ()+main = do+  CLIOptions {..} <- Opts.execParser cliOptionsP+  (_, rawRows) <- either (throwIO . userError) pure . decodeByName =<< LBS.readFile inputFile+  let sd = MIM.toList $ foldMap fromRawRow rawRows+  LBS.writeFile outputFile $ encodeDefaultOrderedByName $ coerce @_ @[ODP] sd
+ app/qsort.hs view
@@ -0,0 +1,17 @@+{-# LANGUAGE ApplicativeDo #-}+{-# LANGUAGE BangPatterns #-}+{-# LANGUAGE BlockArguments #-}+{-# LANGUAGE DeriveGeneric #-}+{-# LANGUAGE LambdaCase #-}+{-# LANGUAGE PartialTypeSignatures #-}+{-# LANGUAGE QualifiedDo #-}+{-# LANGUAGE RecordWildCards #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# OPTIONS_GHC -Wno-name-shadowing #-}++module Main (main) where++import PureBorrow.Demo.QSort (defaultMain)++main :: IO ()+main = defaultMain
+ bench/qsort.hs view
@@ -0,0 +1,11 @@+{-# LANGUAGE BlockArguments #-}+{-# LANGUAGE QualifiedDo #-}+{-# LANGUAGE TypeApplications #-}+{-# OPTIONS_GHC -Wno-name-shadowing #-}++module Main (main) where++import PureBorrow.Internal.Bench.QSort (defaultMain)++main :: IO ()+main = defaultMain
+ dockerfiles/artifact/Dockerfile view
@@ -0,0 +1,44 @@+FROM debian:bookworm AS build++RUN apt-get update && apt-get install -y build-essential curl libffi-dev libffi8ubuntu1 libgmp-dev libgmp10 libncurses-dev gnupg2 git++# install ghcup+RUN echo ${ARCH}+RUN curl --proto '=https' --tlsv1.2 -sSf https://get-ghcup.haskell.org | BOOTSTRAP_HASKELL_NONINTERACTIVE=1 BOOTSTRAP_HASKELL_MINIMAL=1 sh+RUN cp ~/.ghcup/bin/ghcup /usr/local/bin/ghcup++ARG GHC=9.10.3+RUN ghcup install ghc   --isolate /usr/local --force ${GHC}+ARG CABAL=3.14.2.0+RUN ghcup install cabal --isolate /usr/local/bin --force ${CABAL}++RUN mkdir -p /workspace+ARG PURE_BORROW_COMMIT=e5b027fb84663d2fc2b92956bbc32a09dfeda272+RUN git clone https://github.com/SoftwareFoundationGroupAtKyotoU/pure-borrow.git /workspace/pure-borrow && \+  cd /workspace/pure-borrow && \+  git fetch --all && \+  git checkout ${PURE_BORROW_COMMIT}++WORKDIR /workspace/pure-borrow+ENV PATH="/usr/local/bin:${PATH}"+ENV LANG=C.UTF-8++ARG CABAL_INDEX_STATE=2026-02-16T11:32:42Z+RUN cabal update --index-state=${CABAL_INDEX_STATE}+ARG NUM_CPUS=8+RUN cabal configure --enable-tests --enable-benchmarks --semaphore -j${NUM_CPUS} -fartifact+RUN cabal build all --only-dependencies+RUN cabal build all+RUN mkdir -p /opt/pure-borrow+RUN cp "$(cabal list-bin artifact-runner)" /opt/pure-borrow+RUN apt-get update && apt-get install -y gnuplot++FROM debian:bookworm-slim++ENV PATH="/opt/pure-borrow:${PATH}"+RUN mkdir -p /workspace+WORKDIR /workspace+COPY --from=build /opt/pure-borrow /opt/pure-borrow+RUN apt-get update && apt-get install -y gnuplot++ENTRYPOINT ["/opt/pure-borrow/artifact-runner"]
+ doctests/doctests.hs view
@@ -0,0 +1,9 @@+{-# LANGUAGE CPP #-}++module Main (main) where++import System.Environment (getArgs)+import Test.DocTest (mainFromCabal)++main :: IO ()+main = mainFromCabal "pure-borrow" =<< getArgs
+ internal-src/qsort-bench-suites/PureBorrow/Internal/Bench/QSort.hs view
@@ -0,0 +1,169 @@+{-# LANGUAGE BlockArguments #-}+{-# LANGUAGE QualifiedDo #-}+{-# LANGUAGE RecordWildCards #-}+{-# LANGUAGE TypeApplications #-}+{-# OPTIONS_GHC -Wno-name-shadowing #-}++module PureBorrow.Internal.Bench.QSort (+  defaultMain,+  defaultMainWith,+  optionsP,+  rawOptsP,+  BenchOpts (..),+  benches,+  kMAX_SIZE,+) where++import Control.Applicative+import Control.Concurrent (getNumCapabilities)+import Control.Concurrent.DivideConquer.Linear (qsortDC)+import Control.Functor.Linear qualified as Control+import Control.Monad.Borrow.Pure.BO+import Control.Syntax.DataFlow qualified as DataFlow+import Data.Proxy (Proxy (..))+import Data.Vector qualified as V+import Data.Vector.Algorithms.Intro qualified as AI+import Data.Vector.Mutable.Linear.Borrow qualified as VL+import Options.Applicative qualified as Opts+import Prelude.Linear (dup, unur)+import Prelude.Linear qualified as PL+import System.Random.Stateful+import Test.Tasty (askOption, defaultMainWithIngredients)+import Test.Tasty.Bench hiding (defaultMain)+import Test.Tasty.Bench qualified as Bench+import Test.Tasty.Ingredients.Basic (includingOptions)+import Test.Tasty.Options+import Text.Read (readMaybe)+import Prelude as P++data Mode = Parallel Word | Worksteal Int | Sequential | IntroSort+  deriving (Show, Eq, Ord)++data BenchOpts = BenchOpts {numThreads :: !Int, sampleSize :: !Int}+  deriving (Show, Eq, Ord)++optionsP :: Opts.ParserInfo BenchOpts+optionsP =+  Opts.info (p <**> Opts.helper) $+    Opts.fullDesc+      <> Opts.progDesc "Options for qsort benchmark"+  where+    p :: Opts.Parser BenchOpts+    p =+      BenchOpts+        <$> Opts.option+          Opts.auto+          ( Opts.long "threads"+              <> Opts.short 'N'+              <> Opts.metavar "NUM_THREADS"+              <> Opts.help "Number of threads to use for parallel benchmarks"+          )+        <*> Opts.option+          Opts.auto+          ( Opts.long "size"+              <> Opts.short 's'+              <> Opts.metavar "SAMPLE_SIZE"+              <> Opts.help "Number of samples to take (must divide 32768)"+          )++rawOptsP :: Opts.Parser BenchOpts+rawOptsP =+  BenchOpts+    <$> Opts.option+      Opts.auto+      ( Opts.long "threads"+          <> Opts.short 'N'+          <> Opts.value 10+          <> Opts.metavar "NUM_THREADS"+          <> Opts.help "Number of threads to use for parallel benchmarks"+      )+    <*> Opts.option+      Opts.auto+      ( Opts.long "size"+          <> Opts.short 's'+          <> Opts.metavar "SAMPLE_SIZE"+          <> Opts.value 32+          <> Opts.help "Number of samples to take (must divide 32768)"+      )++qsortWith :: Mode -> V.Vector Int -> V.Vector Int+qsortWith IntroSort v = V.modify AI.sort v+qsortWith (Parallel budget) v =+  unur PL.$ linearly \lin ->+    DataFlow.do+      (lin, l2) <- dup lin+      runBO lin Control.do+        (v, lend) <- borrowM (VL.fromVector v l2)+        VL.qsort budget v+        Control.pure PL.$ VL.toVector Control.<$> reclaim' lend+qsortWith Sequential v =+  unur PL.$ linearly \lin ->+    DataFlow.do+      (lin, l2) <- dup lin+      runBO lin Control.do+        (v, lend) <- borrowM (VL.fromVector v l2)+        VL.qsort 0 v+        pureAfter (VL.toVector PL.$ reclaim lend)+qsortWith (Worksteal p) v =+  unur PL.$ linearly \lin ->+    DataFlow.do+      (lin, l2) <- dup lin+      runBO lin Control.do+        (v, lend) <- borrowM (VL.fromVector v l2)+        Control.void PL.$ qsortDC p 128 v+        pureAfter (VL.toVector PL.$ reclaim lend)++data SampleSize = SampleSize Int+  deriving (Show, Eq, Ord)++instance IsOption SampleSize where+  defaultValue = SampleSize 32+  parseValue s =+    case readMaybe s of+      Just n | kMAX_SIZE `rem` n == 0 -> Just (SampleSize n)+      _ -> Nothing+  optionName = return "size"+  optionHelp = return "Step size to take a sample (must divide 32768)"++defaultMain :: IO ()+defaultMain = do+  numThreads <- getNumCapabilities+  let customOpts = [Option (Proxy :: Proxy SampleSize)]+      ingredients = includingOptions customOpts : benchIngredients+  defaultMainWithIngredients ingredients $ askOption \(SampleSize sampleSize) ->+    bgroup "All" $ benches BenchOpts {..}++defaultMainWith :: BenchOpts -> IO ()+defaultMainWith opts = do+  Bench.defaultMain $ benches opts++benches :: BenchOpts -> [Benchmark]+benches BenchOpts {..} =+  [ bgroup+      "qsort"+      [ env+          ( pure $ runStateGen_ (mkStdGen 42) \g -> do+              V.replicateM size (uniformM g)+          )+          \vec ->+            bgroup+              (show size)+              ( [ bench "intro" $ nf (qsortWith IntroSort) vec+                , bench "sequential" $ nf (qsortWith Sequential) vec+                ]+                  ++ [ bench ("parallel (budget = " <> show n <> ")") $+                         nf (qsortWith $ Parallel n) vec+                     | n <- [4, 8, 16, 32]+                     ]+                  ++ [ bench ("worksteal (workers = " <> show n <> ")") $+                         nf (qsortWith $ Worksteal n) vec+                     | n <- [2, 4 .. numThreads]+                     ]+              )+      | i <- [0 .. sampleSize]+      , let size = i * kMAX_SIZE `quot` sampleSize+      ]+  ]++kMAX_SIZE :: Int+kMAX_SIZE = 32 * 1024
+ internal-src/qsort-demo-impl/PureBorrow/Demo/QSort.hs view
@@ -0,0 +1,111 @@+{-# LANGUAGE ApplicativeDo #-}+{-# LANGUAGE BangPatterns #-}+{-# LANGUAGE BlockArguments #-}+{-# LANGUAGE DeriveGeneric #-}+{-# LANGUAGE LambdaCase #-}+{-# LANGUAGE PartialTypeSignatures #-}+{-# LANGUAGE QualifiedDo #-}+{-# LANGUAGE RecordWildCards #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TypeApplications #-}+{-# OPTIONS_GHC -Wno-name-shadowing #-}++module PureBorrow.Demo.QSort (+  defaultMain,+  defaultMainWith,+  CLIOpts (..),+  optionsP,+) where++import Control.Applicative ((<**>), (<|>))+import Control.Concurrent (getNumCapabilities)+import Control.Concurrent.DivideConquer.Linear (qsortDC)+import Control.DeepSeq (force)+import Control.Exception (evaluate)+import Control.Functor.Linear qualified as Control+import Control.Monad.Borrow.Pure.BO+import Control.Syntax.DataFlow qualified as DataFlow+import Data.Functor (void)+import Data.Vector qualified as V+import Data.Vector.Algorithms.Intro qualified as AI+import Data.Vector.Mutable.Linear.Borrow qualified as VL+import GHC.Generics (Generic)+import Options.Applicative qualified as Opts+import Prelude.Linear hiding (Eq, Ord, Semigroup (..), ($), ($!))+import Prelude.Linear qualified as PL hiding (($!))+import System.Mem (performGC)+import System.Random+import System.Random.Stateful (runStateGen_, uniformM)++data Mode = Parallel Word | Worksteal Int Int | Sequential | IntroSort+  deriving (Show, Eq, Ord, Generic)++data CLIOpts = CLIOpts {mode :: Mode, size :: Int, seed :: Maybe Int}+  deriving (Show, Eq, Ord, Generic)++optionsP :: Int -> Opts.ParserInfo CLIOpts+optionsP numCap = Opts.info (p <**> Opts.helper) $ Opts.progDesc "Parallel quicksort with linear borrows"+  where+    p = do+      mode <-+        Parallel <$> Opts.option Opts.auto (Opts.long "parallel" <> Opts.short 'p' <> Opts.help "Use parallel quicksort with specified capacity (default: 8)")+          <|> Opts.flag' Sequential (Opts.long "sequential" <> Opts.short 'S' <> Opts.help "Use sequential quicksort")+          <|> Opts.flag' (Worksteal numCap 512) (Opts.long "worksteal" <> Opts.short 'w' <> Opts.help "Use work-stealing quicksort")+          <|> Opts.flag (Parallel 8) IntroSort (Opts.long "intro" <> Opts.short 'i' <> Opts.help "Use intro sort")+      size <-+        Opts.option+          Opts.auto+          ( Opts.long "size"+              <> Opts.short 'n'+              <> Opts.value 256+              <> Opts.showDefault+              <> Opts.help "Size of the vector to sort"+          )+      seed <- Opts.optional $ Opts.option Opts.auto (Opts.long "seed" <> Opts.short 's' <> Opts.help "Random seed for vector generation (default: random)")+      pure CLIOpts {..}++qsortWith :: Mode -> StdGen -> V.Vector Int -> V.Vector Int+qsortWith IntroSort _ v = V.modify AI.sort v+qsortWith (Parallel bud) _ v =+  unur PL.$ linearly \lin ->+    DataFlow.do+      (lin, l2) <- dup lin+      runBO lin Control.do+        (v, lend) <- borrowM (VL.fromVector v l2)+        VL.qsort bud v+        pureAfter (VL.toVector PL.$ reclaim lend)+qsortWith Sequential _ v =+  unur PL.$ linearly \lin ->+    DataFlow.do+      (lin, l2) <- dup lin+      runBO lin Control.do+        (v, lend) <- borrowM (VL.fromVector v l2)+        VL.qsort 0 v+        pureAfter (VL.toVector PL.$ reclaim lend)+qsortWith (Worksteal workers thresh) _ v =+  unur PL.$ linearly \lin ->+    DataFlow.do+      (lin, l2) <- dup lin+      runBO lin Control.do+        (v, lend) <- borrowM (VL.fromVector v l2)+        Control.void PL.$ qsortDC workers thresh v+        pureAfter (VL.toVector PL.$ reclaim lend)++defaultMainWith :: CLIOpts -> IO ()+defaultMainWith CLIOpts {..} = do+  putStrLn $ "Sorting " <> show size <> " elements with mode: " <> show mode+  gen <- case seed of+    Just s -> return $ mkStdGen s+    Nothing -> newStdGen+  let !vec =+        runStateGen_ gen \g -> do+          V.replicateM size (uniformM g)+  gen <- newStdGen+  performGC+  void $ evaluate $ force $ qsortWith mode gen vec++defaultMain :: IO ()+defaultMain = do+  numCap <- getNumCapabilities+  opts <- Opts.execParser $ optionsP numCap+  defaultMainWith opts
+ pure-borrow.cabal view
@@ -0,0 +1,298 @@+cabal-version: 3.4+name: pure-borrow+version: 0.0.0.0+synopsis: Rust-style borrowing in Linear Haskell with purity+description:+  This package realizes rust-style borrowing in Linear Haskell with purity and concurrency support.+  See "Control.Monad.Borrow.Pure" for the main API documentation, and see our paper [/Pure Borrowing: Linear Haskell Meets Rust-Style Borrowing/](https://arxiv.org/abs/2604.15290) by Y. Matsushita and H. Ishii for the details.++license: BSD-3-Clause+license-file: LICENSE+author: Yusuke Matsushita and Hiromi Ishii+maintainer:+  ysk.m24t@gmail.com+  konn.jinro@gmail.com++copyright: Copyright (c) 2025-present, Yusuke Matsushita and Hiromi Ishii+category: Linear Haskell+build-type: Simple+homepage: https://github.com/SoftwareFoundationGroupAtKyotoU/pure-borrow+extra-doc-files:+  CHANGELOG.md+  README.md++data-files:+  dockerfiles/artifact/Dockerfile+  scripts/genplot.gnuplot++tested-with: ghc ==9.10.2 || ==9.12.4 || ==9.14.1++source-repository head+  type: git+  location: https://github.com/SoftwareFoundationGroupAtKyotoU/pure-borrow++flag artifact+  description: Build the artifact runner executable, which runs all the benchmarks and produces CSV files.+  default: False+  manual: True++common defaults+  default-language: GHC2021+  default-extensions: LinearTypes+  autogen-modules: Paths_pure_borrow+  other-modules: Paths_pure_borrow+  ghc-options:+    -Wall+    -Wcompat+    -Widentities+    -Wincomplete-record-updates+    -Wincomplete-uni-patterns+    -Wmissing-export-lists+    -Wmissing-home-modules+    -Wpartial-fields+    -Wredundant-constraints+    -Wunused-packages++  build-depends:+    base >=4.17 && <5,+    linear-base >=0.7,++library+  import: defaults+  build-depends:+    array,+    containers,+    deepseq,+    hybrid-vectors,+    linear-generics,+    stm,+    vector,+    vector-algorithms,++  hs-source-dirs: src+  -- cabal-gild: discover src --exclude src/**/Utils.hs --exclude src/**/Utils/**/*.hs+  exposed-modules:+    Control.Concurrent.DivideConquer.Linear+    Control.Concurrent.STM.TMDeque+    Control.Concurrent.STM.TMDequeRingBuffer+    Control.Monad.Borrow.Pure+    Control.Monad.Borrow.Pure.Affine+    Control.Monad.Borrow.Pure.Affine.Internal+    Control.Monad.Borrow.Pure.Affine.Unsafe+    Control.Monad.Borrow.Pure.BO+    Control.Monad.Borrow.Pure.BO.Internal+    Control.Monad.Borrow.Pure.BO.Unsafe+    Control.Monad.Borrow.Pure.Clone+    Control.Monad.Borrow.Pure.Copyable+    Control.Monad.Borrow.Pure.Experimental.Borrows+    Control.Monad.Borrow.Pure.Experimental.Loop+    Control.Monad.Borrow.Pure.Experimental.Reborrowable+    Control.Monad.Borrow.Pure.Lifetime+    Control.Monad.Borrow.Pure.Lifetime.Internal+    Control.Monad.Borrow.Pure.Lifetime.Token+    Control.Monad.Borrow.Pure.Lifetime.Token.Internal+    Control.Monad.Borrow.Pure.Lifetime.Token.Unsafe+    Control.Syntax.DataFlow+    Data.Coerce.Directed+    Data.Coerce.Directed.Internal+    Data.Coerce.Directed.Unsafe+    Data.Comonad.Linear+    Data.Record.Linear.Borrow.Experimental.PatternMatch+    Data.Record.Linear.Borrow.Experimental.Split+    Data.Ref.Linear+    Data.Ref.Linear.Borrow+    Data.Ref.Linear.Unlifted+    Data.Unique.Linear+    Data.Vector.Mutable.Linear.Borrow++  -- cabal-gild: discover src --include src/**/Utils.hs --include src/**/Utils/**/*.hs+  other-modules:+    Control.Concurrent.DivideConquer.Utils.OnceChan.Linear+    Control.Concurrent.DivideConquer.Utils.OnceChan.Linear.Unlifted+    Control.Concurrent.DivideConquer.Utils.QueuePool+    Control.Monad.Borrow.Pure.Utils++  build-tool-depends: cabal-gild:cabal-gild >=1.6.0.0+  build-depends:++test-suite pure-borrow-test+  import: defaults+  default-language: GHC2021+  type: exitcode-stdio-1.0+  hs-source-dirs: test+  main-is: Main.hs+  -- cabal-gild: discover test --exclude=test/Main.hs+  other-modules:+    Control.Concurrent.DivideConquer.LinearSpec+    Control.Monad.Borrow.Pure.Lifetime.TypingCases+    Control.Monad.Borrow.Pure.LifetimeSpec+    Data.Vector.Mutable.Linear.BorrowSpec++  ghc-options:+    -O2+    -threaded+    -with-rtsopts=-N++  build-tool-depends:+    tasty-discover:tasty-discover >=5.0.1++  build-depends:+    deepseq,+    falsify,+    pure-borrow,+    tasty,+    tasty-expected-failure,+    tasty-hunit,+    vector,++test-suite pure-borrow-doctests+  import: defaults++  -- NOTE: the older GHC has a bug where REPL segfaults with LinearTypes.+  -- See: https://gitlab.haskell.org/ghc/ghc/-/issues/26565#note_645783+  if impl(ghc <9.12.3)+    buildable: False+  default-language: GHC2021+  type: exitcode-stdio-1.0+  hs-source-dirs: doctests+  main-is: doctests.hs+  -- cabal-gild: discover doctests --exclude=test/doctests.hs+  other-modules:+  ghc-options:+    -O2+    -threaded+    -with-rtsopts=-N++  build-depends:+    doctest-parallel >=0.4.1,+    pure-borrow,++library qsort-bench-suites+  import: defaults+  hs-source-dirs: internal-src/qsort-bench-suites+  -- cabal-gild: discover internal-src/qsort-bench-suites+  exposed-modules: PureBorrow.Internal.Bench.QSort+  build-depends:+    base >=4.7 && <5,+    deepseq,+    optparse-applicative,+    pure-borrow,+    random,+    tasty,+    tasty-bench,+    vector,+    vector-algorithms,++  default-language: GHC2021++benchmark qsort-bench+  import: defaults+  type: exitcode-stdio-1.0+  main-is: qsort.hs+  hs-source-dirs: bench+  ghc-options:+    -threaded+    -rtsopts+    -O2+    "-with-rtsopts=-N -s"++  build-depends:+    base >=4.7 && <5,+    pure-borrow:qsort-bench-suites,++  default-language: GHC2021++library qsort-demo-impl+  import: defaults+  hs-source-dirs: internal-src/qsort-demo-impl+  -- cabal-gild: discover internal-src/qsort-demo-impl+  exposed-modules: PureBorrow.Demo.QSort+  build-depends:+    base >=4.7 && <5,+    deepseq,+    optparse-applicative,+    pure-borrow,+    random,+    vector,+    vector-algorithms,++  default-language: GHC2021++executable qsort+  import: defaults+  main-is: qsort.hs+  hs-source-dirs: app+  ghc-options:+    -threaded+    -rtsopts+    -with-rtsopts=-N++  build-depends:+    base >=4.7 && <5,+    pure-borrow:qsort-demo-impl,++  default-language: GHC2021++executable convert-qsort-bench-csv+  import: defaults+  main-is: convert-qsort-bench-csv.hs+  hs-source-dirs: app+  ghc-options:+    -threaded+    -rtsopts+    -with-rtsopts=-N++  build-depends:+    base >=4.7 && <5,+    bytestring,+    cassava,+    deepseq,+    monoidal-containers,+    optparse-applicative,+    pure-borrow,+    text,+    unordered-containers,+    vector,+    vector-algorithms,++  default-language: GHC2021++executable artifact-runner+  import: defaults++  if flag(artifact)+    buildable: True+  else+    buildable: False++  main-is: artifact-runner.hs+  hs-source-dirs: app+  ghc-options:+    -O2+    -threaded+    -rtsopts+    "-with-rtsopts=-N -s"++  build-depends:+    base >=4.7 && <5,+    bytestring,+    cassava,+    containers,+    deepseq,+    directory,+    file-embed,+    monoidal-containers,+    optparse-applicative,+    process,+    pure-borrow,+    pure-borrow:qsort-bench-suites,+    pure-borrow:qsort-demo-impl,+    tasty,+    template-haskell,+    temporary,+    text,+    transformers,+    vector,+    vector-algorithms,++  default-language: GHC2021
+ scripts/genplot.gnuplot view
@@ -0,0 +1,98 @@+# Gnuplot script for qsort benchmark plots+# Usage: gnuplot -e "input='path/to/data.csv'" scripts/genplot.gnuplot+# If input is not set, defaults to the CSV name derived from git rev.++if (!exists("input")) input = "qsort.csv"+if (!exists("output")) output = "qsort.png"++set terminal pngcairo enhanced color size 1600,700 font "Latin Modern Roman,12"+set output output++set datafile separator ","++# ── Colours & styles ─────────────────────────────────────────────────+# Intro          : black  solid line, no markers+# Sequential     : red    solid line, no markers+# Naïve  4 / 16 / 32 : blue / green / black, open triangles+# WS     4 /  8 / 10 : blue / green / black, + markers++set style line 1 lc rgb "black" lw 1.4 dt 1          # Intro+set style line 2 lc rgb "red"   lw 1.0 dt 1          # Sequential+set style line 3 lc rgb "blue"  lw 1.0 dt 1 pt 8 ps 1.8   # Naive 4  (open triangle up)+set style line 4 lc rgb "green" lw 1.0 dt 1 pt 8 ps 1.8   # Naive 16 (open triangle up)+set style line 5 lc rgb "black" lw 1.0 dt 1 pt 8 ps 1.8   # Naive 32 (open triangle up)+set style line 6 lc rgb "blue"  lw 1.0 dt 1 pt 1 ps 1.8   # WS 4     (+)+set style line 7 lc rgb "green" lw 1.0 dt 1 pt 1 ps 1.8   # WS 8     (+)+set style line 8 lc rgb "black" lw 1.0 dt 1 pt 1 ps 1.8   # WS 10    (+)++# ── Layout (manual positioning) ──────────────────────────────────────+# Reserve bottom 20% for the shared legend+legend_h = 0.20+plot_b   = legend_h+plot_t   = 0.98+plot_gap = 0.08++set multiplot+unset key++# ── Left panel: Wall Clock Time ──────────────────────────────────────+set lmargin at screen 0.07+set rmargin at screen 0.48+set bmargin at screen plot_b+set tmargin at screen plot_t+set xlabel 'N'+set ylabel 'Wall Clock Time [ms]'++plot \+  input using "size":"introMean"       with lines      ls 1 notitle, \+  input using "size":"sequentialMean"   with lines      ls 2 notitle, \+  input using "size":"parallel4Mean"    with linespoints ls 3 notitle, \+  input using "size":"parallel16Mean"   with linespoints ls 4 notitle, \+  input using "size":"parallel32Mean"   with linespoints ls 5 notitle, \+  input using "size":"workSteal4Mean"   with linespoints ls 6 notitle, \+  input using "size":"workSteal8Mean"   with linespoints ls 7 notitle, \+  input using "size":"workSteal10Mean"  with linespoints ls 8 notitle++# ── Right panel: Allocation ──────────────────────────────────────────+set lmargin at screen 0.56+set rmargin at screen 0.97+set bmargin at screen plot_b+set tmargin at screen plot_t+set xlabel 'N'+set ylabel 'Allocation [MB]'++plot \+  input using "size":"introAlloc"       with lines      ls 1 notitle, \+  input using "size":"sequentialAlloc"   with lines      ls 2 notitle, \+  input using "size":"parallel4Alloc"    with linespoints ls 3 notitle, \+  input using "size":"parallel16Alloc"   with linespoints ls 4 notitle, \+  input using "size":"parallel32Alloc"   with linespoints ls 5 notitle, \+  input using "size":"workSteal4Alloc"   with linespoints ls 6 notitle, \+  input using "size":"workSteal8Alloc"   with linespoints ls 7 notitle, \+  input using "size":"workSteal10Alloc"  with linespoints ls 8 notitle++# ── Shared legend (dummy plot spanning full width) ───────────────────+set lmargin at screen 0.07+set rmargin at screen 0.97+set bmargin at screen 0.0+set tmargin at screen legend_h+unset xlabel+unset ylabel+unset tics+unset border+set xrange [0:1]+set yrange [0:1]+set key center center horizontal samplen 2 spacing 1.2 \+    font ",15" maxrows 1++plot \+  NaN with lines      ls 1 title 'Intro', \+  NaN with lines      ls 2 title 'Sequential', \+  NaN with linespoints ls 3 title "Naive 4", \+  NaN with linespoints ls 4 title "Naive 16", \+  NaN with linespoints ls 5 title "Naive 32", \+  NaN with linespoints ls 6 title 'WS 4', \+  NaN with linespoints ls 7 title 'WS 8', \+  NaN with linespoints ls 8 title 'WS 10'++unset multiplot
+ src/Control/Concurrent/DivideConquer/Linear.hs view
@@ -0,0 +1,266 @@+{-# LANGUAGE BlockArguments #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE DeriveAnyClass #-}+{-# LANGUAGE DerivingStrategies #-}+{-# LANGUAGE DerivingVia #-}+{-# LANGUAGE ImpredicativeTypes #-}+{-# LANGUAGE LambdaCase #-}+{-# LANGUAGE LinearTypes #-}+{-# LANGUAGE MultiWayIf #-}+{-# LANGUAGE OverloadedRecordDot #-}+{-# LANGUAGE QualifiedDo #-}+{-# LANGUAGE RecordWildCards #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TemplateHaskell #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE NoImplicitPrelude #-}+{-# OPTIONS_GHC -Wno-name-shadowing #-}+{-# OPTIONS_GHC -Wno-partial-type-signatures #-}++module Control.Concurrent.DivideConquer.Linear (+  divideAndConquer,+  DivideConquer (..),++  -- * Examples+  qsortDC,+) where++import Control.Applicative qualified as NonLinear+import Control.Concurrent (ThreadId, forkIO, killThread)+import Control.Concurrent.DivideConquer.Utils.OnceChan.Linear (Sink, Source)+import Control.Concurrent.DivideConquer.Utils.OnceChan.Linear qualified as Once+import Control.Concurrent.DivideConquer.Utils.QueuePool (QueuePool, newQueuePool, popWork, pushWork, pushWorkMaster)+import Control.Functor.Linear qualified as Control+import Control.Monad.Borrow.Pure.Affine (Affine, GenericallyAffine (..))+import Control.Monad.Borrow.Pure.BO+import Control.Monad.Borrow.Pure.BO.Unsafe+import Control.Monad.Borrow.Pure.Copyable+import Data.Functor.Linear qualified as Data+import Data.Kind (Type)+import Data.List.Linear qualified as LL+import Data.List.NonEmpty.Linear (NonEmpty (..))+import Data.List.NonEmpty.Linear qualified as NEL+import Data.Proxy (Proxy (..))+import Data.V.Linear (V)+import Data.V.Linear.Internal (V (..))+import Data.Vector qualified as V+import Data.Vector.Mutable.Linear.Borrow qualified as LV+import GHC.Exts qualified as GHC+import GHC.Generics qualified as GHC+import GHC.TypeNats (SomeNat (..), someNatVal)+import Generics.Linear.TH (deriveGenericAnd1)+import Prelude.Linear+import Prelude.Linear.Generically (Generically, Generically1)+import System.IO.Unsafe (unsafePerformIO)+import Unsafe.Linear qualified as Unsafe++data DivideConquer α t a = DivideConquer+  { divide :: forall β. (α >= β) => Mut β a %1 -> BO β (Result β t a)+  }++data Result β t a = Done | Continue (t (Mut β a))++data Work α a (t :: Type -> Type) where+  Process :: Mut α a %1 -> Sink () %1 -> Work α a t %1 -> Work α a t+  Unite :: t (Source ()) %1 -> Sink () %1 -> Work α a t+  Final :: Work α a t++newtype Thread = Thread ThreadId++instance Consumable Thread where+  {-# NOINLINE consume #-}+  consume = GHC.noinline $ Unsafe.toLinear \(Thread tid) -> unsafePerformIO $ do+    killThread tid++newtype DList a = DList ([a] %1 -> [a])++instance Semigroup (DList a) where+  DList f <> DList g = DList (f . g)+  {-# INLINE (<>) #-}++instance Monoid (DList a) where+  mempty = DList id+  {-# INLINE mempty #-}++singletonD :: a %1 -> DList a+singletonD = DList . (:)+{-# INLINE singletonD #-}++toListD :: DList a %1 -> [a]+toListD (DList f) = f []+{-# INLINE toListD #-}++-- TODO: perhaps we can use atomic counter here again?++data QState α a t+  = Idle !(Mut α (QueuePool (Work α a t)))+  | DoThen !(Work α a t) !(Mut α (QueuePool (Work α a t)))++popQState ::+  QState α a t %1 ->+  BO α (Maybe (Work α a t, QState α a t))+popQState = \case+  Idle q -> Control.do+    m <- popWork q+    case m of+      Nothing -> Control.pure Nothing+      Just (work, q) -> Control.pure (Just (work, Idle q))+  DoThen work q -> Control.pure $ Just (work, Idle q)++enqueue :: QState α a t %1 -> Work α a t %1 -> BO α (QState α a t)+enqueue q work = case q of+  Idle q -> Idle Control.<$> pushWork q work+  DoThen work' q -> error "Could not happen!" work q work'++doAndEnqueue :: QState α a t %1 -> Work α a t %1 -> Work α a t %1 -> BO α (QState α a t)+doAndEnqueue q work cont = case q of+  Idle q -> DoThen work Control.<$> pushWork q cont+  DoThen work' q -> error "Could not happen!" work cont work' q++divideAndConquer ::+  forall α β t a.+  (Data.Traversable t, Consumable (t ()), α >= β) =>+  -- | The # of workers.+  Int ->+  DivideConquer α t a ->+  Mut α a %1 ->+  BO β (Mut α a)+divideAndConquer n DivideConquer {..} ini+  | n == 0 = error ("divideAndConquer: # of workers must be positive, but got: " <> show n) ini+  | otherwise =+      upcast $+        uncurry (lseq @()) Control.<$> reborrowing' ini \(ini :: Mut γ a) ->+          someNatVal (fromIntegral n) & \(SomeNat (_ :: Proxy n)) -> Control.do+            (workers, master) <- newQueuePool @n+            (masterQ, masterLend) <- asksLinearly $ borrow master+            (rootSink, rootSource) <- asksLinearly Once.new++            Control.void $ pushWorkMaster masterQ $ Process ini rootSink Final++            concurrentMap_ worker workers+            Once.take rootSource++            Control.pure (upcast $ consume Control.<$> reclaim' masterLend)+  where+    worker :: (α >= α') => Mut α' (QueuePool (Work α' a t)) %1 -> BO α' ()+    worker q =+      whileJust_ (Idle q) popQState \q -> \case+        Final -> Control.pure q+        Process ini sink next -> Control.do+          q <- enqueue q next+          resl <- divide ini+          case resl of+            Done -> Control.do+              Once.put sink ()+              Control.pure q+            Continue ts -> Control.do+              (sources, ks) <-+                flip Control.runStateT mempty $ Data.for ts \work -> Control.do+                  (sink, source) <- Control.lift $ asksLinearly Once.new+                  Control.modify (<> singletonD (work, sink))+                  Control.pure source+              let %1 !cont = Unite sources sink+              case NEL.nonEmpty $ toListD ks of+                Nothing -> enqueue q cont+                Just ((ini, sink) :| ks) ->+                  doAndEnqueue+                    q+                    (Process ini sink Final)+                    $ LL.foldr (uncurry Process) cont ks+        Unite children sink -> Control.do+          Control.void $ Data.traverse Once.take children+          Once.put sink ()+          Control.pure q++concurrentMap_ ::+  forall n a α.+  (a %1 -> BO α ()) ->+  V n a %1 ->+  BO α ()+concurrentMap_ k = Unsafe.toLinear \(V ts) -> unsafeSystemIOToBO do+  V.mapM_+    (\a -> unsafeBOToSystemIO $ forkBO (k a))+    ts++forkBO :: BO α () %1 -> BO α Thread+forkBO = Unsafe.toLinear \bo ->+  unsafeSystemIOToBO (Thread NonLinear.<$> forkIO (unsafeBOToSystemIO bo))++whileJust_ ::+  (Control.Monad m) =>+  r %1 ->+  (r %1 -> m (Maybe (a, r))) ->+  (r %1 -> a %1 -> m r) ->+  m ()+whileJust_ ini next action = loop ini+  where+    loop cur = Control.do+      m <- next cur+      case m of+        Nothing -> Control.pure ()+        Just (!x, !cur) -> Control.do+          cur <- action cur x+          loop cur++data Pair a where+  Pair :: !a %1 -> !a %1 -> Pair a+  deriving (GHC.Generic, GHC.Generic1)++deriveGenericAnd1 ''Pair++deriving via Generically1 Pair instance Data.Functor Pair++deriving via+  Generically (Pair a)+  instance+    (Consumable a) => Consumable (Pair a)++deriving via+  Generically (Pair a)+  instance+    (Dupable a) => Dupable (Pair a)++deriving via+  GenericallyAffine (Pair a)+  instance+    (Affine a) => Affine (Pair a)++deriving via+  Generically (Pair a)+  instance+    (Movable a) => Movable (Pair a)++instance Data.Traversable Pair where+  traverse = Data.genericTraverse+  {-# INLINE traverse #-}++qsortDC ::+  (Ord a, Copyable a, α >= β) =>+  -- | The # of workers.+  Int ->+  -- | Threshold for the length of vector to switch to sequential sort.+  Int ->+  Mut α (LV.Vector a) %1 ->+  BO β (Mut α (LV.Vector a))+qsortDC nwork thresh = divideAndConquer nwork (qsortDC' thresh)++qsortDC' ::+  (Ord a, Copyable a) =>+  -- | Threshold for the length of vector to switch to sequential sort.+  Int ->+  DivideConquer α Pair (LV.Vector a)+qsortDC' thresh =+  DivideConquer+    { divide = \vs ->+        case LV.size vs of+          (Ur n, v)+            | n <= 1 ->+                v `lseq` Control.pure Done+            | n <= thresh ->+                Done Control.<$ LV.qsort 0 v+            | otherwise -> Control.do+                let i = n `quot` 2+                (Ur pivot, v) <- LV.copyAtMut i v+                (lo, hi) <- LV.divide pivot v 0 n+                Control.pure $ Continue $ Pair lo hi+    }
+ src/Control/Concurrent/DivideConquer/Utils/OnceChan/Linear.hs view
@@ -0,0 +1,67 @@+{-# LANGUAGE BlockArguments #-}+{-# LANGUAGE MagicHash #-}+{-# LANGUAGE QualifiedDo #-}+{-# LANGUAGE RoleAnnotations #-}+{-# LANGUAGE UnboxedTuples #-}+{-# LANGUAGE UnliftedNewtypes #-}+{-# LANGUAGE NoImplicitPrelude #-}+{-# OPTIONS_GHC -Wno-name-shadowing #-}++module Control.Concurrent.DivideConquer.Utils.OnceChan.Linear (+  Sink,+  Source,+  new,+  put,+  take,+) where++import Control.Concurrent.DivideConquer.Utils.OnceChan.Linear.Unlifted+import Control.Monad.Borrow.Pure.Affine+import Control.Monad.Borrow.Pure.Affine.Unsafe (unsafeAff)+import Control.Monad.Borrow.Pure.BO+import Control.Monad.Borrow.Pure.Lifetime.Token.Unsafe (+  LinearOnly (..),+  LinearOnlyWitness (..),+ )+import Data.Unrestricted.Linear+import Prelude.Linear hiding (take)+import Unsafe.Linear qualified as Unsafe++data Sink a = Sink (Sink# a)++data Source a = Source (Source# a)++type role Sink nominal++type role Source representational++new :: Linearly %1 -> (Sink a, Source a)+{-# INLINE new #-}+new lin = case new# lin of+  (# sink, source #) -> (Sink sink, Source source)++instance LinearOnly (Sink a) where+  linearOnly = UnsafeLinearOnly++instance LinearOnly (Source a) where+  linearOnly = UnsafeLinearOnly++instance Affine (Sink a) where+  aff = unsafeAff++instance Consumable (Sink a) where+  consume = Unsafe.toLinear \(Sink !_) -> ()++instance Consumable (Source a) where+  consume = Unsafe.toLinear \(Source !_) -> ()++instance Affine (Source a) where+  aff = unsafeAff++take :: Source a %1 -> BO α a+{-# INLINE take #-}+take (Source v) = evaluateBO $ take# v++put :: Sink a %1 -> a %1 -> BO α ()+{-# INLINE put #-}+put (Sink v) !a = evaluateBO $ put# v a
+ src/Control/Concurrent/DivideConquer/Utils/OnceChan/Linear/Unlifted.hs view
@@ -0,0 +1,59 @@+{-# LANGUAGE BlockArguments #-}+{-# LANGUAGE MagicHash #-}+{-# LANGUAGE RoleAnnotations #-}+{-# LANGUAGE UnboxedTuples #-}+{-# LANGUAGE UnliftedNewtypes #-}+{-# LANGUAGE NoImplicitPrelude #-}+{-# OPTIONS_GHC -Wno-name-shadowing #-}++module Control.Concurrent.DivideConquer.Utils.OnceChan.Linear.Unlifted (+  Sink#,+  Source#,+  new#,+  put#,+  take#,+) where++import Control.Monad.Borrow.Pure.Lifetime.Token+import Control.Monad.Borrow.Pure.Lifetime.Token.Unsafe (+  LinearOnly (..),+  LinearOnlyWitness (..),+ )+import GHC.Exts qualified as GHC+import Prelude.Linear+import Unsafe.Linear qualified as Unsafe++newtype Source# a = Source# (GHC.MVar# GHC.RealWorld a)++newtype Sink# a = Sink# (GHC.MVar# GHC.RealWorld a)++type role Source# representational++type role Sink# nominal++new# :: Linearly %1 -> (# Sink# a, Source# a #)+{-# NOINLINE new# #-}+new# = GHC.noinline $ Unsafe.toLinear $ \_ ->+  GHC.runRW# \s ->+    case GHC.newMVar# s of+      (# _, !v #) -> (# Sink# v, Source# v #)++take# :: Source# a %1 -> a+{-# INLINE take# #-}+take# = GHC.noinline $ Unsafe.toLinear \(Source# mv) ->+  GHC.runRW# \s ->+    case GHC.takeMVar# mv s of+      (# _, !a #) -> a++put# :: Sink# a %1 -> a %1 -> ()+{-# NOINLINE put# #-}+put# = GHC.noinline $ Unsafe.toLinear2 \(Sink# mv) !a ->+  GHC.runRW# \s ->+    case GHC.putMVar# mv a s of+      !_ -> ()++instance LinearOnly (Sink# a) where+  linearOnly = UnsafeLinearOnly++instance LinearOnly (Source# a) where+  linearOnly = UnsafeLinearOnly
+ src/Control/Concurrent/DivideConquer/Utils/QueuePool.hs view
@@ -0,0 +1,156 @@+{-# LANGUAGE BlockArguments #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE DeriveAnyClass #-}+{-# LANGUAGE DerivingStrategies #-}+{-# LANGUAGE DerivingVia #-}+{-# LANGUAGE ImpredicativeTypes #-}+{-# LANGUAGE LambdaCase #-}+{-# LANGUAGE LinearTypes #-}+{-# LANGUAGE MagicHash #-}+{-# LANGUAGE MultiWayIf #-}+{-# LANGUAGE OverloadedLabels #-}+{-# LANGUAGE OverloadedRecordDot #-}+{-# LANGUAGE QualifiedDo #-}+{-# LANGUAGE RecordWildCards #-}+{-# LANGUAGE TemplateHaskell #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE UnboxedTuples #-}+{-# LANGUAGE UndecidableInstances #-}+{-# LANGUAGE NoImplicitPrelude #-}+{-# OPTIONS_GHC -Wno-name-shadowing #-}+{-# OPTIONS_GHC -Wno-partial-type-signatures #-}++module Control.Concurrent.DivideConquer.Utils.QueuePool (+  QueuePool,+  newQueuePool,+  pushWork,+  pushWorks,+  popWork,+  pushWorkMaster,+) where++import Control.Applicative (Alternative (..))+import Control.Applicative qualified as P+import Control.Concurrent (yield)+import Control.Concurrent.STM (STM, atomically, retry)+import Control.Concurrent.STM.TMDeque (TMDeque, closeTMDeque, isClosedTMDeque, newTMDequeIO, pushFrontTMDeque, sizeTMDeque, tryPopBackTMDeque, tryPopFrontTMDeque)+import Control.Monad qualified as NonLinear+import Control.Monad qualified as P+import Control.Monad.Borrow.Pure.BO+import Control.Monad.Borrow.Pure.BO.Unsafe (Alias (..), unsafeSystemIOToBO)+import Data.Coerce (coerce)+import Data.Foldable qualified as P+import Data.Function (fix)+import Data.List qualified as L+import Data.Monoid (Alt (..))+import Data.Ord (Down (..))+import Data.Ord qualified as P+import Data.V.Linear (V, theLength)+import Data.V.Linear.Internal (V (..))+import Data.Vector qualified as V+import Data.Vector.Algorithms.Intro qualified as AI+import Data.Vector.Hybrid.Mutable qualified as HMV+import Data.Vector.Mutable (RealWorld)+import GHC.Exts qualified as GHC+import GHC.IO qualified as GHC+import GHC.TypeLits (KnownNat)+import Prelude.Linear+import Unsafe.Linear qualified as Unsafe+import Prelude qualified as P++data QueuePool a = QueuePool+  { mine :: !(TMDeque a)+  , others :: !(V.MVector RealWorld (TMDeque a))+  , num :: !Int+  }++newtype MasterQueuePool a = MasterQueuePool [TMDeque a]++instance Consumable (MasterQueuePool a) where+  consume = consume . map consumeTMDQ . Unsafe.coerce @_ @[TMDeque a]++consumeTMDQ :: TMDeque a %1 -> ()+{-# NOINLINE consumeTMDQ #-}+consumeTMDQ = GHC.noinline $ Unsafe.toLinear \q -> GHC.unsafePerformIO do+  !() <- atomically $ closeTMDeque q+  P.pure ()++newQueuePool ::+  forall n a α.+  (KnownNat n) =>+  BO α (V n (Mut α (QueuePool a)), MasterQueuePool a)+newQueuePool = unsafeSystemIOToBO do+  let n = theLength @n++  qs <- NonLinear.replicateM n newTMDequeIO+  pools <-+    P.mapM+      ( \(num, ini, mine, tl) -> do+          others <- V.unsafeThaw $ V.fromList $ tl <> ini+          P.pure P.$ QueuePool {others, ..}+      )+      P.$ L.zip4+        [0 ..]+        (L.inits qs)+        qs+        (P.drop 1 $ L.tails qs)+  let master = MasterQueuePool $ P.map (mine P.. coerce) pools+  P.pure (V $ V.fromList $ map UnsafeAlias pools, master)++pushWorkMaster :: Mut α (MasterQueuePool a) %1 -> a %1 -> BO α (Mut α (MasterQueuePool a))+pushWorkMaster = Unsafe.toLinear2 \(UnsafeAlias (MasterQueuePool pools)) work ->+  case pools of+    (q : qs) -> unsafeSystemIOToBO do+      atomically $ pushFrontTMDeque q work+      P.pure $ UnsafeAlias $ MasterQueuePool (q : qs)+    [] -> error "impossible: the length of pools is determined by the type-level nat n and cannot be zero"++pushWork :: Mut α (QueuePool a) %1 -> a %1 -> BO α (Mut α (QueuePool a))+pushWork = Unsafe.toLinear2 \(UnsafeAlias QueuePool {..}) work ->+  unsafeSystemIOToBO do+    atomically $ pushFrontTMDeque mine work+    P.pure $ UnsafeAlias QueuePool {..}++newtype Backwards f a = Backwards {runBackwards :: f a}+  deriving newtype (P.Functor)++instance (P.Applicative f) => P.Applicative (Backwards f) where+  pure = Backwards P.. P.pure+  Backwards f <*> Backwards x = Backwards (x P.<**> f)++-- | Pushes works, the first element is on top.+pushWorks :: Mut α (QueuePool a) %1 -> [a] %1 -> BO α (Mut α (QueuePool a))+pushWorks = Unsafe.toLinear2 \(UnsafeAlias QueuePool {..}) work ->+  unsafeSystemIOToBO do+    atomically $ runBackwards P.$ P.traverse_ (Backwards P.. pushFrontTMDeque mine) work+    P.pure $ UnsafeAlias QueuePool {..}++popWork :: Mut α (QueuePool a) %1 -> BO α (Maybe (a, Mut α (QueuePool a)))+popWork = Unsafe.toLinear \qs@(UnsafeAlias QueuePool {..}) ->+  unsafeSystemIOToBO do+    atomically (tryPopFrontTMDeque mine) P.>>= \case+      Nothing -> P.pure Nothing+      Just (Just x) -> P.pure $ Just (x, qs)+      Just Nothing -> fix \self -> do+        !ranks <-+          V.unsafeThaw+            P.=<< atomically P.. (\x -> do xs <- V.mapM sizeTMDeque x; xs P.<$ P.unless (V.any (P.> 0) xs) retry)+            P.=<< V.unsafeFreeze others+        let ranked = HMV.unsafeZip ranks others+        !() <- AI.sortBy (P.comparing P.$ Down P.. P.fst) ranked+        others' <- V.unsafeFreeze others++        progress <-+          atomically do+            ( isClosedTMDeque mine P.>>= \closed ->+                if closed then P.pure Nothing else retry+              )+              <|> getAlt (P.foldMap' (Alt P.. (P.fmap Just P.. fromJustSTM P.<=< tryPopBackTMDeque)) P.$ others')+              <|> P.pure (Just Nothing)+        case progress of+          Nothing -> P.pure Nothing+          Just Nothing -> yield P.*> self+          Just (Just x) -> P.pure $ Just (x, qs)++fromJustSTM :: Maybe (Maybe a) -> STM (Maybe a)+fromJustSTM = P.maybe (P.pure Nothing) $ P.maybe retry (P.pure P.. Just)
+ src/Control/Concurrent/STM/TMDeque.hs view
@@ -0,0 +1,229 @@+{-# LANGUAGE BlockArguments #-}+{-# LANGUAGE NoLinearTypes #-}++{- | A closable, concurrent double-ended queue backed by STM, with amortized+O(1) operations. The underlying implementation uses a two-stack design with+separate 'TVar's for the front and rear, reducing STM contention: in the+common case, @pushFront@ and @popBack@ touch disjoint variables and do not+conflict.++Closing semantics follow @stm-chans@ conventions:++  * __Closed + empty__ → read returns @Nothing@ (end-of-stream)+  * __Closed + non-empty__ → read returns @Just a@ (drain remaining)+  * __Open + empty__ → read blocks (@retry@)+  * __Open + non-empty__ → read returns @Just a@+  * __Write to closed__ → silently ignored+-}+module Control.Concurrent.STM.TMDeque (+  -- * The TMDeque type+  TMDeque,++  -- * Construction+  newTMDeque,+  newTMDequeIO,++  -- * Push operations+  pushFrontTMDeque,++  -- * Pop operations (blocking)+  popFrontTMDeque,+  popBackTMDeque,++  -- * Pop operations (non-blocking)+  tryPopFrontTMDeque,+  tryPopBackTMDeque,++  -- * Closing & queries+  closeTMDeque,+  isClosedTMDeque,+  isClosedTMDequeIO,+  isEmptyTMDeque,+  sizeTMDeque,+  countTMDequeIO,+) where++import Control.Concurrent.STM (STM, TVar, modifyTVar', newTVar, newTVarIO, readTVar, retry, writeTVar)+import Control.Concurrent.STM.TVar (readTVarIO)+import Control.Monad (unless)++{- | Reverse a non-empty list and split into head and tail.+Precondition: the input list is non-empty.+-}+unconsReverse :: [a] -> (a, [a])+unconsReverse xs = case reverse xs of+  y : ys -> (y, ys)+  [] -> error "TMDeque.unconsReverse: impossible – called on empty list"++------------------------------------------------------------------------+-- STM two-stack queue+------------------------------------------------------------------------++-- | A closable, STM-backed double-ended queue with amortized O(1) operations.+data TMDeque a+  = TMDeque+      {-# UNPACK #-} !(TVar Bool) -- closed flag (monotonic: False → True)+      {-# UNPACK #-} !(TVar [a]) -- front (push end)+      {-# UNPACK #-} !(TVar [a]) -- rear (pop end)+      {-# UNPACK #-} !(TVar Int) -- size (maintained for O(1) count)++-- | Create a new empty 'TMDeque'.+newTMDeque :: STM (TMDeque a)+newTMDeque = TMDeque <$> newTVar False <*> newTVar [] <*> newTVar [] <*> newTVar 0++-- | IO variant of 'newTMDeque'.+newTMDequeIO :: IO (TMDeque a)+newTMDequeIO = TMDeque <$> newTVarIO False <*> newTVarIO [] <*> newTVarIO [] <*> newTVarIO 0++{- | Push an element to the front of the deque.  Silently ignored if the+deque is closed.+-}+pushFrontTMDeque :: TMDeque a -> a -> STM ()+pushFrontTMDeque (TMDeque closedVar frontVar _rearVar sizeVar) x = do+  closed <- readTVar closedVar+  unless closed do+    modifyTVar' frontVar (x :)+    modifyTVar' sizeVar (+ 1)++{- | Pop an element from the front.  Blocks if the deque is open and empty.+Returns @Nothing@ when the deque is closed and empty (end-of-stream).+-}+popFrontTMDeque :: TMDeque a -> STM (Maybe a)+popFrontTMDeque (TMDeque closedVar frontVar rearVar sizeVar) = do+  f <- readTVar frontVar+  case f of+    x : f' -> do+      writeTVar frontVar f'+      modifyTVar' sizeVar (subtract 1)+      pure (Just x)+    [] -> do+      r <- readTVar rearVar+      case r of+        _ : _ -> do+          let (x, f') = unconsReverse r+          writeTVar rearVar []+          writeTVar frontVar f'+          modifyTVar' sizeVar (subtract 1)+          pure (Just x)+        [] -> do+          closed <- readTVar closedVar+          if closed+            then pure Nothing+            else retry++{- | Non-blocking pop from the front.++  * @Nothing@         — closed (end-of-stream)+  * @Just Nothing@    — open and empty (would block)+  * @Just (Just a)@   — got an element+-}+tryPopFrontTMDeque :: TMDeque a -> STM (Maybe (Maybe a))+tryPopFrontTMDeque (TMDeque closedVar frontVar rearVar sizeVar) = do+  f <- readTVar frontVar+  case f of+    x : f' -> do+      writeTVar frontVar f'+      modifyTVar' sizeVar (subtract 1)+      pure (Just (Just x))+    [] -> do+      r <- readTVar rearVar+      case r of+        _ : _ -> do+          let (x, f') = unconsReverse r+          writeTVar rearVar []+          writeTVar frontVar f'+          modifyTVar' sizeVar (subtract 1)+          pure (Just (Just x))+        [] -> do+          closed <- readTVar closedVar+          if closed+            then pure Nothing+            else pure (Just Nothing)++{- | Pop an element from the back.  Blocks if the deque is open and empty.+Returns @Nothing@ when the deque is closed and empty (end-of-stream).+-}+popBackTMDeque :: TMDeque a -> STM (Maybe a)+popBackTMDeque (TMDeque closedVar frontVar rearVar sizeVar) = do+  r <- readTVar rearVar+  case r of+    x : r' -> do+      writeTVar rearVar r'+      modifyTVar' sizeVar (subtract 1)+      pure (Just x)+    [] -> do+      f <- readTVar frontVar+      case f of+        _ : _ -> do+          let (x, r') = unconsReverse f+          writeTVar frontVar []+          writeTVar rearVar r'+          modifyTVar' sizeVar (subtract 1)+          pure (Just x)+        [] -> do+          closed <- readTVar closedVar+          if closed+            then pure Nothing+            else retry++{- | Non-blocking pop from the back.++  * @Nothing@         — closed (end-of-stream)+  * @Just Nothing@    — open and empty (would block)+  * @Just (Just a)@   — got an element+-}+tryPopBackTMDeque :: TMDeque a -> STM (Maybe (Maybe a))+tryPopBackTMDeque (TMDeque closedVar frontVar rearVar sizeVar) = do+  r <- readTVar rearVar+  case r of+    x : r' -> do+      writeTVar rearVar r'+      modifyTVar' sizeVar (subtract 1)+      pure (Just (Just x))+    [] -> do+      f <- readTVar frontVar+      case f of+        _ : _ -> do+          let (x, r') = unconsReverse f+          writeTVar frontVar []+          writeTVar rearVar r'+          modifyTVar' sizeVar (subtract 1)+          pure (Just (Just x))+        [] -> do+          closed <- readTVar closedVar+          if closed+            then pure Nothing+            else pure (Just Nothing)++{- | Close the deque.  After closing, writes are silently ignored and reads+will drain remaining elements before signalling end-of-stream.  Closing+is idempotent.+-}+closeTMDeque :: TMDeque a -> STM ()+closeTMDeque (TMDeque closedVar _ _ _) = writeTVar closedVar True++-- | Check whether the deque has been closed.+isClosedTMDeque :: TMDeque a -> STM Bool+isClosedTMDeque (TMDeque closedVar _ _ _) = readTVar closedVar++-- | Check whether the deque has been closed.+isClosedTMDequeIO :: TMDeque a -> IO Bool+isClosedTMDequeIO (TMDeque closedVar _ _ _) = readTVarIO closedVar++-- | Check whether the deque is currently empty.+isEmptyTMDeque :: TMDeque a -> STM Bool+isEmptyTMDeque (TMDeque _ frontVar rearVar _) = do+  f <- readTVar frontVar+  case f of+    _ : _ -> pure False+    [] -> do+      r <- readTVar rearVar+      pure (null r)++-- | Return the number of elements currently in the deque. O(1).+sizeTMDeque :: TMDeque a -> STM Int+sizeTMDeque (TMDeque _ _ _ sizeVar) = readTVar sizeVar++-- | IO variant of 'countTMDeque'. O(1).+countTMDequeIO :: TMDeque a -> IO Int+countTMDequeIO (TMDeque _ _ _ sizeVar) = readTVarIO sizeVar
+ src/Control/Concurrent/STM/TMDequeRingBuffer.hs view
@@ -0,0 +1,218 @@+{-# LANGUAGE BlockArguments #-}+{-# LANGUAGE OverloadedRecordDot #-}+{-# LANGUAGE NoLinearTypes #-}++module Control.Concurrent.STM.TMDequeRingBuffer (+  -- * The TMDeque type+  TMDeque,++  -- * Construction+  newTMDeque,+  newTMDequeIO,++  -- * Push operations+  pushFrontTMDeque,++  -- * Pop operations (blocking)+  popFrontTMDeque,+  popBackTMDeque,++  -- * Pop operations (non-blocking)+  tryPopFrontTMDeque,+  tryPopBackTMDeque,++  -- * Closing & queries+  closeTMDeque,+  isClosedTMDeque,+  isClosedTMDequeIO,+  isEmptyTMDeque,+  estimateSizeTMDequeIO,+  sizeTMDeque,+) where++import Control.Concurrent.STM+import Control.Monad (when)+import Data.Array.Base (newArray_, readArray, writeArray)+import Data.Function (fix, (&))++{- | 0 | 1 | 2 | ... | i | ... | N - 1 |+      ^             ^+      |             |+     back         front+-}+data TMDeque a = TMDeque+  { closed :: TVar Bool+  , ringBuffer :: TVar (TArray Int a)+  , capacity :: TVar Int+  , front :: TVar Int+  , back :: TVar Int+  }++newtype UniqIx = UniqIx Int++initialCapacity :: Int+initialCapacity = 64++-- | Create a new empty 'TMDeque'.+newTMDeque :: STM (TMDeque a)+newTMDeque =+  TMDeque+    <$> newTVar False+    <*> (newTVar =<< newArray_ (0, initialCapacity - 1))+    <*> newTVar initialCapacity+    <*> newTVar 0+    <*> newTVar 0++-- | IO variant of 'newTMDeque', which is faster without STM transaction overhead.+newTMDequeIO :: IO (TMDeque a)+newTMDequeIO =+  TMDeque+    <$> newTVarIO False+    <*> (newTVarIO =<< newArray_ (0, initialCapacity - 1))+    <*> newTVarIO initialCapacity+    <*> newTVarIO 0+    <*> newTVarIO 0++growThreshold :: Int+growThreshold = 16++{- | Push an element to the front of the deque.  Silently ignored if the+deque is closed.+-}+pushFrontTMDeque :: TMDeque a -> a -> STM ()+pushFrontTMDeque deq v = do+  growIfNeeded deq+  capa <- readTVar deq.capacity+  UniqIx dest <- stateTVar deq.front \i ->+    let !j = i + 1+     in (UniqIx $ i `rem` capa, j)+  buf <- readTVar deq.ringBuffer+  writeArray buf dest v++growIfNeeded :: TMDeque a -> STM ()+{-# INLINE growIfNeeded #-}+growIfNeeded deq = do+  capa <- readTVar deq.capacity+  size <- sizeTMDeque deq+  when (capa - size - 1 <= growThreshold) do+    ring <- doubleDeq capa deq+    writeTVar deq.ringBuffer ring+    writeTVar deq.capacity (capa * 2)++sizeTMDeque :: TMDeque a -> STM Int+sizeTMDeque deq = do+  front <- readTVar deq.front+  back <- readTVar deq.back+  pure $ front - back++doubleDeq :: Int -> TMDeque a -> STM (TArray Int a)+{-# INLINE doubleDeq #-}+doubleDeq oldSize deq = do+  let !newSize = oldSize * 2+  back <- (`rem` oldSize) <$> readTVar deq.back+  front <- (`rem` oldSize) <$> readTVar deq.front+  arr <- readTVar deq.ringBuffer+  dest <- newArray_ (0, newSize - 1)+  if back <= front+    then -- linear copy on [back, front]+      back & fix \go !i -> when (i < front) do+        e <- readArray arr i+        writeArray dest i e+        go (i + 1)+    else do+      -- first copy [0, front), then copy [back, oldSize)+      0 & fix \go !i -> when (i < front) do+        e <- readArray arr i+        writeArray dest i e+        go (i + 1)+      back & fix \go !i -> when (i < oldSize) do+        e <- readArray arr i+        writeArray dest (i + oldSize) e+        go (i + 1)+  pure dest++{- | Pop an element from the front.  Blocks if the deque is open and empty.+Returns @Nothing@ when the deque is closed and empty (back-of-stream).+-}+popFrontTMDeque :: TMDeque a -> STM (Maybe a)+popFrontTMDeque deq = do+  may <- tryPopFrontTMDeque deq+  maybe retry pure may++{- | Pop an element from the back.  Blocks if the deque is open and empty.+Returns @Nothing@ when the deque is closed and empty (back-of-stream).+-}+popBackTMDeque :: TMDeque a -> STM (Maybe a)+popBackTMDeque deq = do+  may <- tryPopBackTMDeque deq+  maybe retry pure may++{- | Non-blocking pop from the front.++  * @Nothing@         — closed (end-of-stream)+  * @Just Nothing@    — open and empty (would block)+  * @Just (Just a)@   — got an element+-}+tryPopFrontTMDeque :: TMDeque a -> STM (Maybe (Maybe a))+tryPopFrontTMDeque deq = do+  size <- sizeTMDeque deq+  if size == 0+    then do+      closed <- readTVar deq.closed+      if closed+        then pure Nothing+        else pure (Just Nothing)+    else do+      capa <- readTVar deq.capacity+      UniqIx dest <- stateTVar deq.front \i ->+        let !j = i - 1+         in (UniqIx $ j `rem` capa, j)+      buf <- readTVar deq.ringBuffer+      e <- readArray buf dest+      pure (Just (Just e))++{- | Non-blocking pop from the back.++  * @Nothing@         — closed (end-of-stream)+  * @Just Nothing@    — open and empty (would block)+  * @Just (Just a)@   — got an element+-}+tryPopBackTMDeque :: TMDeque a -> STM (Maybe (Maybe a))+tryPopBackTMDeque deq = do+  back <- readTVar deq.back+  front <- readTVar deq.front+  if back == front+    then do+      closed <- readTVar deq.closed+      if closed+        then pure Nothing+        else pure (Just Nothing)+    else do+      capa <- readTVar deq.capacity+      UniqIx dest <- stateTVar deq.back \i ->+        let !j = i + 1+         in (UniqIx $ i `rem` capa, j)+      buf <- readTVar deq.ringBuffer+      e <- readArray buf dest+      pure (Just (Just e))++-- | Close the deque.  After this, all push operations will be ignored, and all pop operations will return @Nothing@ once the deque is empty.+closeTMDeque :: TMDeque a -> STM ()+closeTMDeque deq = writeTVar deq.closed True++-- | Check if the deque is closed.+isClosedTMDeque :: TMDeque a -> STM Bool+isClosedTMDeque deq = readTVar deq.closed++-- | IO variant of 'isClosedTMDeque'.+isClosedTMDequeIO :: TMDeque a -> IO Bool+isClosedTMDequeIO deq = readTVarIO deq.closed++-- | Check if the deque is empty.  Note that an open deque may become non-empty after this returns.+isEmptyTMDeque :: TMDeque a -> STM Bool+isEmptyTMDeque deq = (==) <$> readTVar deq.front <*> readTVar deq.back++-- | IO variant of 'countTMDeque'.+estimateSizeTMDequeIO :: TMDeque a -> IO Int+estimateSizeTMDequeIO deq =+  (-) <$> readTVarIO deq.front <*> readTVarIO deq.back
+ src/Control/Monad/Borrow/Pure.hs view
@@ -0,0 +1,453 @@+{-# LANGUAGE BlockArguments #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE DerivingVia #-}+{-# LANGUAGE ExplicitNamespaces #-}+{-# LANGUAGE ImpredicativeTypes #-}+{-# LANGUAGE PartialTypeSignatures #-}+{-# LANGUAGE QualifiedDo #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TypeAbstractions #-}+{-# LANGUAGE NoImplicitPrelude #-}+{-# OPTIONS_GHC -Wno-name-shadowing #-}++{- |+This module is meant to be the prelude module of /Pure Borrow/, a Rust-style borrow realization in Linear Haskell.+This module provides only the basic pieces of the API, and you may want to import other modules, e.g. "Control.Monad.Borrow.Pure.BO", "Data.Ref.Linear.Borrow", or "Data.Vector.Mutable.Linear.Borrow", for more utilities.+-}+module Control.Monad.Borrow.Pure (+  -- $header++  -- * Core 'BO' monad+  BO (),+  runBO,+  runBOLend,+  runBO_,+  srunBO,+  srunBO_,++  -- * Lifetimes and Subtyping+  -- $lifetimes++  -- ** Lifetime+  Lifetime,+  type (/\),+  type (<=) (),+  type (>=),+  type Static,+  neverEnds,++  -- ** Subtyping and upcasting+  upcast,+  type (<:),++  -- * Linearity witnesses+  -- $linearly+  Linearly,+  linearly,+  LinearOnly,+  withLinearly,+  askLinearly,+  asksLinearly,+  asksLinearlyM,++  -- * Parallel computation+  parBO,++  -- * Borrowing+  -- $borrow++  -- ** Central Borrow types+  Mut,+  Share,+  Lend,+  Borrow,+  Alias,++  -- ** Introduction form+  borrowM,+  borrowLinearlyM,+  share,++  -- ** Reborrowing and computation in sublifetime+  reborrowing',+  reborrowing,+  (<%~),+  reborrowing_,+  (<%=),+  sharing',+  sharing,+  (<$~),+  sharing_,+  (<$=),++  -- ** Finalization and reclamation+  After (..),+  reclaim',+  reclaim,+  pureAfter,+  End,++  -- ** In-place modification with mutable borrows+  modifyBO,+  modifyBO_,+  modifyLinearOnlyBO,+  modifyLinearOnlyBO_,++  -- ** Utility function to manipulate borrows+  joinMut,+  joinLend,+  coerceShare,++  -- ** Copying and Cloning+  -- $copy-and-clone+  Copyable (..),+  copyMut,+  Clone (..),++  -- ** Splitting aliases+  -- $splitting+  splitPair,+  splitEither,+  split,+  DistributesAlias (),+  GenericDistributesAlias,+  genericSplit,++  -- * Re-exporting Prelude.Linear classes+  Consumable (..),+  Dupable (..),+  dup,+  dup3,+  Movable (..),+  Ur (..),+) where++import Control.Monad.Borrow.Pure.BO+import Control.Monad.Borrow.Pure.Clone+import Control.Monad.Borrow.Pure.Copyable+import Data.Unrestricted.Linear (Consumable (..), Dupable (..), Movable (..), Ur (..), dup, dup3)++{- $setup+>>> :set -XBlockArguments -XLinearTypes -XNoImplicitPrelude -XImpredicativeTypes -XQualifiedDo+>>> :m -Prelude+>>> import Prelude.Linear+>>> import qualified Data.Vector.Mutable.Linear.Borrow as VL+>>> import Control.Syntax.DataFlow qualified as DataFlow+>>> import Control.Functor.Linear qualified as Control+-}++{- $header+= Pure Borrow: An Overview++This module provides the main API of /Pure Borrow/, the pure realization of Rust-style borrowing in Linear Haskell.++The core idea is that mutable resources are accessed through lifetime-indexed borrows:++    * 'Linearly' proves that we are in a context where linear resources can be allocated and used safely.+    * @'BO' α a@ is a computation that may use borrows valid during the lifetime @α@. It also provides pure API with the concurrency primitive.+    * @'Mut' α a@ is a mutable borrow of an @a@ valid during @α@.+    * @'Share' α a@ is an immutable borrow of an @a@ valid during @α@.+    * @'Lend' α a@ is the capability to recover the original @a@ after @α@ ends.+    * @'After' α a@ describes post-processing that runs after @α@ ends, such as reclaiming a 'Lend'.++== Examples++You need the following language extensions to use this module:++    * BlockArguments+    * LinearTypes+    * NoImplicitPrelude+    * ImpredicativeTypes+    * QualifiedDo++...and import these modules:++@+import Prelude.Linear+import Control.Monad.Borrow.Pure+import qualified Data.Vector.Mutable.Linear.Borrow as VL+import Control.Syntax.DataFlow qualified as DataFlow+import Control.Functor.Linear qualified as Control+@++The examples use qualified do-notation. @DataFlow.do@ is convenient for rebiding pure values, and @Control.do@ is the do-notation for linear functors and monads.++The following example initializes a mutable vector, modifies it coordinate-wise, and then reads one element and the final contents:++>>> :{+  example1 :: (Int, [Int])+  example1 = linearly \lin -> DataFlow.do+    (lin, lin') <- dup lin+    vec <- VL.fromList [0, 1, 2] lin+    runBO lin' Control.do+      (mvec, lend) <- borrowM vec+      mvec <- VL.modify 0 (+ 3) mvec+      mvec <- VL.modify 2 (+ 5) mvec+      mvec <- VL.modify 0 (* 4) mvec+      let !(Ur svec) = share mvec+      Ur n <- VL.copyAt 0 svec+      pureAfter (n, unur $ VL.toList (reclaim lend))+:}++>>> example1+(12,[12,1,7])++This just returns @(12, [12, 1, 7])@ as expected, which is not so surprising.+But what if you want to modify non-overlapping segments of the vectors /in-parallel/?+In particular, while you have to do two modifications to index @0@ sequentially, you can modify the segment containing original index @2@ in parallel with the first modification to index @0@.+This is where pure concurrency with 'parBO' comes in:++>>> :{+  example2 :: (Int, [Int])+  example2 = linearly \lin -> DataFlow.do+    (lin, lin') <- dup lin+    vec <- VL.fromList [0, 1, 2] lin+    runBO lin' Control.do+      (mvec, lend) <- borrowM vec+      let !(mvec1, mvec2) = VL.splitAt 1 mvec -- (*)+      (mvec, ()) <-+        parBO+          ( Control.do+              mvec1 <- VL.modify 0 (+ 3) mvec1+              VL.modify 0 (* 4) mvec1+          )+          (consume Control.<$> VL.modify 1 (+ 5) mvec2)+      let !(Ur svec) = share mvec+      Ur n <- VL.copyAt 0 svec+      pureAfter (n, unur $ VL.toList (reclaim lend))+:}++>>> example2+(12,[12,1,7])++The line after @(*)@ splits the mutable vector into two non-overlapping mutable borrows, which can be safely used in parallel with 'parBO'.+The left branch returns the modified first slice, while the right branch consumes its slice and returns @()@. The whole original vector is later recovered through @lend@.++Manual discarding of split resources becomes tedious quickly.+This is where the /borrow/-based /affine/ API helps: 'reborrowing' lets you work in a shorter lifetime without manually reclaiming the original borrow.++>>> :{+  example3 :: (Int, [Int])+  example3 = linearly \lin -> DataFlow.do+    (lin, lin') <- dup lin+    vec <- VL.fromList [0, 1, 2] lin+    runBO lin' Control.do+      (mvec, lend) <- borrowM vec+      -- (!)+      mvec <- reborrowing_ mvec \mvec -> Control.do+        let !(mvec1, mvec2) = VL.splitAt 1 mvec+        -- (!!)+        consume+          Control.<$> parBO+            ( Control.do+                mvec1 <- VL.modify 0 (+ 3) mvec1+                VL.modify 0 (* 4) mvec1+            )+            (VL.modify 1 (+ 5) mvec2)+      let !(Ur svec) = share mvec -- (!!!)+      Ur n <- VL.copyAt 0 svec+      pureAfter (n, unur $ VL.toList (reclaim lend))+:}++>>> example3+(12,[12,1,7])++The line after @(!)@ opens a new sublifetime with 'reborrowing_'.+Within this sublifetime, the new mutable borrow @mvec@ is divided into two pieces, and then both slices are modified in parallel after @(!!)@.+This time, the split @mvec1@ and @mvec2@ are 'consume'd after 'parBO' returns. Once the sublifetime ends, the original mutable borrow to the whole vector is recovered and used at @(!!!)@.++This way, you can treat and split mutable and immutable borrows freely without manually dropping or reuniting them into the original resources.+-}++{- $lifetimes+Lifetime is a key concept in borrowing.+You can understand it as a version of the thread parameter @s@ in @'Control.Monad.ST' s@, but refined with the subtyping relation t'(<=)' (or /outlives/-relation t'(>=)').++Every @'BO' α@ computation is parametrized with lifetime, and ordinary borrows, such as @'Mut' α a@ or @'Share' α a@, and lenders @'Lend' α a@ also have the lifetime for which they are valid.+To accommodate casting between different lifetimes, we also provide the 'upcast' operator that has a lifetime parameter according to the sublifetime relation.+The 'upcast' operator casts a given type along t'(<:)' relation, which extends t'(<=)' to the other types appropriately.++Any two lifetimes @α@ and @β@ have the /meet/ @α '/\' β@, which is the longest lifetime that is shorter than both @α@ and @β@; i.e. @α '/\' β@ is the most generic lifetime such that @α '/\' β <= α@ and @α '/\' β <= β@.+We use some tricks with '/\' to work around type-checking higher-level combinators.+For example, consider the type of 'srunBO_':++@+'srunBO_' :: (forall β. 'BO' (β '/\' α) a) %1 -> 'BO' α a+@++At first glance, the type @forall β. 'BO' (β '/\' α) a@ might look rather cryptic.+But essentially, the above type is morally equivalent to the following:++@+'srunBO_' :: (forall β \<= α. 'BO' β a) %1 -> 'BO' α a+@++That is, all 'srunBO_' does is open an ephemeral sublifetime @β <= α@ and run the computation inside it.+However, without involved hacking or type-checker plugins, the type system is not good at treating transitivity of subtyping relation.+By quantifying over all lifetimes and combining them with '/\', we can make the type-checker happy without losing generality.++So, if you see a pattern that binds other lifetimes with @forall@ and combines them with '/\', you can think of it as quantifying over a sublifetime of the current lifetime.+-}++{- $linearly++When you allocate mutable resources, you must ensure that they are used only /linearly/; i.e. they are used exactly once.+In Linear Haskell, we use /linear arrow/ @%1 ->@ to express this invariant.+More precisely, @a %1 -> b@ reads that /if the application of the function is consumed exactly once, then the argument is consumed exactly once/.+This definition poses a subtle problem: the resource is guaranteed to be used linearly only when the resource is bound under some linear arrow context.+Hence, we must know that we are under a linear context before allocating mutable references, otherwise the mutable state can leak outside.++The 'Linearly' token witnesses exactly this invariant.+The important point is that it can be introduced into the context only by 'linearly' combinator:++@+'linearly' :: 'Movable' a => ('Linearly' %1 -> a) %1 -> a+@++This assures that 'Linearly' can be used as a linearity witness when mutable resources are allocated.+You can duplicate a 'Linearly' token as many times as you want with 'dup' and drop it with 'consume'.++@+fromList :: [a] %1 -> 'Linearly' %1 -> 'Data.Vector.Mutable.Linear.Borrow.Vector' a+@++See [Linear Constraints: the Problem with Scopes](https://www.tweag.io/blog/2023-03-23-linear-constraints-linearly/) for more details.++Those mutable datatypes can only be introduced via a 'Linearly' witness, so they can be seen as carrying the 'Linearly' witness inside.+'LinearOnly' is a type class for such datatypes and we can use it to recover a 'Linearly' witness from such values.++@+'withLinearly' :: ('LinearOnly' a) => a %1 -> ('Linearly', a)+@++Further, running the 'BO' computation also requires 'Linearly':++@+runBO_ :: 'Linearly' %1 -> (forall α. 'BO' α a) %1 -> a+@++Hence, you can retrieve a 'Linearly' token inside 'BO' via 'askLinearly', 'asksLinearlyM', etc.+-}++{- $borrow+To treat a linear resource inside 'BO' monad, you have to borrow it first.+The most typical introduction form is 'borrowM':++@+'borrowM' :: a %1 -> 'BO' α ('Mut' α a, 'Lend' α a)+@++This borrows a linear resource into the same lifetime as the ambient 'BO', returning a 'Mut'able borrow and a 'Lend'er of the original resource.+Or, you can do the linear allocation of the resource and borrow it at the same time with 'borrowLinearlyM':++@+'borrowLinearlyM' :: (Linearly %1 -> a) %1 -> 'BO' α ('Mut' α a, 'Lend' α a)+@++In any case, the main computation with possible destructive updates is done on 'Mut'able borrows, and the original resource will be 'reclaim'ed from the 'Lend'er at the end of the lifetime @α@.+More precisely, @'Lend' α a@ must be processed in an appropriate @'After' α r@ value that is returned to 'runBO', 'srunBO', or the reborrowing operators described later.+@'After' α a@ is a kind of finalizer that will be run after the lifetime @α@ has 'End'ed, and it can be used to reclaim the original resource from a 'Lend'er and do further final computation such as conversion or consumption.++One can 'share' the 'Mut'able borrow into 'Share'd borrow:++@+'share' :: 'Mut' α a %1 -> 'Ur' ('Share' α a)+@++As 'Share' is an immutable borrow, it can be freely duplicated and dropped, as witnessed by the 'Ur' wrapper.+'Share'd borrows are always introduced nonlinearly, so that you can freely use them multiple times or drop them at any time.+Note that 'share' consumes the original 'Mut'. If you want to share the resource temporarily into a sublifetime and then continue mutating afterwards, you can use the 'sharing' combinator (and its variants 'sharing'' and 'sharing_'):++@+'sharing' ::+  forall α α' a r.+  'Mut' α a %1 ->+  (forall β. 'Share' (β '/\' α) a -> 'BO' (β '/\' α') r) %1 ->+  'BO' α' (r, 'Mut' α a)+@++Analogously, you can reborrow mutable borrows into sublifetimes using the 'reborrowing' combinator (and its variants 'reborrowing'' and 'reborrowing_').++@+'reborrowing' ::+  forall α α' a r.+  'Mut' α a %1 ->+  (forall β. 'Mut' (β '/\' α) a -> 'BO' (β '/\' α') r) %1 ->+  'BO' α' (r, 'Mut' α a)+@++There is an experimental interface abstracting the reborrowable borrows in "Control.Monad.Borrow.Pure.Experimental.Reborrowable".++== Borrow polymorphism++'Mut', 'Share', and 'Lend' are all specific instantiations of the 'Alias' type:++@+type 'Mut' α a = 'Borrow' 'Mut α a+type 'Share' α a = 'Borrow' 'Share α a+type 'Borrow' bk α a = 'Alias' ('Borrow bk) α a+type 'Lend' α a = 'Alias' 'Lend α a+@++Hence, if you see @'Borrow' bk α a@ in a function, it can be either 'Mut' or 'Share'. If you see @'Alias' ak α a@, it may also be a 'Lend'.++"Control.Monad.Borrow.Pure.Experimental.Borrows" provides an experimental API for treating a bundle of multiple borrows in the same lifetime at once.++== Which combinator should I use?++    * Use 'borrowM' to borrow an existing linear value inside 'BO'.+    * Use 'borrowLinearlyM' to allocate a linear value and immediately borrow it inside 'BO'.+    * Use 'share' to permanently turn a 'Mut' into an unrestricted 'Share'.+    * Use 'sharing' or 'sharing_' to share temporarily and then regain the original 'Mut'.+    * Use 'reborrowing' or 'reborrowing_' to create a shorter-lived 'Mut' and then regain the original 'Mut'.+    * Use 'reclaim' or 'reclaim'' to recover the original resource from a 'Lend' after the lifetime ends.+-}++{- $copy-and-clone++For some types, you can 'copy' them as the direct value out of a borrow:++@+'copy' :: 'Borrow' bk α a %1 -> a+@++Note that 'copy' consumes a borrow linearly.+For 'Share'd borrows it doesn't matter because they are always introduced nonlinearly.+But for 'Mut'able borrows, we cannot use a 'copy'ed value multiple times as 'Mut's are always bound linearly.+To alleviate this problem, we also provide 'copyMut' that wraps copied value inside 'Ur':++@+'copyMut' :: 'Mut' α a %1 -> 'Ur' a+@++Precisely, if the type @a@ does not contain any mutable or foreign resources, it can be safely 'Copyable' out of borrows.+Some examples are (but not limited to):++    * Primitive types, such as 'Int', 'Bool', etc.+    * Immutable data structures, such as lists, tuples of them, etc. (but not mutable vectors, arrays, etc.)++For possibly mutable types, you can still 'clone' them out of borrows linearly inside 'BO'-monad:++@+'clone' :: 'Clone' a => 'Share' α a %1 -> 'BO' α a+@++This includes, for example, 'Data.Ref.Linear.Ref' or 'Data.Vector.Mutable.Linear.Borrow.Vector'.+The fact that the 'clone'd value is only accessible inside 'BO' ensures that we cannot leak mutable states inside @a@ into /unrestricted/ contexts -- otherwise, we can introduce mutable values into unrestricted context via @'move' :: 'Share' α a -> 'Ur' ('Share' α a)@.+-}++{- $splitting++You can do case-splitting on 'Borrow's - for example:++@+'splitPair' :: 'Alias' ak α (a, b) %1 -> ('Alias' ak α a, 'Alias' ak α b)+'splitEither' :: 'Alias' ak α ('Either' a b) %1 -> 'Either' ('Alias' ak α a) ('Alias' ak α b)+@++For other datatypes, you can use 'split' to split general parametric types into borrows.+It is morally an instance method of the 'DistributesAlias' class, and you can derive it using @anyclass@ derivation together with the 'Generics.Linear.TH.deriveGenericAnd1' macro.++We also provide experimental splitting on record types in "Data.Record.Linear.Borrow.Experimental.PatternMatch" and "Data.Record.Linear.Borrow.Experimental.Split".+-}
+ src/Control/Monad/Borrow/Pure/Affine.hs view
@@ -0,0 +1,21 @@+{-# LANGUAGE ConstraintKinds #-}+{-# LANGUAGE DefaultSignatures #-}+{-# LANGUAGE DerivingVia #-}+{-# LANGUAGE PolyKinds #-}+{-# LANGUAGE StandaloneKindSignatures #-}++module Control.Monad.Borrow.Pure.Affine (+  -- * Affine Modality+  Affine (..),+  AsAffine (..),+  Aff,+  affu,+  unaff,+  pop,++  -- ** Linear Generics+  GenericAffine,+  GenericallyAffine (..),+) where++import Control.Monad.Borrow.Pure.Affine.Internal
+ src/Control/Monad/Borrow/Pure/Affine/Internal.hs view
@@ -0,0 +1,226 @@+{-# LANGUAGE BlockArguments #-}+{-# LANGUAGE ConstraintKinds #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE DefaultSignatures #-}+{-# LANGUAGE DerivingVia #-}+{-# LANGUAGE LambdaCase #-}+{-# LANGUAGE MagicHash #-}+{-# LANGUAGE PatternSynonyms #-}+{-# LANGUAGE PolyKinds #-}+{-# LANGUAGE StandaloneKindSignatures #-}+{-# LANGUAGE UnboxedTuples #-}+{-# LANGUAGE UndecidableInstances #-}+{-# LANGUAGE UnliftedNewtypes #-}+{-# OPTIONS_GHC -Wno-redundant-constraints #-}+{-# OPTIONS_HADDOCK hide #-}++module Control.Monad.Borrow.Pure.Affine.Internal (+  module Control.Monad.Borrow.Pure.Affine.Internal,+) where++import Data.Comonad.Linear qualified as Data+import Data.Functor.Linear qualified as Data+import Data.Int+import Data.Kind+import Data.Monoid qualified as Mon+import Data.Semigroup qualified as Sem+import Data.Unrestricted.Linear+import Data.Word+import GHC.Base+import Generics.Linear+import Prelude.Linear qualified as PL+import Unsafe.Linear qualified as Unsafe++data Aff a where+  UnsafeAff :: !a %One -> Aff a++unaff :: Aff a %1 -> a+unaff (UnsafeAff !a) = a+{-# INLINE unaff #-}++{- | You can bring unrestricted resources into 'Aff' context.++Note that, when you use 'aff' to bring a foreign resource (e.g. 'Foreign.Ptr'),+it is user's responsibility to ensure 'Forign.free' is called on the resource after the @'Aff' ('Foreign.Ptr' a)@ is popped.+-}+affu :: a -> Aff a+affu = UnsafeAff+{-# INLINE affu #-}++pop :: Aff a %1 -> ()+pop = Unsafe.toLinear (\(UnsafeAff _) -> ())+{-# INLINE pop #-}++instance Consumable (Aff a) where+  consume = pop+  {-# INLINE consume #-}++instance Data.Functor Aff where+  fmap f (UnsafeAff a) = UnsafeAff (f a)+  {-# INLINE fmap #-}++instance Data.Comonad Aff where+  extract (UnsafeAff a) = a+  {-# INLINE extract #-}++  duplicate (UnsafeAff a) = UnsafeAff (UnsafeAff a)+  {-# INLINE duplicate #-}++instance Data.ComonadApply Aff where+  (UnsafeAff f) <@> (UnsafeAff a) = UnsafeAff (f a)+  {-# INLINE (<@>) #-}++type Affine :: Type -> Constraint+class Affine a where+  aff :: a %1 -> Aff a++instance (Movable a) => Affine (AsMovable a) where+  aff (AsMovable a) = move a PL.& \(Ur x) -> UnsafeAff (AsMovable x)+  {-# INLINE aff #-}++deriving via AsMovable (Ur a) instance Affine (Ur a)++deriving via AsMovable Bool instance Affine Bool++deriving via AsMovable Char instance Affine Char++deriving via AsMovable Int instance Affine Int++deriving via AsMovable Int8 instance Affine Int8++deriving via AsMovable Int16 instance Affine Int16++deriving via AsMovable Int32 instance Affine Int32++deriving via AsMovable Int64 instance Affine Int64++deriving via AsMovable Word instance Affine Word++deriving via AsMovable Word8 instance Affine Word8++deriving via AsMovable Word16 instance Affine Word16++deriving via AsMovable Word32 instance Affine Word32++deriving via AsMovable Word64 instance Affine Word64++newtype AsAffine a = AsAffine a++instance (Affine a) => Consumable (AsAffine a) where+  consume (AsAffine a) = pop (aff a)+  {-# INLINE consume #-}++deriving newtype instance Affine Sem.Any++deriving newtype instance Affine Sem.All++deriving via GenericallyAffine (Maybe a) instance (Affine a) => Affine (Maybe a)++deriving via+  GenericallyAffine (Either a b)+  instance+    (Affine a, Affine b) => Affine (Either a b)++deriving via GenericallyAffine () instance Affine ()++deriving via+  GenericallyAffine (a, b)+  instance+    (Affine a, Affine b) => Affine (a, b)++deriving via+  GenericallyAffine (a, b, c)+  instance+    (Affine a, Affine b, Affine c) => Affine (a, b, c)++deriving via+  GenericallyAffine (a, b, c, d)+  instance+    (Affine a, Affine b, Affine c, Affine d) => Affine (a, b, c, d)++deriving via+  GenericallyAffine (a, b, c, d, e)+  instance+    (Affine a, Affine b, Affine c, Affine d, Affine e) => Affine (a, b, c, d, e)++deriving via GenericallyAffine (Sem.Sum a) instance (Affine a) => Affine (Sem.Sum a)++deriving via GenericallyAffine (Sem.Product a) instance (Affine a) => Affine (Sem.Product a)++deriving via GenericallyAffine (Sem.First a) instance (Affine a) => Affine (Sem.First a)++deriving via GenericallyAffine (Sem.Last a) instance (Affine a) => Affine (Sem.Last a)++deriving via GenericallyAffine (Sem.Dual a) instance (Affine a) => Affine (Sem.Dual a)++deriving via GenericallyAffine [a] instance (Affine a) => Affine [a]++deriving via (Maybe a) instance (Affine a) => Affine (Mon.First a)++deriving via (Maybe a) instance (Affine a) => Affine (Mon.Last a)++-- * Generics++{- | We need this instead of 'Generically' becuase+it gives a different 'Consumable' instance.+-}+newtype GenericallyAffine a = GenericallyAffine a++unGenericallyAffine :: GenericallyAffine a %1 -> a+unGenericallyAffine (GenericallyAffine a) = a++deriving via+  AsAffine (GenericallyAffine a)+  instance+    (GenericAffine a) => Consumable (GenericallyAffine a)++instance (GenericAffine a) => Affine (GenericallyAffine a) where+  aff = Data.fmap GenericallyAffine PL.. genericAff PL.. unGenericallyAffine+  {-# INLINE aff #-}++genericAff :: (GenericAffine a) => a %1 -> Aff a+genericAff a = to Data.<$> gaff (from a)++{- | A constraint synonym for types for which 'Affine' instance+can be safely derived via 'Generically'.+-}+class (Generic a, GAffine (Rep a)) => GenericAffine a++instance (Generic a, GAffine (Rep a)) => GenericAffine a++type GAffine :: (k -> Type) -> Constraint+class GAffine f where+  gaff :: f a %1 -> Aff (f a)++instance (Affine a) => GAffine (K1 i a) where+  gaff (K1 a) = K1 Data.<$> aff a+  {-# INLINE gaff #-}++instance (GAffine f, GAffine g) => GAffine (f :+: g) where+  gaff (L1 x) = L1 Data.<$> gaff x+  gaff (R1 y) = R1 Data.<$> gaff y+  {-# INLINE gaff #-}++instance (GAffine f, GAffine g) => GAffine (f :*: g) where+  gaff (x :*: y) = (:*:) Data.<$> gaff x Data.<@> gaff y+  {-# INLINE gaff #-}++instance GAffine (MP1 Many f) where+  gaff (MP1 x) = UnsafeAff (MP1 x)+  {-# INLINE gaff #-}++instance (GAffine f) => GAffine (MP1 One f) where+  gaff (MP1 x) = MP1 Data.<$> gaff x+  {-# INLINE gaff #-}++instance GAffine V1 where+  gaff = \case {}+  {-# INLINE gaff #-}++instance GAffine U1 where+  gaff U1 = UnsafeAff U1+  {-# INLINE gaff #-}++instance (GAffine f) => GAffine (M1 i c f) where+  gaff (M1 x) = M1 Data.<$> gaff x+  {-# INLINE gaff #-}
+ src/Control/Monad/Borrow/Pure/Affine/Unsafe.hs view
@@ -0,0 +1,17 @@+{- |+This module provides __unsafe__ internals of "Control.Monad.Borrow.Pure.Affine".+These are not meant to be used by end-users, so generally YOU SHOULD NOT import this module, and import "Control.Monad.Borrow.Pure.Affine" instead.++This module is meant for library authors who want to build a new API on top of Pure Borrow.+This module provides internals of 'BO' and 'Alias', which can break the soundness guarded by the role system.+We __STRONGLY__ recommend to you to import only the needed parts of the definitions, and not to import everything or qualified.+-}+module Control.Monad.Borrow.Pure.Affine.Unsafe (+  -- * Affine Modality+  unsafeAff,+) where++import Control.Monad.Borrow.Pure.Affine.Internal++unsafeAff :: a %1 -> Aff a+unsafeAff = UnsafeAff
+ src/Control/Monad/Borrow/Pure/BO.hs view
@@ -0,0 +1,372 @@+{-# LANGUAGE BlockArguments #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE DerivingVia #-}+{-# LANGUAGE ExplicitNamespaces #-}+{-# LANGUAGE ImpredicativeTypes #-}+{-# LANGUAGE PartialTypeSignatures #-}+{-# LANGUAGE QualifiedDo #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TypeAbstractions #-}+{-# LANGUAGE NoImplicitPrelude #-}+{-# OPTIONS_GHC -Wno-name-shadowing #-}++{- |+This module provides all the safe API of 'BO' monad, including the advanced, low-level combinators that are not meant to be used by most users.+For the conceptual overview, please refer to "Control.Monad.Borrow.Pure", which is the prelude of this package.+-}+module Control.Monad.Borrow.Pure.BO (+  -- $header++  -- * Core 'BO' monad+  BO (),+  execBO,+  runBO,+  runBOLend,+  runBO_,+  sexecBO,+  scope_,+  srunBO,+  srunBO_,+  askLinearly,+  asksLinearly,+  asksLinearlyM,+  evaluateBO,++  -- ** In-place modification with mutable borrows+  modifyBO,+  modifyBO_,+  modifyLinearOnlyBO,+  modifyLinearOnlyBO_,++  -- * Parallel computation+  parBO,++  -- * Borrowing+  Alias,+  AliasKind,+  BorrowKind,+  Borrow,+  Mut,+  Share,+  Lend,+  coerceShare,+  shareCoercion,+  borrowM,+  borrowLinearlyM,+  sharing',+  sharing,+  (<$~),+  sharing_,+  (<$=),+  reborrowing',+  reborrowing,+  (<%~),+  reborrowing_,+  (<%=),+  share,+  reclaim',+  reclaim,+  pureAfter,+  reborrow,+  joinMut,+  joinLend,++  -- *** Lower-level operators+  borrow,+  borrowLinearOnly,++  -- ** Splitting aliases+  DistributesAlias (),+  split,+  GenericDistributesAlias,+  genericSplit,+  splitPair,+  splitEither,++  -- ** Misc Utilities++  -- *** Manual lifetime reassociation+  assocRBO,+  assocLBO,+  assocBOEq,+  assocBorrowL,+  assocBorrowR,+  assocBorrowEq,+  assocLendL,+  assocLendR,+  assocLendEq,++  -- * Re-exports+  module Control.Monad.Borrow.Pure.Lifetime,+  module Control.Monad.Borrow.Pure.Lifetime.Token,+  module Data.Coerce.Directed,+) where++import Control.Functor.Linear qualified as Control+import Control.Monad.Borrow.Pure.BO.Internal+import Control.Monad.Borrow.Pure.Lifetime+import Control.Monad.Borrow.Pure.Lifetime.Token+import Control.Monad.Borrow.Pure.Utils (coerceLin)+import Control.Syntax.DataFlow qualified as DataFlow+import Data.Coerce (Coercible)+import Data.Coerce.Directed+import Data.Type.Coercion (Coercion (..))+import Prelude.Linear++{- |+Runs a 'BO' computation and returns the result of postprocessing 'After' the lifetime has ended.++See also: 'runBOLend' and 'runBO_'.+-}+runBO :: forall a. Linearly %1 -> (forall α. BO α (After α a)) %1 -> a+{-# INLINE runBO #-}+runBO lin bo =+  case newLifetime lin of+    MkSomeNow (now :: Now α) -> DataFlow.do+      (now, f) <- execBO @α @(After α a) bo now+      case endLifetime now of+        Ur end -> withEnd @α end f++-- | A variant of 'runBO' that returns the original rsource retained by the 'Lend'er+runBOLend :: Linearly %1 -> (forall α. BO α (Lend α a)) %1 -> a+{-# INLINE runBOLend #-}+runBOLend lin bo = runBO lin Control.do+  lend <- bo+  Control.pure (reclaim' lend)++-- | A variant of 'runBO' that returns the direct value of 'BO' computation.+runBO_ :: Linearly %1 -> (forall α. BO α a) %1 -> a+{-# INLINE runBO_ #-}+runBO_ lin bo = runBO lin Control.do+  a <- bo+  pureAfter a++-- | Flipped version of 'sexecBO'.+scope_ :: Now α %1 -> BO (α /\ β) a %1 -> BO β (Now α, a)+{-# INLINE scope_ #-}+scope_ = flip sexecBO++-- | A variant of 'borrow' that obtains 'Linearly' viar 'LinearOnly'.+borrowLinearOnly :: forall α a. (LinearOnly a) => a %1 -> (Mut α a, Lend α a)+borrowLinearOnly !a = case withLinearly a of+  (!lin, !a) -> borrow a lin++{- | A variant of 'sharing'' that discards the final result of the computation.+There is also a flipped infix version '(<$=)'.++See also: 'sharing'. For 'Mut'able borrows, see 'reborrowing_'.+-}+sharing_ ::+  forall α α' a r.+  (Consumable r) =>+  Mut α a %1 ->+  (forall β. Share (β /\ α) a -> BO (β /\ α') r) %1 ->+  BO α' (Mut α a)+{-# INLINE sharing_ #-}+sharing_ v k = uncurry lseq Control.<$> sharing v k++-- | Flipped infix version of 'sharing_', smoewhat analgous to '(Control.<$>)' and @(<%=)@ in @lens@ package.+(<$=) ::+  (forall β. Share (β /\ α) a -> BO (β /\ α') ()) %1 ->+  Mut α a %1 ->+  BO α' (Mut α a)+{-# INLINE (<$=) #-}+(<$=) = flip sharing_++{- | A variant of 'sharing'' that returns the direct value of the computation on the shared borrow.+There is also a flipped infix version '(<$~)'.++See also: 'sharing_'. For 'Mut'able borrows, see 'reborrowing'.+-}+sharing ::+  forall α α' a r.+  Mut α a %1 ->+  (forall β. Share (β /\ α) a -> BO (β /\ α') r) %1 ->+  BO α' (r, Mut α a)+{-# INLINE sharing #-}+sharing v k = sharing' v (\mut -> Control.pure Control.<$> k mut)++-- | Flipped infix version of 'sharing', smoewhat analgous to '(Control.<$>)' and @(<%~)@ in @lens@ package.+(<$~) ::+  (forall β. Share (β /\ α) a -> BO (β /\ α') r) %1 ->+  Mut α a %1 ->+  BO α' (r, Mut α a)+{-# INLINE (<$~) #-}+(<$~) = flip sharing++infix 4 <$~++{- | Executes an operation on 'Share'd borrow in sub lifetime.+You may need @-XImpredicativeTypes@ extension to use this function.++See also: 'sharing' and 'sharing_'. For 'Mut'able borrows, see 'reborrowing''.+-}+sharing' ::+  Mut α a %1 ->+  (forall β. Share (β /\ α) a -> BO (β /\ α') (After β r)) %1 ->+  BO α' (r, Mut α a)+{-# INLINE sharing' #-}+sharing' v k = DataFlow.do+  srunBO DataFlow.do+    (v, lend) <- reborrow v+    share v & \(Ur v) -> Control.do+      k v Control.<&> \v -> (,) Control.<$> v Control.<*> upcast (reclaim' lend)++{- | Executes an operation on 'Mut'able borrow in sub lifetime.+You may need @-XImpredicativeTypes@ extension to use this function.++See also: 'reborrowing', and 'reborrowing_'. For 'Share'd borrows, see 'sharing', 'sharing'', and 'sharing_'.+-}+reborrowing' ::+  Mut α a %1 ->+  (forall β. Mut (β /\ α) a %1 -> BO (β /\ α') (After β r)) %1 ->+  BO α' (r, Mut α a)+reborrowing' v k = srunBO DataFlow.do+  (v, lend) <- reborrow v+  Control.do+    v <- k v+    Control.pure $ (,) Control.<$> v Control.<*> upcast (reclaim' lend)++{- | A variant of 'reborrowing'' that returns the direct value of the operation on the reborrowed mutable borrow.+There is also a flipped infix version '(<%~)'.++See also: 'reborrowing_' and 'sharing'.+-}+reborrowing ::+  Mut α a %1 ->+  (forall β. Mut (β /\ α) a %1 -> BO (β /\ α') r) %1 ->+  BO α' (r, Mut α a)+reborrowing mutα k = reborrowing' mutα (\mut -> Control.pure Control.<$> k mut)++-- | Flipped infix version of 'reborrowing', smoewhat analgous to '(Control.<$>)' and @(<%~)@ in @lens@ package.+(<%~) ::+  (forall β. Mut (β /\ α) a %1 -> BO (β /\ α') r) %1 ->+  Mut α a %1 ->+  BO α' (r, Mut α a)+{-# INLINE (<%~) #-}+(<%~) = flip reborrowing++infix 4 <%~++{- |+A variant of 'reborrowing'' that discards the final result of the computation.+There is also a flipped infix version '(<%=)'.++See also: 'reborrowing' and 'sharing_'.+-}+reborrowing_ ::+  (Consumable r) =>+  Mut α a %1 ->+  (forall β. Mut (β /\ α) a %1 -> BO (β /\ α') r) %1 ->+  BO α' (Mut α a)+reborrowing_ mutα k = reborrowing mutα (Control.fmap consume . k) Control.<&> \((), a) -> a++-- | Flipped infix version of 'reborrowing_', smoewhat analgous to '(Control.<$>)' and @(<%=)@ in @lens@ package.+(<%=) ::+  (forall β. Mut (β /\ α) a %1 -> BO (β /\ α') ()) %1 ->+  Mut α a %1 ->+  BO α' (Mut α a)+{-# INLINE (<%=) #-}+(<%=) = flip reborrowing_++infix 4 <%=++-- | Modifies linear resources in-place, together with results.+modifyBO ::+  a %1 ->+  Linearly %1 ->+  (forall α. Mut α a %1 -> BO α r) %1 ->+  (r, a)+modifyBO v lin k = DataFlow.do+  (lin, lin') <- dup lin+  runBO lin Control.do+    let %1 !(mut, lend) = borrow v lin'+    r <- k mut+    Control.pure $ (r,) Control.<$> reclaim' lend++-- | Modifies linear resources in-place, without results.+modifyBO_ ::+  a %1 ->+  Linearly %1 ->+  (forall α. Mut α a %1 -> BO α ()) %1 ->+  a+modifyBO_ v lin k = DataFlow.do+  (lin, lin') <- dup lin+  runBO lin Control.do+    let %1 !(mut, lend) = borrow v lin'+    k mut+    Control.pure $ reclaim' lend++-- | Modifies linear resources in-place, together with results.+modifyLinearOnlyBO ::+  (LinearOnly a) =>+  a %1 ->+  (forall α. Mut α a %1 -> BO α r) %1 ->+  (r, a)+modifyLinearOnlyBO v k = DataFlow.do+  (lin, v) <- withLinearly v+  runBO lin Control.do+    let %1 !(mut, lend) = borrowLinearOnly v+    !r <- k mut+    Control.pure $ (r,) Control.<$> reclaim' lend++-- | Modifies linear resources in-place, together with results.+modifyLinearOnlyBO_ ::+  (LinearOnly a) =>+  a %1 ->+  (forall α. Mut α a %1 -> BO α ()) %1 ->+  a+modifyLinearOnlyBO_ v k = DataFlow.do+  (lin, v) <- withLinearly v+  runBO lin Control.do+    let %1 !(mut, lend) = borrowLinearOnly v+    k mut+    Control.pure (reclaim' lend)++asksLinearly :: (Linearly %1 -> r) %1 -> BO α r+{-# INLINE asksLinearly #-}+asksLinearly k = asksLinearlyM $ Control.pure . k++pureAfter :: ((End α) => a) %1 -> BO α (After α a)+{-# INLINE pureAfter #-}+pureAfter a = Control.pure (After a)++coerceShare :: forall b α a. (Coercible a b) => Share α a %1 -> Share α b+{-# INLINE coerceShare #-}+coerceShare = coerceLin++shareCoercion :: forall a b α. (Coercible a b) => Coercion (Share α a) (Share α b)+{-# INLINE shareCoercion #-}+shareCoercion = Coercion++{- |+Borrow a resource linearly for the same lifetime as the ambient 'BO' computation.+Returns the pair of the mutable borrow to the resource, and 'Lend'er to be invoked later to 'reclaim' the resource at the 'End' of the lifetime.++See also 'borrowLinearlyM'.++If you want to borrow a resource indepdendent of the ambient lifetime, you can use 'borrow' instead.+-}+borrowM :: a %1 -> BO α (Mut α a, Lend α a)+{-# INLINE borrowM #-}+borrowM !a = asksLinearly \lin -> borrow a lin++-- | A variant of 'borrowM' that does linear allocation first.+borrowLinearlyM :: (Linearly %1 -> a) %1 -> BO α (Mut α a, Lend α a)+{-# INLINE borrowLinearlyM #-}+borrowLinearlyM k = asksLinearlyM $ borrowM . k++-- | Runs a 'BO' computation within the ephemeral sublifetime and returns the result.+srunBO :: (forall α. BO (α /\ β) (After α a)) %1 -> BO β a+{-# INLINE srunBO #-}+srunBO bo = asksLinearlyM \lin ->+  newLifetime' lin \now -> Control.do+    (now, f) <- sexecBO bo now+    Ur end <- Control.pure (endLifetime now)+    Control.pure (withEnd end f)++-- | A variant of 'srunBO' that returns the direct value of 'BO' computation.+srunBO_ :: (forall α. BO (α /\ β) a) %1 -> BO β a+{-# INLINE srunBO_ #-}+srunBO_ k = srunBO Control.do a <- k; Control.pure $ After a
+ src/Control/Monad/Borrow/Pure/BO/Internal.hs view
@@ -0,0 +1,524 @@+{-# LANGUAGE BlockArguments #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE DefaultSignatures #-}+{-# LANGUAGE DeriveAnyClass #-}+{-# LANGUAGE DerivingVia #-}+{-# LANGUAGE ImpredicativeTypes #-}+{-# LANGUAGE LambdaCase #-}+{-# LANGUAGE MagicHash #-}+{-# LANGUAGE PartialTypeSignatures #-}+{-# LANGUAGE PatternSynonyms #-}+{-# LANGUAGE QualifiedDo #-}+{-# LANGUAGE QuantifiedConstraints #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE RoleAnnotations #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE StandaloneKindSignatures #-}+{-# LANGUAGE TypeData #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE UnboxedTuples #-}+{-# LANGUAGE UndecidableInstances #-}+{-# LANGUAGE UnliftedNewtypes #-}+{-# LANGUAGE ViewPatterns #-}+{-# LANGUAGE NoImplicitPrelude #-}+{-# OPTIONS_GHC -Wno-name-shadowing #-}+{-# OPTIONS_GHC -Wno-partial-type-signatures #-}+{-# OPTIONS_GHC -Wno-redundant-constraints #-}+{-# OPTIONS_HADDOCK hide #-}++module Control.Monad.Borrow.Pure.BO.Internal (+  module Control.Monad.Borrow.Pure.BO.Internal,+) where++import Control.Exception qualified as SystemIO+import Control.Functor.Linear qualified as Control+import Control.Monad qualified as NonLinear+import Control.Monad.Borrow.Pure.Affine.Internal+import Control.Monad.Borrow.Pure.Lifetime+import Control.Monad.Borrow.Pure.Lifetime.Token+import Control.Monad.Borrow.Pure.Lifetime.Token.Internal+import Control.Monad.Borrow.Pure.Utils (coerceLin)+import Control.Monad.ST.Strict (ST)+import Control.Syntax.DataFlow qualified as DataFlow+import Data.Coerce qualified+import Data.Coerce.Directed.Unsafe+import Data.Functor.Identity (Identity)+import Data.Functor.Linear qualified as Data+import Data.Kind (Type)+import Data.Monoid qualified as Mon+import Data.Ord qualified as Ord+import Data.Semigroup qualified as Sem+import Data.Tuple (Solo (..))+import Data.Type.Equality ((:~:) (Refl))+import GHC.Base (TYPE)+import GHC.Base qualified as GHC+import GHC.Exts (State#, runRW#)+import GHC.ST qualified as ST+import GHC.TypeError (ErrorMessage (..))+import Generics.Linear+import Prelude.Linear+import Prelude.Linear qualified as PL+import Prelude.Linear.Unsatisfiable (Unsatisfiable, unsatisfiable)+import System.IO.Linear qualified as L+import Unsafe.Coerce (unsafeCoerce#)+import Unsafe.Linear qualified as Unsafe++-- NOTE: NOINLINE here is REALLY important, otherwise GHC will inline 'UnsafeLinearly' and common subexpression elimination+-- causes severe soundness bug that the same expression reuses the same+-- linear resource and sometimes SEGV.+askLinearly :: BO α Linearly+{-# NOINLINE askLinearly #-}+askLinearly = GHC.noinline $ Control.pure UnsafeLinearly++asksLinearlyM :: (Linearly %1 -> BO α r) %1 -> BO α r+{-# INLINE asksLinearlyM #-}+asksLinearlyM k = Control.do+  lin <- askLinearly+  !a <- k lin+  Control.pure a++-- NOTE: We want to use @TypeData@ extension for 'ForBO', but it makes Haddock panic!++type ForBO :: Lifetime -> Type+data ForBO α++{- | Computation returning @a@ that can be performed only during the lifetime @α@.+     Internally it is a linear ST monad.+-}+newtype BO α a = BO (State# (ForBO α) %1 -> (# State# (ForBO α), a #))++instance (Semigroup w) => Semigroup (BO α w) where+  (<>) = Control.liftA2 (<>)+  {-# INLINE (<>) #-}++instance (Monoid w) => Monoid (BO α w) where+  mempty = Control.pure mempty+  {-# INLINE mempty #-}++unsafeUnBO :: BO α a %1 -> State# (ForBO α) %1 -> (# State# (ForBO α), a #)+{-# INLINE unsafeUnBO #-}+unsafeUnBO (BO f) = f++assocRBO :: BO ((α /\ β) /\ γ) a %1 -> BO (α /\ (β /\ γ)) a+{-# INLINE assocRBO #-}+assocRBO = unsafeCastBO++assocLBO :: BO (α /\ (β /\ γ)) a %1 -> BO ((α /\ β) /\ γ) a+{-# INLINE assocLBO #-}+assocLBO = unsafeCastBO++assocBOEq :: forall α β γ a. BO ((α /\ β) /\ γ) a :~: BO (α /\ (β /\ γ)) a+{-# INLINE assocBOEq #-}+assocBOEq = Unsafe.coerce $ Refl @(BO (α /\ β /\ γ) a)++instance Data.Functor (BO α) where+  fmap f (BO g) = BO \s -> case g s of+    (# s', a #) -> (# s', f a #)+  {-# INLINE fmap #-}++instance Control.Functor (BO α) where+  fmap f (BO g) = BO \s -> case g s of+    (# s', a #) -> (# s', f a #)+  {-# INLINE fmap #-}++instance Data.Applicative (BO α) where+  pure a = Control.pure a+  {-# INLINE pure #-}++  (<*>) = \f g -> f Control.<*> g+  {-# INLINE (<*>) #-}++instance Control.Applicative (BO α) where+  pure a = BO \s -> (# s, a #)+  {-# INLINE pure #-}++  BO f <*> BO g = BO \s -> case f s of+    (# s', h #) -> case g s' of+      (# s'', a #) -> (# s'', h a #)+  {-# INLINE (<*>) #-}++instance Control.Monad (BO α) where+  BO fa >>= f = BO \s -> case fa s of+    (# s', a #) -> (f a) PL.& \(BO g) -> g s'+  {-# INLINE (>>=) #-}++-- | Unsafely converts a 'BO' computation to linear 'L.IO'.+unsafeBOToLinIO :: BO α a %1 -> L.IO a+{-# INLINE unsafeBOToLinIO #-}+unsafeBOToLinIO (BO f) = L.IO (Unsafe.coerce f)++{- |+Unsafely performs a linear 'L.IO' computation in 'BO' monad.++This is really, really unsafe. If you don't know what you are doing,+you MUST NOT use this function, otherwise you can break purity in a hard way.+-}+unsafeLinIOToBO :: L.IO a %1 -> BO α a+{-# INLINE unsafeLinIOToBO #-}+unsafeLinIOToBO (L.IO f) = BO (Unsafe.coerce f)++runBO# :: forall {rep} α (o :: TYPE rep). (State# (ForBO α) %1 -> o) %1 -> o+{-# INLINE runBO# #-}+runBO# = Unsafe.toLinear \f -> runRW# \s ->+  f (unsafeCoerce# s)++execBO :: BO α a %1 -> Now α %1 -> (Now α, a)+{-# INLINE execBO #-}+execBO (BO f) !now =+  case runBO# f of+    (# s, !a #) -> dropState# s `PL.lseq` (now, a)++dropState# :: State# a %1 -> ()+{-# INLINE dropState# #-}+dropState# = Unsafe.toLinear \ !_ -> ()++-- | See also 'Control.Monad.Borrow.Pure.scope'.+sexecBO :: BO (α /\ β) a %1 -> Now α %1 -> BO β (Now α, a)+{-# INLINE sexecBO #-}+sexecBO f now = unsafeCastBO ((now,) PL.. Unsafe.toLinear (\ !a -> a) Control.<$> f)++{- |+Coerces lifetime in 'BO' computation usafely and brutally.++This is really, really unsafe. If you don't know what you are doing,+you MUST NOT use this function, otherwise you will break the soundness of the type system.+-}+unsafeCastBO :: BO α a %1 -> BO β a+{-# INLINE unsafeCastBO #-}+unsafeCastBO = Unsafe.coerce++-- | Unsafely peforms a 'ST' computation in 'BO' monad.+unsafeSTToBO :: ST s a %1 -> BO α a+{-# INLINE unsafeSTToBO #-}+unsafeSTToBO (ST.ST f) = BO (Unsafe.coerce f)++{- |+Unsafely peforms a 'BO' computation in 'ST' monad.++This is really unsafe. If you don't know what you are doing, you MUST NOT use this function, otherwise you can break purity in a hard way.+-}+unsafeBOToST :: BO α a %1 -> ST s a+{-# INLINE unsafeBOToST #-}+unsafeBOToST (BO f) = ST.ST (Unsafe.coerce f)++{- |+Unsafely performs a standard, non-linear 'IO' computation in 'BO' monad.++This is really, really unsafe. If you don't know what you are doing,+you MUST NOT use this function, otherwise you can break purity in a hard way.+-}+unsafeSystemIOToBO :: IO a %1 -> BO α a+{-# INLINE unsafeSystemIOToBO #-}+unsafeSystemIOToBO (GHC.IO a) = BO (Unsafe.coerce a)++-- | Unsafely performs a 'BO' in the standard, non-linear 'IO' monad.+unsafeBOToSystemIO :: BO α a %1 -> IO a+{-# INLINE unsafeBOToSystemIO #-}+unsafeBOToSystemIO (BO f) = GHC.IO (Unsafe.coerce f)++unsafePerformEvaluateUndupableBO :: BO α a %1 -> a+unsafePerformEvaluateUndupableBO (BO f) = runBO# \s ->+  case Unsafe.toLinear GHC.noDuplicate# s of+    s -> case f s of+      (# s, !a #) -> dropState# s `PL.lseq` a++-- | Run two computations in parallel, returning their results as a tuple.+parBO :: BO α a %1 -> BO α b %1 -> BO α (a, b)+parBO = Unsafe.toLinear2 \a b ->+  BO $+    Unsafe.toLinear \s ->+      case Unsafe.toLinear2 GHC.spark# (case unsafeUnBO a (GHC.noDuplicate# s) of (# _, a #) -> GHC.lazy a) s of+        (# _, a #) ->+          case Unsafe.toLinear2 GHC.spark# (case unsafeUnBO b (GHC.noDuplicate# s) of (# _, b #) -> GHC.lazy b) s of+            (# _, b #) ->+              case Unsafe.toLinear2 GHC.seq# a s of+                (# s, !a #) -> case Unsafe.toLinear2 GHC.seq# b s of+                  (# s, !b #) -> (# s, (a, b) #)++evaluateBO :: a %1 -> BO α a+{-# INLINE evaluateBO #-}+evaluateBO a = unsafeSystemIOToBO (Unsafe.toLinear SystemIO.evaluate a)++-- | Alias of kind 'ak' to a resource of type 'a'.+type Alias :: AliasKind -> Lifetime -> Type -> Type+newtype Alias ak α a = UnsafeAlias a++unsafeUnalias :: Alias ak α a %1 -> a+unsafeUnalias (UnsafeAlias x) = x++type role Alias nominal nominal representational++-- | Alias kind.+data AliasKind+  = -- | Borrower.+    Borrow BorrowKind+  | -- | Lender.+    Lend++-- | Borrower kind.+data BorrowKind+  = -- | Mutable.+    Mut+  | -- | Shared.+    Share++-- | Borrower of kind @bk@ that is active during the lifetime @α@.+type Borrow :: BorrowKind -> Lifetime -> Type -> Type+type Borrow bk = Alias ('Borrow bk)++-- | Mutable borrower, which is affine and can update the data.+type Mut :: Lifetime -> Type -> Type+type Mut = Borrow 'Mut++assocBorrowR ::+  Borrow bk ((α /\ β) /\ γ) a %1 ->+  Borrow bk (α /\ (β /\ γ)) a+{-# INLINE assocBorrowR #-}+assocBorrowR = coerceLin++assocBorrowL ::+  Borrow bk (α /\ (β /\ γ)) a %1 ->+  Borrow bk ((α /\ β) /\ γ) a+{-# INLINE assocBorrowL #-}+assocBorrowL = coerceLin++assocBorrowEq ::+  forall bk α β γ a.+  (Borrow bk ((α /\ β) /\ γ) a) :~: (Borrow bk (α /\ (β /\ γ)) a)+{-# INLINE assocBorrowEq #-}+assocBorrowEq = Unsafe.coerce $ Refl @(Borrow bk (α /\ β /\ γ) a)++assocLendR ::+  Lend ((α /\ β) /\ γ) a %1 ->+  Lend (α /\ (β /\ γ)) a+{-# INLINE assocLendR #-}+assocLendR = coerceLin++assocLendL ::+  Lend (α /\ (β /\ γ)) a %1 ->+  Lend ((α /\ β) /\ γ) a+{-# INLINE assocLendL #-}+assocLendL = coerceLin++assocLendEq :: forall α β γ a. (Lend ((α /\ β) /\ γ) a) :~: (Lend (α /\ (β /\ γ)) a)+{-# INLINE assocLendEq #-}+assocLendEq = Unsafe.coerce $ Refl @(Lend (α /\ β /\ γ) a)++instance (bk ~ 'Mut) => LinearOnly (Borrow bk α a) where+  linearOnly = UnsafeLinearOnly++deriving via AsAffine (Borrow bk α a) instance Consumable (Borrow bk α a)++-- | Shared borrower, which is unrestricted but usually can only read from the data.+type Share :: Lifetime -> Type -> Type+type Share = Borrow 'Share++instance Affine (Borrow bk α a) where+  aff = UnsafeAff+  {-# INLINE aff #-}++instance (k ~ 'Borrow 'Share) => Dupable (Alias k α a) where+  dup2 = Unsafe.toLinear $ NonLinear.join (,)+  {-# INLINE dup2 #-}++instance (k ~ 'Borrow 'Share) => Movable (Alias k α a) where+  move = Unsafe.toLinear Ur+  {-# INLINE move #-}++instance (α >= β, a <: b) => BO α a <: BO β b where+  subtype = UnsafeSubtype++instance (α >= β, a <: b, b <: a) => Mut α a <: Mut β b where+  subtype = UnsafeSubtype++instance (α >= β, a <: b) => Share α a <: Share β b where+  subtype = UnsafeSubtype++-- | Lender, which can retrieve the lifetime at the lifetime @α@.+type Lend :: Lifetime -> Type -> Type+type Lend = Alias 'Lend++instance (α <= β, a <: b) => Lend α a <: Lend β b where+  subtype = UnsafeSubtype++{- |+Borrow a resource linearly and obtain the mutable borrow to it and 'Lend' witness to 'reclaim the resource to lend at the 'End' of the lifetime.++For typical usage, you should use 'Control.Monad.Borrow.Pure.borrowM' to avoid type ambiguity.+-}+borrow :: forall α a. a %1 -> Linearly %1 -> (Mut α a, Lend α a)+borrow = Unsafe.toLinear2 \ !a !_ ->+  (UnsafeAlias a, UnsafeAlias a)++-- | Shares a mutable borrow, invalidating the original one.+share :: Borrow k α a %1 -> Ur (Share α a)+share = Unsafe.toLinear \(UnsafeAlias !a) -> Ur (UnsafeAlias a)++-- | Reclaims a 'borrow'ed resource at the 'End' of lifetime @α'.+reclaim' :: Lend α a %1 -> After α a+reclaim' l = After (reclaim l)++-- | Reclaims a 'borrow'ed resource at the 'End' of lifetime @α'.+reclaim :: (End α) => Lend α a %1 -> a+reclaim = \(UnsafeAlias !a) -> a++-- | Reborrow a mutable borrow into a sublifetime.+reborrow :: forall β α a. (α >= β) => Mut α a %1 -> (Mut β a, Lend β (Mut α a))+reborrow = Unsafe.toLinear \ !mutA ->+  (Data.Coerce.coerce mutA, Data.Coerce.coerce mutA)++-- | Collapse a borrower to a mutable borrower.+joinMut :: Borrow bk α (Mut β a) %1 -> Borrow bk (α /\ β) a+joinMut = coerceLin++joinLend :: Lend α (Lend α a) %1 -> Lend α a+joinLend = coerceLin++-- | Distribute an alias over a functor.+class DistributesAlias f where+  split_ :: Alias ak α (f x) %1 -> f (Alias ak α x)+  default split_ ::+    (GenericDistributesAlias f) =>+    Alias ak α (f x) %1 -> f (Alias ak α x)+  split_ = genericSplit++split ::+  forall f x ak α.+  (DistributesAlias f) =>+  Alias ak α (f x) %1 -> f (Alias ak α x)+{-# INLINE [1] split #-}+split = split_++deriving anyclass instance DistributesAlias Identity++deriving anyclass instance DistributesAlias []++deriving anyclass instance DistributesAlias Maybe++deriving anyclass instance DistributesAlias Solo++deriving anyclass instance DistributesAlias Ord.Down++deriving anyclass instance DistributesAlias Sem.Dual++deriving anyclass instance DistributesAlias Sem.Max++deriving anyclass instance DistributesAlias Sem.Min++deriving anyclass instance DistributesAlias Sem.First++deriving anyclass instance DistributesAlias Sem.Last++deriving anyclass instance DistributesAlias Mon.First++deriving anyclass instance DistributesAlias Mon.Last++splitPair :: Alias ak α (a, b) %1 -> (Alias ak α a, Alias ak α b)+{-# INLINE splitPair #-}+splitPair = coerceLin++splitEither :: Alias ak α (Either a b) %1 -> Either (Alias ak α a) (Alias ak α b)+{-# INLINE splitEither #-}+splitEither = coerceLin++instance (Unsatisfiable ('Text "Use splitEither directly!")) => DistributesAlias (Either e) where+  {-# INLINE split_ #-}+  split_ = unsatisfiable++instance (Unsatisfiable ('Text "Use splitPair instead!")) => DistributesAlias ((,) a) where+  {-# INLINE split_ #-}+  split_ = unsatisfiable++type GenericDistributesAlias f = (Generic1 f, GDistributeAlias (Rep1 f))++genericSplit ::+  forall f x ak α.+  (GenericDistributesAlias f) =>+  Alias ak α (f x) %1 -> f (Alias ak α x)+{-# INLINE genericSplit #-}+genericSplit =+  to1+    . gdistributeAlias @(Rep1 f)+    . unsafeMapAlias from1++unsafeMapAlias :: (a %1 -> b) %1 -> Alias ak α a %1 -> Alias ak α b+{-# INLINE unsafeMapAlias #-}+unsafeMapAlias f = coerceLin (\x -> let !y = f x in y)++instance (GenericDistributesAlias f) => DistributesAlias (Generically1 f) where+  {-# INLINE split_ #-}+  split_ = Generically1 . genericSplit . unsafeMapAlias \(Generically1 f) -> f++class GDistributeAlias f where+  gdistributeAlias :: Alias ak α (f x) %1 -> f (Alias ak α x)++instance+  ( GDistributeAlias f+  , GDistributeAlias g+  ) =>+  GDistributeAlias (f :*: g)+  where+  {-# INLINE gdistributeAlias #-}+  gdistributeAlias !(UnsafeAlias !(f :*: g)) =+    DataFlow.do+      !f <- gdistributeAlias $ UnsafeAlias f+      !g <- gdistributeAlias $ UnsafeAlias g+      f :*: g++instance+  ( GDistributeAlias f+  , GDistributeAlias g+  ) =>+  GDistributeAlias (f :+: g)+  where+  {-# INLINE gdistributeAlias #-}+  gdistributeAlias (UnsafeAlias x) = case x of+    L1 !l -> L1 (gdistributeAlias (UnsafeAlias l))+    R1 !r -> R1 (gdistributeAlias (UnsafeAlias r))++instance+  (Unsatisfiable (Text "Nonlinear fields cannot distribute borrows!")) =>+  GDistributeAlias (MP1 GHC.Many f)+  where+  {-# INLINE gdistributeAlias #-}+  gdistributeAlias = unsatisfiable++instance (GDistributeAlias f) => GDistributeAlias (MP1 GHC.One f) where+  {-# INLINE gdistributeAlias #-}+  gdistributeAlias =+    MP1 . gdistributeAlias . UnsafeAlias . unMP1 . unsafeUnalias++instance (GDistributeAlias f) => GDistributeAlias (M1 i c f) where+  {-# INLINE gdistributeAlias #-}+  gdistributeAlias (UnsafeAlias (M1 x)) =+    M1 $ gdistributeAlias $ UnsafeAlias x++instance DistributesAlias Par1 where+  {-# INLINE split_ #-}+  split_ (UnsafeAlias (Par1 a)) = Par1 (UnsafeAlias a)++instance+  ( DistributesAlias f+  , DistributesAlias g+  , Data.Functor f+  ) =>+  GDistributeAlias (f :.: g)+  where+  {-# INLINE gdistributeAlias #-}+  gdistributeAlias (UnsafeAlias (Comp1 !fg)) =+    Comp1 $ Data.fmap split_ $ split_ $ UnsafeAlias fg++instance GDistributeAlias Par1 where+  {-# INLINE gdistributeAlias #-}+  gdistributeAlias (UnsafeAlias (Par1 !a)) = Par1 (UnsafeAlias a)++instance+  (Unsatisfiable (Text "A type containing non-parametric field with type `" :<>: ShowType c :<>: Text "', which cannot be safely splitted!")) =>+  GDistributeAlias (K1 i c)+  where+  {-# INLINE gdistributeAlias #-}+  gdistributeAlias = unsatisfiable++instance GDistributeAlias U1 where+  gdistributeAlias = coerceLin+  {-# INLINE gdistributeAlias #-}
+ src/Control/Monad/Borrow/Pure/BO/Unsafe.hs view
@@ -0,0 +1,37 @@+{-# LANGUAGE BlockArguments #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE DerivingVia #-}+{-# LANGUAGE ImpredicativeTypes #-}+{-# LANGUAGE PartialTypeSignatures #-}+{-# LANGUAGE QualifiedDo #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE NoImplicitPrelude #-}+{-# OPTIONS_GHC -Wno-name-shadowing #-}++{- |+This module provides __unsafe__ internals of "Control.Monad.Borrow.Pure".+These are not meant to be used by end-users, so generally YOU SHOULD NOT import this module, and import "Control.Monad.Borrow.Pure" instead.++This module is meant for library authors who want to build a new API on top of Pure Borrow.+This module provides internals of 'BO' and 'Alias', which can break the soundness guarded by the role system.+We __STRONGLY__ recommend to you to import only the needed parts of the definitions, and not to import everything or qualified.+-}+module Control.Monad.Borrow.Pure.BO.Unsafe (+  -- * Internal definitions and utilities of core types.+  BO (..),+  Alias (..),+  unsafeUnalias,+  unsafeMapAlias,++  -- * Conversions from/to 'BO' monad.+  unsafeBOToLinIO,+  unsafeLinIOToBO,+  unsafeBOToSystemIO,+  unsafeSystemIOToBO,+  unsafeSTToBO,+  unsafeBOToST,+  unsafeUnBO,+) where++import Control.Monad.Borrow.Pure.BO.Internal
+ src/Control/Monad/Borrow/Pure/Clone.hs view
@@ -0,0 +1,241 @@+{-# LANGUAGE BlockArguments #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE DefaultSignatures #-}+{-# LANGUAGE DerivingStrategies #-}+{-# LANGUAGE DerivingVia #-}+{-# LANGUAGE LambdaCase #-}+{-# LANGUAGE LinearTypes #-}+{-# LANGUAGE QualifiedDo #-}+{-# LANGUAGE UndecidableInstances #-}+{-# LANGUAGE NoImplicitPrelude #-}++module Control.Monad.Borrow.Pure.Clone (+  Clone (..),+  genericClone,+  AsCopyable (..),+  Clone1 (..),+  clone1,+  GenericClone1,+  genericLiftClone,+  genericClone1,+) where++import Control.Functor.Linear qualified as Control+import Control.Monad.Borrow.Pure.BO.Internal+import Control.Monad.Borrow.Pure.Copyable+import Control.Monad.Borrow.Pure.Utils (coerceLin)+import Data.Coerce (Coercible, coerce)+import Data.Data (Proxy)+import Data.Int+import Data.Kind (Constraint, Type)+import Data.List.NonEmpty (NonEmpty)+import Data.Word+import GHC.Exts (Multiplicity (..))+import Generics.Linear+import Numeric.Natural+import Prelude.Linear+import Unsafe.Linear qualified as Unsafe++{- | @'Clone' a@ is analogous o @'Copyable' a@, but requires cloned values+to be accessible only inside the @'BO' α@ monad.++The difference between 'Clone' and 'Copyable' is that the former allows for+cloning a shared borrow of a /mutable/ or /linear/ value, while the latter requires cloning a shared borrow of an /immutable/ value.+This is because we can leak @'Share' α a@ via 'Prelude.Linear.Movable' instance, and+hence it can outlive the original @'BO' α@ lifetime, which allows leaking mutable states inside @a@ into /unrestricted/ contexts, which destroys the soundness severly.+-}+class Clone a where+  clone :: Share α a %1 -> BO α a+  default clone :: (GenericClone a) => Share α a %1 -> BO α a+  clone = genericClone++newtype AsCopyable a = AsCopyable a+  deriving newtype (Copyable)++instance (Copyable a) => Clone (AsCopyable a) where+  clone = Control.pure . copy+  {-# INLINE clone #-}++deriving via AsCopyable Int instance Clone Int++deriving via AsCopyable Int8 instance Clone Int8++deriving via AsCopyable Int16 instance Clone Int16++deriving via AsCopyable Int32 instance Clone Int32++deriving via AsCopyable Int64 instance Clone Int64++deriving via AsCopyable Word instance Clone Word++deriving via AsCopyable Word8 instance Clone Word8++deriving via AsCopyable Word16 instance Clone Word16++deriving via AsCopyable Word32 instance Clone Word32++deriving via AsCopyable Word64 instance Clone Word64++deriving via AsCopyable Char instance Clone Char++deriving via AsCopyable Bool instance Clone Bool++deriving via AsCopyable Integer instance Clone Integer++deriving via AsCopyable Natural instance Clone Natural++deriving via AsCopyable Double instance Clone Double++deriving via AsCopyable Float instance Clone Float++deriving via AsCopyable () instance Clone ()++type GenericClone a = (Generic a, GClone (Rep a))++genericClone :: (GenericClone a) => Share α a %1 -> BO α a+{-# INLINE genericClone #-}+genericClone (UnsafeAlias x) = to Control.<$> gclone (UnsafeAlias (from x))++type GClone :: forall {k}. (k -> Type) -> Constraint+class GClone f where+  gclone :: Share α (f x) %1 -> BO α (f x)++instance (Clone a) => GClone (K1 i a) where+  gclone = coerceLin $ clone @a++instance (GClone f, GClone g) => GClone (f :*: g) where+  gclone (UnsafeAlias (f :*: g)) =+    (:*:) Control.<$> gclone (UnsafeAlias f) Control.<*> gclone (UnsafeAlias g)++instance (GClone f) => GClone (M1 i c f) where+  gclone = \case+    UnsafeAlias (M1 x) -> coerceLin $ gclone (UnsafeAlias x)++instance (GClone f) => GClone (MP1 'One f) where+  gclone = \case+    UnsafeAlias (MP1 x) -> MP1 Control.<$> gclone (UnsafeAlias x)++instance GClone (MP1 'Many f) where+  gclone = \case+    UnsafeAlias mp1 -> Control.pure mp1++instance (GClone f, GClone g) => GClone (f :+: g) where+  gclone = \case+    UnsafeAlias (L1 x) -> L1 Control.<$> gclone (UnsafeAlias x)+    UnsafeAlias (R1 x) -> R1 Control.<$> gclone (UnsafeAlias x)++instance GClone U1 where+  gclone = Control.pure . coerceLin . unsafeUnalias++instance GClone V1 where+  gclone = \case {} . unsafeUnalias++instance (GenericClone a) => Clone (Generically a) where+  clone = Control.fmap Generically . genericClone . unsafeMapAlias (\(Generically x) -> x)++deriving via+  Generically (a, b)+  instance+    (Clone a, Clone b) => Clone (a, b)++deriving via+  Generically (a, b, c)+  instance+    (Clone a, Clone b, Clone c) => Clone (a, b, c)++deriving via+  Generically (a, b, c, d)+  instance+    (Clone a, Clone b, Clone c, Clone d) => Clone (a, b, c, d)++deriving via+  Generically (a, b, c, d, e)+  instance+    (Clone a, Clone b, Clone c, Clone d, Clone e) => Clone (a, b, c, d, e)++deriving via+  Generically (Either a b)+  instance+    (Clone a, Clone b) => Clone (Either a b)++deriving via Generically [a] instance (Clone a) => Clone [a]++deriving via Generically (Maybe a) instance (Clone a) => Clone (Maybe a)++deriving via Generically (NonEmpty a) instance (Clone a) => Clone (NonEmpty a)++-- | Lifting of the 'Clone' operation to unary type constructors.+class Clone1 f where+  liftClone :: (Share α a %1 -> BO α b) -> Share α (f a) %1 -> BO α (f b)+  default liftClone :: (GenericClone1 f) => (Share α a %1 -> BO α b) -> Share α (f a) %1 -> BO α (f b)+  liftClone = genericLiftClone++clone1 :: (Clone1 f, Clone a) => Share α (f a) %1 -> BO α (f a)+{-# INLINE clone1 #-}+clone1 = liftClone clone++type GenericClone1 f = (Clone1 (Rep1 @Type f), Generic1 f)++genericLiftClone :: forall f a b α. (GenericClone1 f) => (Share α a %1 -> BO α b) -> Share α (f a) %1 -> BO α (f b)+{-# INLINE genericLiftClone #-}+genericLiftClone f (UnsafeAlias x) =+  to1 Control.<$> liftClone f (UnsafeAlias $ from1 x)++genericClone1 :: forall f a α. (GenericClone1 f, Clone a) => Share α (f a) %1 -> BO α (f a)+{-# INLINE genericClone1 #-}+genericClone1 = genericLiftClone clone++instance (GenericClone1 f) => Clone1 (Generically1 @Type f) where+  liftClone f = Control.fmap Generically1 . genericLiftClone f . coerceShr+  {-# INLINE liftClone #-}++instance (Clone a) => Clone1 (K1 i a) where+  liftClone _ = coerce $! clone @a+  {-# INLINE liftClone #-}++instance Clone1 Par1 where+  liftClone f = coerceLin . f . coerceShr+  {-# INLINE liftClone #-}++instance (Clone1 f) => Clone1 (M1 i c f) where+  liftClone f = Control.fmap M1 . liftClone f . coerceShr @_+  {-# INLINE liftClone #-}++instance (Clone1 f, Clone1 g) => Clone1 (f :*: g) where+  liftClone f (UnsafeAlias (f' :*: g')) =+    (:*:)+      Control.<$> liftClone f (UnsafeAlias f')+      Control.<*> liftClone f (UnsafeAlias g')++instance (Clone1 f, Clone1 g) => Clone1 (f :+: g) where+  liftClone f = \case+    UnsafeAlias (L1 x) -> Control.fmap L1 . liftClone f . coerceShr $ UnsafeAlias x+    UnsafeAlias (R1 x) -> Control.fmap R1 . liftClone f . coerceShr $ UnsafeAlias x+  {-# INLINE liftClone #-}++instance (Clone1 f, Clone1 g) => Clone1 (f :.: g) where+  liftClone f = \(UnsafeAlias (Comp1 x)) -> Control.fmap Comp1 . liftClone (liftClone f) $ UnsafeAlias x+  {-# INLINE liftClone #-}++instance Clone1 U1 where+  liftClone _ = coerceLin . gclone+  {-# INLINE liftClone #-}++instance Clone1 V1 where+  liftClone _ = \case {} . unsafeUnalias+  {-# INLINE liftClone #-}++coerceShr :: (Coercible a b) => Share α a %1 -> Share α b+coerceShr = Unsafe.toLinear \ !a -> coerce a++deriving via Generically1 Maybe instance Clone1 Maybe++deriving via Generically1 [] instance Clone1 []++deriving via Generically1 Proxy instance Clone1 Proxy++deriving via Generically1 NonEmpty instance Clone1 NonEmpty++deriving via Generically1 (Either a) instance (Clone a) => Clone1 (Either a)++deriving via Generically1 ((,) a) instance (Clone a) => Clone1 ((,) a)
+ src/Control/Monad/Borrow/Pure/Copyable.hs view
@@ -0,0 +1,280 @@+{-# LANGUAGE BlockArguments #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE DefaultSignatures #-}+{-# LANGUAGE DeriveAnyClass #-}+{-# LANGUAGE DerivingVia #-}+{-# LANGUAGE ImpredicativeTypes #-}+{-# LANGUAGE LambdaCase #-}+{-# LANGUAGE MagicHash #-}+{-# LANGUAGE PartialTypeSignatures #-}+{-# LANGUAGE PatternSynonyms #-}+{-# LANGUAGE QualifiedDo #-}+{-# LANGUAGE QuantifiedConstraints #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE RoleAnnotations #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE StandaloneKindSignatures #-}+{-# LANGUAGE TypeData #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE UnboxedTuples #-}+{-# LANGUAGE UndecidableInstances #-}+{-# LANGUAGE UnliftedNewtypes #-}+{-# LANGUAGE ViewPatterns #-}+{-# LANGUAGE NoImplicitPrelude #-}+{-# OPTIONS_GHC -Wno-name-shadowing #-}+{-# OPTIONS_GHC -Wno-partial-type-signatures #-}+{-# OPTIONS_GHC -Wno-redundant-constraints #-}+{-# OPTIONS_HADDOCK hide #-}++module Control.Monad.Borrow.Pure.Copyable (+  Copyable (..),+  copyMut,+  genericCopy,+  GenericCopyable,+  Copyable1 (..),+  AsCopyable1 (..),+  GenericCopyable1,+  copy1,+  genericCopy1,+  genericLiftCopy,+) where++import Control.Monad.Borrow.Pure.BO.Internal+import Control.Monad.Borrow.Pure.Utils (coerceLin)+import Data.Array.Mutable.Linear (Array)+import Data.Int+import Data.Kind (Constraint, Type)+import Data.Semigroup qualified as Sem+import Data.Vector.Mutable.Linear (Vector)+import Data.Word+import GHC.TypeError (ErrorMessage (..))+import Generics.Linear+import Numeric.Natural (Natural)+import Prelude.Linear+import Prelude.Linear.Unsatisfiable (Unsatisfiable, unsatisfiable)++class Copyable a where+  copy :: Borrow bk α a %1 -> a++instance Copyable (Ur a) where+  copy (UnsafeAlias (Ur !a)) = Ur a+  {-# INLINE copy #-}++instance+  (Unsatisfiable (ShowType (Array a) :<>: Text " cannot be copied!")) =>+  Copyable (Array a)+  where+  copy = unsatisfiable++instance+  (Unsatisfiable (ShowType (Vector a) :<>: Text " cannot be copied!")) =>+  Copyable (Vector a)+  where+  copy = unsatisfiable++newtype UnsafeAssumeNoVar a = UnsafeAssumeNoVar a++instance Copyable (UnsafeAssumeNoVar a) where+  copy = \(UnsafeAlias !a) -> a+  {-# INLINE copy #-}++deriving via UnsafeAssumeNoVar Int instance Copyable Int++deriving via UnsafeAssumeNoVar Int8 instance Copyable Int8++deriving via UnsafeAssumeNoVar Int16 instance Copyable Int16++deriving via UnsafeAssumeNoVar Int32 instance Copyable Int32++deriving via UnsafeAssumeNoVar Int64 instance Copyable Int64++deriving via UnsafeAssumeNoVar Word instance Copyable Word++deriving via UnsafeAssumeNoVar Word8 instance Copyable Word8++deriving via UnsafeAssumeNoVar Word16 instance Copyable Word16++deriving via UnsafeAssumeNoVar Word32 instance Copyable Word32++deriving via UnsafeAssumeNoVar Word64 instance Copyable Word64++deriving via UnsafeAssumeNoVar Integer instance Copyable Integer++deriving via UnsafeAssumeNoVar Natural instance Copyable Natural++deriving via UnsafeAssumeNoVar Float instance Copyable Float++deriving via UnsafeAssumeNoVar Double instance Copyable Double++deriving via UnsafeAssumeNoVar Char instance Copyable Char++deriving via UnsafeAssumeNoVar Bool instance Copyable Bool++type GenericCopyable a = (Generic a, GCopyable (Rep a))++genericCopy :: (GenericCopyable a) => Borrow bk α a %1 -> a+{-# INLINE genericCopy #-}+genericCopy (UnsafeAlias x) = to (gcopy (UnsafeAlias (from x)))++type GCopyable :: forall {k}. (k -> Type) -> Constraint+class GCopyable f where+  gcopy :: Borrow bk α (f x) %1 -> f x++instance (Copyable a) => GCopyable (K1 i a) where+  gcopy = \(UnsafeAlias (K1 !a)) -> K1 (copy (UnsafeAlias a))+  {-# INLINE gcopy #-}++instance (GCopyable f, GCopyable g) => GCopyable (f :*: g) where+  gcopy (UnsafeAlias (!f :*: !g)) =+    gcopy (UnsafeAlias f) :*: gcopy (UnsafeAlias g)++instance (GCopyable f) => GCopyable (M1 i c f) where+  gcopy = \case+    UnsafeAlias (M1 !x) -> M1 (gcopy (UnsafeAlias x))++instance (GCopyable f) => GCopyable (MP1 m f) where+  gcopy = \case+    UnsafeAlias (MP1 !x) -> MP1 (gcopy (UnsafeAlias x))++instance (GCopyable f, GCopyable g) => GCopyable (f :+: g) where+  gcopy = \case+    UnsafeAlias (L1 !x) -> L1 (gcopy (UnsafeAlias x))+    UnsafeAlias (R1 !x) -> R1 (gcopy (UnsafeAlias x))++instance GCopyable U1 where+  gcopy = \case+    UnsafeAlias U1 -> U1++instance GCopyable V1 where+  gcopy = \case {} . unsafeUnalias++instance (GenericCopyable a) => Copyable (Generically a) where+  copy = Generically . genericCopy . unsafeMapAlias (\(Generically x) -> x)++deriving via Generically () instance Copyable ()++deriving via+  Generically (Sum a)+  instance+    (Copyable a) => Copyable (Sum a)++deriving via+  Generically (Product a)+  instance+    (Copyable a) => Copyable (Product a)++deriving via+  Generically [a]+  instance+    (Copyable a) => Copyable [a]++deriving via+  Generically (Sem.Max a)+  instance+    (Copyable a) => Copyable (Sem.Max a)++deriving via+  Generically (Maybe a)+  instance+    (Copyable a) => Copyable (Maybe a)++deriving via+  Generically (Sem.Min a)+  instance+    (Copyable a) => Copyable (Sem.Min a)++deriving via+  Generically (a, b)+  instance+    (Copyable a, Copyable b) =>+    Copyable (a, b)++deriving via+  Generically (a, b, c)+  instance+    (Copyable a, Copyable b, Copyable c) =>+    Copyable (a, b, c)++deriving via+  Generically (a, b, c, d)+  instance+    (Copyable a, Copyable b, Copyable c, Copyable d) =>+    Copyable (a, b, c, d)++deriving via+  Generically (Either a b)+  instance+    (Copyable a, Copyable b) => Copyable (Either a b)++deriving via+  Generically (Sem.Arg a b)+  instance+    (Copyable a, Copyable b) => Copyable (Sem.Arg a b)++newtype AsCopyable1 f a = AsCopyable1 (f a)++instance (Copyable1 f, Copyable a) => Copyable (AsCopyable1 f a) where+  copy = AsCopyable1 . copy1 . unsafeMapAlias \(AsCopyable1 x) -> x+  {-# INLINE copy #-}++-- | Lifting of the 'Copyable' operation to unary type constructors.+class Copyable1 f where+  liftCopy :: (Borrow bk α a %1 -> b) -> Borrow bk α (f a) %1 -> f b++type GenericCopyable1 f = (Copyable1 (Rep1 @Type f), Generic1 f)++genericLiftCopy :: forall f bk a b α. (GenericCopyable1 f) => (Borrow bk α a %1 -> b) -> Borrow bk α (f a) %1 -> f b+{-# INLINE genericLiftCopy #-}+genericLiftCopy f (UnsafeAlias x) = to1 $ liftCopy f (UnsafeAlias $ from1 x)++genericCopy1 :: forall f a α. (GenericCopyable1 f, Copyable a) => Share α (f a) %1 -> f a+{-# INLINE genericCopy1 #-}+genericCopy1 = genericLiftCopy copy++copy1 :: (Copyable1 f, Copyable a) => Borrow bk α (f a) %1 -> f a+{-# INLINE copy1 #-}+copy1 = liftCopy copy++instance (GenericCopyable1 f) => Copyable1 (Generically1 @Type f) where+  liftCopy f = Generically1 . genericLiftCopy f . coerceLin+  {-# INLINE liftCopy #-}++instance (Copyable c) => Copyable1 (K1 i c) where+  liftCopy _ = coerceLin $! copy @c+  {-# INLINE liftCopy #-}++instance Copyable1 Par1 where+  liftCopy f = Par1 . f . coerceLin+  {-# INLINE liftCopy #-}++instance (Copyable1 f) => Copyable1 (M1 i c f) where+  liftCopy f = M1 . liftCopy f . coerceLin+  {-# INLINE liftCopy #-}++instance (Copyable1 l, Copyable1 r) => Copyable1 (l :*: r) where+  liftCopy f = \(UnsafeAlias (!l :*: !r)) ->+    let !l' = liftCopy f (UnsafeAlias l)+        !r' = liftCopy f (UnsafeAlias r)+     in l' :*: r'+  {-# INLINE liftCopy #-}++instance (Copyable1 f, Copyable1 g) => Copyable1 (f :.: g) where+  liftCopy f = \(UnsafeAlias (Comp1 x)) ->+    Comp1 . liftCopy (liftCopy f) $ UnsafeAlias x+  {-# INLINE liftCopy #-}++instance (Copyable1 l, Copyable1 r) => Copyable1 (l :+: r) where+  liftCopy f = \(UnsafeAlias sum) -> case sum of+    L1 !l -> L1 $! (liftCopy f (UnsafeAlias l))+    R1 !r -> R1 $! (liftCopy f (UnsafeAlias r))+  {-# INLINE liftCopy #-}++{- | A variant of 'copy' that returns 'Ur' wrapped copy of the value.+'Ur' wrapper was not necessary because 'Share' is always introduced unrestricted,+whereas 'Mut' is introduced linearly, so it is convenient to have 'Ur' wrapped version.+-}+copyMut :: (Copyable a) => Mut α a %1 -> Ur a+{-# INLINE copyMut #-}+copyMut mut =+  let !(Ur shr) = share mut+   in Ur (copy shr)
+ src/Control/Monad/Borrow/Pure/Experimental/Borrows.hs view
@@ -0,0 +1,55 @@+{-# LANGUAGE BlockArguments #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE DefaultSignatures #-}+{-# LANGUAGE DeriveAnyClass #-}+{-# LANGUAGE DerivingVia #-}+{-# LANGUAGE ExplicitNamespaces #-}+{-# LANGUAGE FunctionalDependencies #-}+{-# LANGUAGE ImpredicativeTypes #-}+{-# LANGUAGE LambdaCase #-}+{-# LANGUAGE PartialTypeSignatures #-}+{-# LANGUAGE QualifiedDo #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TypeAbstractions #-}+{-# LANGUAGE UndecidableInstances #-}+{-# LANGUAGE NoImplicitPrelude #-}+{-# OPTIONS_GHC -Wno-name-shadowing #-}+{-# OPTIONS_GHC -Wno-redundant-constraints #-}++{- |+The module provides 'Borrows', which is a heterogeneous list of 'Borrow's in the same lifetime.+-}+module Control.Monad.Borrow.Pure.Experimental.Borrows (+  Borrows (..),+) where++import Control.Functor.Linear qualified as Control+import Control.Monad.Borrow.Pure.Affine+import Control.Monad.Borrow.Pure.Affine.Unsafe (unsafeAff)+import Control.Monad.Borrow.Pure.BO+import Control.Monad.Borrow.Pure.Experimental.Reborrowable+import Data.Coerce.Directed.Unsafe+import Data.Kind+import Prelude.Linear hiding (foldMap)+import Unsafe.Linear qualified as Unsafe++type Borrows :: BorrowKind -> Lifetime -> [Type] -> Type+data Borrows bk α xs where+  BNil :: Borrows bk α '[]+  (:-) :: !(Borrow bk α x) %1 -> !(Borrows bk α xs) %1 -> Borrows bk α (x ': xs)++infixr 5 :-++instance Affine (Borrows bk α xs) where+  aff = unsafeAff++deriving via AsAffine (Borrows bk α xs) instance Consumable (Borrows bk α xs)++instance (β <= α) => Borrows bk α xs <: Borrows bk' β xs where+  subtype = UnsafeSubtype++instance Reborrowable (Borrows bk) where+  locally' = Unsafe.toLinear \bors k -> Control.do+    (,bors) Control.<$> srunBO (k $ upcast bors)+  {-# INLINE locally' #-}
+ src/Control/Monad/Borrow/Pure/Experimental/Loop.hs view
@@ -0,0 +1,316 @@+{-# LANGUAGE BlockArguments #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE DefaultSignatures #-}+{-# LANGUAGE DeriveAnyClass #-}+{-# LANGUAGE DerivingVia #-}+{-# LANGUAGE ExplicitNamespaces #-}+{-# LANGUAGE FunctionalDependencies #-}+{-# LANGUAGE ImpredicativeTypes #-}+{-# LANGUAGE LambdaCase #-}+{-# LANGUAGE PartialTypeSignatures #-}+{-# LANGUAGE QualifiedDo #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TypeAbstractions #-}+{-# LANGUAGE UndecidableInstances #-}+{-# LANGUAGE NoImplicitPrelude #-}+{-# OPTIONS_GHC -Wno-name-shadowing #-}+{-# OPTIONS_GHC -Wno-partial-type-signatures #-}+{-# OPTIONS_GHC -Wno-redundant-constraints #-}++{- |+This module provides 'Foldable' class, and provides a way to loop through it while reborrowing existing 'Borrow's into sublifetime.+The module also introduces 'Borrows', which is a heterogeneous list of 'Borrow's in the same lifetime.+-}+module Control.Monad.Borrow.Pure.Experimental.Loop (+  Borrows (..),+  forReborrowing,+  forReborrowingOf_,+  forReborrowing_,+  iforReborrowingOf_,+  iforReborrowing_,+  Fold,+  Foldable (..),+  IndexedFold,+  ifoldMapDefaultOf,+  FoldableWithIndex (..),+  traverse_,+  for_,+  toListOf,+  toList,+  foldBorrow,+  foldBorrowOf,+  GenericFoldable,+  genericFoldMap,+  ifoldMapDefault,+) where++import Control.Functor.Linear qualified as Control+import Control.Monad.Borrow.Pure+import Control.Monad.Borrow.Pure.BO.Unsafe+import Control.Monad.Borrow.Pure.Experimental.Borrows+import Control.Monad.Borrow.Pure.Experimental.Reborrowable+import Control.Monad.Borrow.Pure.Utils (coerceLin)+import Data.Bifunctor.Linear qualified as Bi+import Data.Functor.Linear qualified as Data+import Data.HashMap.Mutable.Linear qualified as LHM+import Data.List.NonEmpty.Linear (NonEmpty)+import Data.List.NonEmpty.Linear qualified as LNE+import Data.Monoid.Linear+import Data.Vector.Mutable.Linear qualified as LV+import Generics.Linear+import Prelude.Linear hiding (foldMap)+import Prelude.Linear qualified as PL+import Unsafe.Linear qualified as Unsafe++{- |+@'forReborrowingN' iterates over the elements of 'Data.Traversable' @t@+inside the delimited sublifetime, reborrowing the 'Borrows' in @bors@ for that sublifetime.+-}+forReborrowing ::+  (Data.Traversable t, Reborrowable bor) =>+  bor α xs %1 ->+  t b %1 ->+  ( forall β.+    bor (β /\ α) xs %1 ->+    b %1 ->+    BO (β /\ α) c+  ) ->+  BO α (t c, bor α xs)+{-# INLINE forReborrowing #-}+forReborrowing bors tb k =+  flip Control.runStateT bors $+    Data.for tb \a -> Control.StateT \bors ->+      locally bors (\bors -> k bors a)++type Fold s a = forall w. (Monoid w) => (a %1 -> w) -> s %1 -> w++-- See https://github.com/tweag/linear-base/issues/190 for the discussion.+class Foldable t where+  foldMap :: (Monoid w) => (a %1 -> w) -> t a %1 -> w++type IndexedFold i s a = forall w. (Monoid w) => (i %1 -> a %1 -> w) -> s %1 -> w++class (Foldable t) => FoldableWithIndex i t | t -> i where+  ifoldMap :: (Monoid w) => (i %1 -> a %1 -> w) -> t a %1 -> w+  default ifoldMap ::+    (Foldable t, i ~ Int, Monoid w) =>+    (i %1 -> a %1 -> w) -> t a %1 -> w+  ifoldMap = ifoldMapDefault+  {-# INLINE ifoldMap #-}++ifoldMapDefaultOf :: forall s a. Fold s a %1 -> IndexedFold Int s a+{-# INLINE ifoldMapDefaultOf #-}+ifoldMapDefaultOf fld k s =+  flip Control.evalState (Ur 0) $ unAp $ flip fld s $ \a -> Ap Control.do+    Ur i <- Control.get+    Control.put $ Ur $! i + 1+    Control.pure $ k i a++ifoldMapDefault :: (Foldable t) => IndexedFold Int (t a) a+{-# INLINE ifoldMapDefault #-}+ifoldMapDefault = ifoldMapDefaultOf foldMap++foldBorrowOf :: Fold s a %1 -> Fold (Borrow bk α s) (Borrow bk α a)+{-# INLINE foldBorrowOf #-}+foldBorrowOf fld k = fld (k . UnsafeAlias) . unsafeUnalias++foldBorrow :: (Foldable t) => Fold (Borrow bk α (t a)) (Borrow bk α a)+{-# INLINE foldBorrow #-}+foldBorrow = foldBorrowOf foldMap++traverse_ :: (Foldable t, Data.Applicative m) => (a %1 -> m ()) -> t a %1 -> m ()+{-# INLINE traverse_ #-}+traverse_ f = unAp . foldMap (Ap . f)++for_ :: (Foldable t, Data.Applicative m) => t a %1 -> (a %1 -> m ()) -> m ()+{-# INLINE for_ #-}+for_ = flip traverse_++newtype Ap m a = Ap (m a)+  deriving newtype (Data.Functor, Control.Functor, Data.Applicative, Control.Applicative)++instance (Data.Applicative f, Semigroup w) => Semigroup (Ap f w) where+  (<>) = Data.liftA2 (<>)+  {-# INLINE (<>) #-}++instance (Data.Applicative f, Monoid w) => Monoid (Ap f w) where+  mempty = Data.pure mempty+  {-# INLINE mempty #-}++unAp :: Ap m a %1 -> m a+unAp (Ap m) = m+{-# INLINE unAp #-}++forReborrowingOf_ ::+  (Reborrowable bor) =>+  Fold s a %1 ->+  bor α xs %1 ->+  s %1 ->+  ( forall β.+    bor (β /\ α) xs %1 ->+    a %1 ->+    BO (β /\ α) ()+  ) ->+  BO α (bor α xs)+{-# INLINE forReborrowingOf_ #-}+forReborrowingOf_ fld bors s k =+  flip Control.execStateT bors $+    unAp $+      flip fld s $+        Ap . \a -> Control.StateT \bors -> locally bors (\bors -> k bors a)++forReborrowing_ ::+  (Foldable t, Reborrowable bor) =>+  bor α xs %1 ->+  t a %1 ->+  ( forall β.+    bor (β /\ α) xs %1 ->+    a %1 ->+    BO (β /\ α) ()+  ) ->+  BO α (bor α xs)+{-# INLINE forReborrowing_ #-}+forReborrowing_ = forReborrowingOf_ foldMap++iforReborrowingOf_ ::+  (Reborrowable bor) =>+  IndexedFold i s a %1 ->+  bor α xs %1 ->+  s %1 ->+  ( forall β.+    bor (β /\ α) xs %1 ->+    i %1 ->+    a %1 ->+    BO (β /\ α) ()+  ) ->+  BO α (bor α xs)+{-# INLINE iforReborrowingOf_ #-}+iforReborrowingOf_ fld bors s k =+  flip Control.execStateT bors $+    unAp $+      flip fld s \i a ->+        Ap $ Control.StateT \bors -> locally bors (\bors -> k bors i a)++iforReborrowing_ ::+  (FoldableWithIndex i t, Reborrowable bor) =>+  bor α xs %1 ->+  t a %1 ->+  ( forall β.+    bor (β /\ α) xs %1 ->+    i %1 ->+    a %1 ->+    BO (β /\ α) ()+  ) ->+  BO α (bor α xs)+{-# INLINE iforReborrowing_ #-}+iforReborrowing_ = iforReborrowingOf_ ifoldMap++toListOf :: Fold s a %1 -> s %1 -> [a]+{-# INLINE toListOf #-}+toListOf fld = fromDList . fld singletonDL++toList :: (Foldable t) => t a %1 -> [a]+{-# INLINE toList #-}+toList = toListOf foldMap++newtype DList a = DList ([a] %1 -> [a])++fromDList :: DList a %1 -> [a]+{-# INLINE fromDList #-}+fromDList (DList f) = f []++singletonDL :: a %1 -> DList a+{-# INLINE singletonDL #-}+singletonDL a = DList (a :)++instance Semigroup (DList a) where+  DList f <> DList g = DList (f . g)+  {-# INLINE (<>) #-}++instance Monoid (DList a) where+  mempty = DList id+  {-# INLINE mempty #-}++instance Foldable [] where+  foldMap = PL.foldMap+  {-# INLINE foldMap #-}++deriving anyclass instance FoldableWithIndex Int []++instance Foldable Maybe where+  foldMap f = maybe mempty f+  {-# INLINE foldMap #-}++instance FoldableWithIndex () Maybe where+  ifoldMap f = foldMap (f ())+  {-# INLINE ifoldMap #-}++instance (Consumable e) => Foldable ((,) e) where+  foldMap f = uncurry lseq . Bi.bimap consume f+  {-# INLINE foldMap #-}++instance (Consumable e) => Foldable (Either e) where+  foldMap f = either ((`lseq` mempty) . consume) f+  {-# INLINE foldMap #-}++instance Foldable NonEmpty where+  foldMap f = foldMap f . LNE.toList+  {-# INLINE foldMap #-}++instance Foldable U1 where+  foldMap _f = \U1 -> mempty+  {-# INLINE foldMap #-}++instance Foldable V1 where+  foldMap _ = \case {}+  {-# INLINE foldMap #-}++instance (Foldable f) => Foldable (M1 i c f) where+  foldMap f = coerceLin $ foldMap @f f+  {-# INLINE foldMap #-}++instance (Foldable f) => Foldable (MP1 m f) where+  foldMap f (MP1 x) = foldMap f x+  {-# INLINE foldMap #-}++instance (Foldable f, Foldable g) => Foldable (f :*: g) where+  foldMap f (x :*: y) = foldMap f x <> foldMap f y++instance (Foldable f, Foldable g) => Foldable (f :+: g) where+  foldMap f = \case+    L1 x -> foldMap f x+    R1 y -> foldMap f y+  {-# INLINE foldMap #-}++type GenericFoldable t = (Generic1 t, Foldable (Rep1 t))++genericFoldMap :: (GenericFoldable t, Monoid w) => (a %1 -> w) -> t a %1 -> w+{-# INLINE genericFoldMap #-}+genericFoldMap f = foldMap f . from1++instance (GenericFoldable t) => Foldable (Generically1 t) where+  foldMap f = genericFoldMap f . (\(Generically1 x) -> x)+  {-# INLINE foldMap #-}++instance Foldable LV.Vector where+  foldMap f vec =+    LV.size vec & \case+      (Ur n, vec) -> DataFlow.do+        let {-# INLINE loop #-}+            loop !vec !i !w+              | i < n =+                  LV.unsafeGet i vec & \(Ur a, vec) -> DataFlow.do+                    let !w' = w <> f a+                    loop vec (i + 1) w'+              | otherwise = vec `lseq` w+        loop vec 0 mempty+  {-# INLINE foldMap #-}++deriving anyclass instance FoldableWithIndex Int LV.Vector++instance Foldable (LHM.HashMap k) where+  foldMap f hm = foldMap (Unsafe.toLinear \(_, v) -> f v) $ unur $ LHM.toList hm++instance FoldableWithIndex k (LHM.HashMap k) where+  ifoldMap f = foldMap (uncurry f) . unur . LHM.toList
+ src/Control/Monad/Borrow/Pure/Experimental/Reborrowable.hs view
@@ -0,0 +1,62 @@+{-# LANGUAGE BlockArguments #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE DerivingVia #-}+{-# LANGUAGE ExplicitNamespaces #-}+{-# LANGUAGE ImpredicativeTypes #-}+{-# LANGUAGE PartialTypeSignatures #-}+{-# LANGUAGE QualifiedDo #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TypeAbstractions #-}+{-# LANGUAGE NoImplicitPrelude #-}+{-# OPTIONS_GHC -Wno-name-shadowing #-}++module Control.Monad.Borrow.Pure.Experimental.Reborrowable (+  Reborrowable (..),+  locally,+  locally_,+) where++import Control.Functor.Linear qualified as Control+import Control.Monad.Borrow.Pure.BO+import Prelude.Linear++class Reborrowable bor where+  {- |+  Executes an operation on a borrow in sub lifetime.+  You may need @-XImpredicativeTypes@ extension to use this function.++  Generalization of 'reborrowing'' and 'sharing'' that works for both 'Mut' and 'Share' borrows.+  -}+  locally' ::+    bor α a %1 ->+    (forall β. bor (β /\ α) a %1 -> BO (β /\ α') (After β r)) %1 ->+    BO α' (r, bor α a)++instance Reborrowable Mut where+  {-# SPECIALIZE instance Reborrowable Mut #-}+  locally' = reborrowing'+  {-# INLINE locally' #-}++instance Reborrowable Share where+  {-# SPECIALIZE instance Reborrowable Share #-}+  locally' shr k = Control.do+    let %1 !(Ur sh) = move shr+    (,sh) Control.<$> srunBO (k (upcast sh))+  {-# INLINE locally' #-}++locally ::+  (Reborrowable bor) =>+  bor α a %1 ->+  (forall β. bor (β /\ α) a %1 -> BO (β /\ α') r) %1 ->+  BO α' (r, bor α a)+{-# INLINE locally #-}+locally bor k = locally' bor \mut -> Control.pure Control.<$> k mut++locally_ ::+  (Reborrowable bor, Consumable r) =>+  bor α a %1 ->+  (forall β. bor (β /\ α) a %1 -> BO (β /\ α') r) %1 ->+  BO α' (bor α a)+{-# INLINE locally_ #-}+locally_ bor k = uncurry lseq Control.<$> locally bor k
+ src/Control/Monad/Borrow/Pure/Lifetime.hs view
@@ -0,0 +1,11 @@+{-# LANGUAGE ExplicitNamespaces #-}++module Control.Monad.Borrow.Pure.Lifetime (+  type (/\),+  type (<=),+  type (>=),+  type Static,+  Lifetime,+) where++import Control.Monad.Borrow.Pure.Lifetime.Internal
+ src/Control/Monad/Borrow/Pure/Lifetime/Internal.hs view
@@ -0,0 +1,126 @@+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE StandaloneKindSignatures #-}+{-# LANGUAGE TypeData #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE UndecidableInstances #-}+{-# OPTIONS_GHC -Wno-redundant-constraints #-}+{-# OPTIONS_HADDOCK hide #-}++module Control.Monad.Borrow.Pure.Lifetime.Internal (+  module Control.Monad.Borrow.Pure.Lifetime.Internal,+) where++import Control.DeepSeq (NFData (..))+import Data.Kind+import GHC.TypeLits hiding (type (<=))++infixr 3 /\, :/\++-- | The meet of the two lifetimes. It is the longest lifetime that is shorter than both of them.+type (/\) = (:/\)++-- NOTE:  We want to use @TypeData@ extension for Lifetime, but it makes Haddock panic!++-- Lifetime is a free bounded lower semilattice generated by atomic lifetimes.++-- | The kind (type) of lifetimes.+data Lifetime = Al Nat | Lifetime :/\ Lifetime | Static++type Al = 'Al++-- | 'Static' lifetime, which lives forever and 'Control.Monad.Borrow.Pure.Lifetime.Token.neverEnds'.+type Static = 'Static++infix 2 <=, <=!, <=!!++type Witness :: Lifetime -> Lifetime -> Type+data Witness a b where+  Inf :: Witness a b -> Witness a c -> Witness a (b /\ c)+  Top :: Witness a Static+  Inherit' :: Witness' a b -> Witness a b++instance NFData (Witness a b) where+  rnf (Inf a b) = rnf a `seq` rnf b+  rnf Top = ()+  rnf (Inherit' w) = rnf w++deriving instance Show (Witness a b)++type Witness' :: Lifetime -> Lifetime -> Type+data Witness' a b where+  AssocR :: Witness' (a /\ (b /\ c)) d -> Witness' ((a /\ b) /\ c) d+  Inherit'' :: Witness'' a b -> Witness' a b++instance NFData (Witness' a b) where+  rnf (AssocR w) = rnf w+  rnf (Inherit'' w) = rnf w++deriving instance Show (Witness' a b)++type Witness'' :: Lifetime -> Lifetime -> Type+data Witness'' a b where+  Reflect :: Witness'' a a+  InfL :: Witness'' (a /\ b) a+  InfIntroL :: Witness' b c -> Witness'' (a /\ b) c++instance NFData (Witness'' a b) where+  rnf Reflect = ()+  rnf InfL = ()+  rnf (InfIntroL w) = rnf w++deriving instance Show (Witness'' a b)++type (<=) :: Lifetime -> Lifetime -> Constraint+class α <= β where+  -- | The witness of the relation.+  witness :: Witness α β++-- | Flipped version of '<='.+type (>=) :: Lifetime -> Lifetime -> Constraint+type α >= β = β <= α++instance (α <= β, α <= γ) => α <= β /\ γ where+  witness = Inf witness witness+  {-# NOINLINE witness #-}++instance α <= Static where+  witness = Top+  {-# NOINLINE witness #-}++instance {-# INCOHERENT #-} (α <=! β) => α <= β where+  witness = Inherit' witness'+  {-# NOINLINE witness #-}++type (<=!) :: Lifetime -> Lifetime -> Constraint+class α <=! β where+  -- | The witness of the relation.+  witness' :: Witness' α β++instance (α /\ (β /\ γ) <=! δ) => (α /\ β) /\ γ <=! δ where+  witness' = AssocR witness'+  {-# NOINLINE witness' #-}++instance {-# INCOHERENT #-} (α <=!! β) => α <=! β where+  witness' = Inherit'' witness''+  {-# NOINLINE witness' #-}++type (<=!!) :: Lifetime -> Lifetime -> Constraint+class α <=!! β where+  -- | The witness of the relation.+  witness'' :: Witness'' α β++instance α <=!! α where+  witness'' = Reflect+  {-# NOINLINE witness'' #-}++instance α /\ β <=!! α where+  witness'' = InfL+  {-# NOINLINE witness'' #-}++{-+instance α /\ β <=!! β where+  witness'' = Witness -}++instance {-# INCOHERENT #-} (β <=! γ) => α /\ β <=!! γ where+  witness'' = InfIntroL witness'+  {-# NOINLINE witness'' #-}
+ src/Control/Monad/Borrow/Pure/Lifetime/Token.hs view
@@ -0,0 +1,26 @@+{-# LANGUAGE DerivingVia #-}+{-# LANGUAGE MagicHash #-}+{-# LANGUAGE UnboxedTuples #-}+{-# LANGUAGE UnliftedNewtypes #-}++module Control.Monad.Borrow.Pure.Lifetime.Token (+  Linearly (),+  linearly,+  Now (),+  End (),+  EndToken,+  After (..),+  unAfter,+  withEnd,+  LinearOnly,+  withLinearly,+  withLinearly#,+  endLifetime,+  SomeNow (..),+  newLifetime,+  newLifetime',+  nowStatic,+  neverEnds,+) where++import Control.Monad.Borrow.Pure.Lifetime.Token.Internal
+ src/Control/Monad/Borrow/Pure/Lifetime/Token/Internal.hs view
@@ -0,0 +1,162 @@+{-# LANGUAGE BlockArguments #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE DerivingVia #-}+{-# LANGUAGE ExplicitNamespaces #-}+{-# LANGUAGE ImpredicativeTypes #-}+{-# LANGUAGE MagicHash #-}+{-# LANGUAGE PatternSynonyms #-}+{-# LANGUAGE RoleAnnotations #-}+{-# LANGUAGE UnboxedTuples #-}+{-# LANGUAGE UndecidableInstances #-}+{-# LANGUAGE UnliftedNewtypes #-}+{-# OPTIONS_GHC -Wno-redundant-constraints #-}+{-# OPTIONS_HADDOCK hide #-}++module Control.Monad.Borrow.Pure.Lifetime.Token.Internal (+  module Control.Monad.Borrow.Pure.Lifetime.Token.Internal,+) where++import Control.Functor.Linear qualified as Control+import Control.Monad.Borrow.Pure.Affine.Internal+import Control.Monad.Borrow.Pure.Lifetime.Internal+import Data.Coerce.Directed.Unsafe+import Data.Functor.Linear qualified as Data+import Data.Kind (Constraint)+import Data.Unrestricted.Linear+import GHC.Base (TYPE, UnliftedType, noinline, withDict)+import GHC.Exts qualified as GHC+import GHC.Stack (HasCallStack)+import Unsafe.Linear qualified as Unsafe++type role Now nominal++-- | Witness that the lifetime @α@ is ongoing.+data Now (α :: Lifetime) = UnsafeNow++data SomeNow where+  MkSomeNow :: Now (Al i) %1 -> SomeNow++newLifetime :: Linearly %1 -> SomeNow+newLifetime UnsafeLinearly = MkSomeNow UnsafeNow++newLifetime' :: Linearly %1 -> (forall ι. Now (Al ι) %1 -> a) %1 -> a+newLifetime' lin k =+  case newLifetime lin of+    MkSomeNow now -> k now++-- | Static Lifetime is always available.+nowStatic :: Now Static+nowStatic = UnsafeNow++instance Affine (Now α) where+  aff UnsafeNow = UnsafeAff UnsafeNow+  {-# INLINE aff #-}++instance LinearOnly (Now α) where+  linearOnly = UnsafeLinearOnly+  {-# INLINE linearOnly #-}++type role EndToken nominal++-- | Witness that the lifetime @α@ has ended.+data EndToken (α :: Lifetime) = UnsafeEnd++instance (α >= β) => EndToken α <: EndToken β where+  subtype = UnsafeSubtype++endLifetime :: Now (Al i) %1 -> (Ur (EndToken (Al i)))+endLifetime UnsafeNow = Ur UnsafeEnd++-- | Witness that the lifetime @α@ has ended.+class End (α :: Lifetime) where+  endToken :: EndToken α++-- | Static lifetime lasts forever.+neverEnds :: (HasCallStack, End Static) => a+neverEnds = error "Unreachable: if you see this, you created an End Static in the internal code!"++{- |+Utility type to represent an object available after the lifetime @α@.++You can use 'Control.Applicative' and 'Control.Monad' instances to write 'After' conveniently.+-}+newtype After α a = After ((End α) => a)++instance (α <= β, a <: b) => After α a <: After β b where+  subtype = UnsafeSubtype++unAfter :: (End α) => After α a %1 -> a+{-# INLINE unAfter #-}+unAfter (After r) = r++withEnd :: forall α r. EndToken α -> After α r %1 -> r+{-# INLINE withEnd #-}+withEnd end (After a) = Unsafe.toLinear (withDict @(End α) end) a++instance Data.Functor (After α) where+  fmap f (After r) = After (f r)+  {-# INLINE fmap #-}++instance Control.Functor (After α) where+  fmap f (After r) = After (f r)+  {-# INLINE fmap #-}++instance Data.Applicative (After α) where+  pure a = After a+  {-# INLINE pure #-}+  After f <*> After r = After (f r)+  {-# INLINE (<*>) #-}++instance Control.Applicative (After α) where+  pure a = After a+  {-# INLINE pure #-}+  After f <*> After r = After (f r)+  {-# INLINE (<*>) #-}++instance Control.Monad (After α) where+  After r >>= k = After (unAfter (k r))+  {-# INLINE (>>=) #-}++-- | Witness that the current computation is in a linear context.+data Linearly = UnsafeLinearly++linearly :: (Movable a) => (Linearly %1 -> a) %1 -> a+{-# NOINLINE linearly #-}+linearly = GHC.noinline \f ->+  case move (f UnsafeLinearly) of+    Ur !x -> x++data LinearOnlyWitness a = UnsafeLinearOnly++-- | A (non-bottom) value of the type @a@ can only live in a linear context.+type LinearOnly :: forall rep. TYPE rep -> Constraint+class LinearOnly a where+  linearOnly :: LinearOnlyWitness a++withLinearly :: (LinearOnly a) => a %1 -> (Linearly, a)+{-# NOINLINE withLinearly #-}+withLinearly = noinline \ !a -> (UnsafeLinearly, a)++withLinearly# :: forall (a :: UnliftedType). (LinearOnly a) => a %1 -> (# Linearly, a #)+withLinearly# = noinline \ !a -> (# UnsafeLinearly, a #)++instance LinearOnly Linearly where+  linearOnly = UnsafeLinearOnly+  {-# INLINE linearOnly #-}++instance Consumable Linearly where+  consume = \UnsafeLinearly -> ()+  {-# INLINE consume #-}++instance Dupable Linearly where+  -- NOTE: without inlining, GHC optimizer (especially, full-laziness and demand analysis)+  -- can eliminate duplicated 'Linearly's too eagerly, ruining the state-threading,+  -- and result in resource corruption in some cases.+  -- Such optimization can manifest when, for example, one duplicates 'Linearly'+  -- tokens multiple times and feed them to different allocation functions.+  -- Although we are not able to detect the exact situation, but we believe that+  -- GHC optimizer then eliminates every invocation on bulk allocation functions+  -- into a single one, which introduces unintended reuse of linear resources.+  -- Hence, we must instruct GHC not to inline this function and force+  dup2 = GHC.noinline \UnsafeLinearly -> (UnsafeLinearly, UnsafeLinearly)+  {-# NOINLINE dup2 #-}
+ src/Control/Monad/Borrow/Pure/Lifetime/Token/Unsafe.hs view
@@ -0,0 +1,23 @@+{-# LANGUAGE DerivingVia #-}+{-# LANGUAGE MagicHash #-}+{-# LANGUAGE UnboxedTuples #-}+{-# LANGUAGE UnliftedNewtypes #-}++{- |+This module provides __unsafe__ internals of "Control.Monad.Borrow.Pure.Lifetime.Token".+These are not meant to be used by end-users, so generally YOU SHOULD NOT import this module, and import "Control.Monad.Borrow.Pure.Lifetime.Token" instead.++This module is meant for library authors who want to build a new API on top of Pure Borrow.+This module provides internals of 'BO' and 'Alias', which can break the soundness guarded by the role system.+We __STRONGLY__ recommend to you to import only the needed parts of the definitions, and not to import everything or qualified.+-}+module Control.Monad.Borrow.Pure.Lifetime.Token.Unsafe (+  Linearly (..),+  LinearOnly (..),+  LinearOnlyWitness (..),+  Now (..),+  End (..),+  EndToken (..),+) where++import Control.Monad.Borrow.Pure.Lifetime.Token.Internal
+ src/Control/Monad/Borrow/Pure/Utils.hs view
@@ -0,0 +1,31 @@+{-# LANGUAGE MagicHash #-}++module Control.Monad.Borrow.Pure.Utils (+  module Control.Monad.Borrow.Pure.Utils,+) where++import Data.Coerce (Coercible)+import Data.Coerce qualified+import Data.Type.Coercion (Coercion, coerceWith)+import Data.Unrestricted.Linear+import GHC.Base (UnliftedType)+import Unsafe.Linear qualified as Unsafe++coerceLin :: (Coercible a b) => a %1 -> b+{-# INLINE coerceLin #-}+coerceLin = Unsafe.toLinear Data.Coerce.coerce++lseq# :: forall a (s :: UnliftedType). (Consumable a) => a %1 -> s %1 -> s+{-# INLINE lseq# #-}+lseq# a = case consume a of+  () -> \b -> b++coerceWithLin :: Coercion a b %1 -> a %1 -> b+{-# INLINE coerceWithLin #-}+coerceWithLin = Unsafe.toLinear2 coerceWith++infixr 1 >>>++(>>>) :: (a %1 -> b) -> (b %1 -> c) -> a %1 -> c+{-# INLINE (>>>) #-}+(>>>) f g = \x -> g (f x)
+ src/Control/Syntax/DataFlow.hs view
@@ -0,0 +1,26 @@+{-# LANGUAGE NoImplicitPrelude #-}++module Control.Syntax.DataFlow ((>>=), (>>), (*>), pure, return, (<*>), (<*)) where++import Prelude.Linear qualified as PL++(>>=) :: a %1 -> (a %1 -> b) %1 -> b+a >>= b = b a++(>>) :: (PL.Consumable a) => a %1 -> b %1 -> b+a >> b = PL.consume a PL.& \() -> b++(*>) :: (PL.Consumable a) => a %1 -> b %1 -> b+(*>) = (>>)++(<*) :: (PL.Consumable b) => a %1 -> b %1 -> a+a <* b = PL.consume b PL.& \() -> a++pure :: a %1 -> a+pure = PL.id++return :: a %1 -> a+return = PL.id++(<*>) :: (a %1 -> b) %1 -> a %1 -> b+f <*> a = f a
+ src/Data/Coerce/Directed.hs view
@@ -0,0 +1,19 @@+{-# LANGUAGE BlockArguments #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE DefaultSignatures #-}+{-# LANGUAGE DerivingVia #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE UndecidableInstances #-}+{-# LANGUAGE NoImplicitPrelude #-}+{-# OPTIONS_GHC -Wno-orphans #-}+{-# OPTIONS_GHC -Wno-redundant-constraints #-}++module Data.Coerce.Directed (+  type (<:) (),+  upcast,+  AsCoercible (..),+  GenericSubtype,+  genericUpcast,+) where++import Data.Coerce.Directed.Internal
+ src/Data/Coerce/Directed/Internal.hs view
@@ -0,0 +1,108 @@+{-# LANGUAGE BlockArguments #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE DefaultSignatures #-}+{-# LANGUAGE DerivingVia #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE UndecidableInstances #-}+{-# LANGUAGE NoImplicitPrelude #-}+{-# OPTIONS_GHC -Wno-orphans #-}+{-# OPTIONS_GHC -Wno-redundant-constraints #-}+{-# OPTIONS_HADDOCK hide #-}++module Data.Coerce.Directed.Internal (module Data.Coerce.Directed.Internal) where++import Data.Coerce (Coercible)+import Data.Kind (Constraint, Type)+import Data.Type.Ord+import GHC.Base (Multiplicity (..))+import Generics.Linear+import Prelude.Linear+import Unsafe.Coerce (unsafeCoerce)+import Unsafe.Linear qualified as Unsafe++infix 4 <:++-- Orphan instance!+type instance Compare (a :: Multiplicity) (b :: Multiplicity) = CmpMult One Many++type CmpMult :: Multiplicity -> Multiplicity -> Ordering+type family CmpMult p q where+  CmpMult One One = EQ+  CmpMult One Many = LT+  CmpMult Many One = GT+  CmpMult Many Many = EQ++data SubtypeWitness a b = UnsafeSubtype++class a <: b where+  subtype :: SubtypeWitness a b++upcast :: (a <: b) => a %1 -> b+upcast = Unsafe.toLinear unsafeCoerce++instance {-# INCOHERENT #-} (Coercible a b) => a <: b where+  subtype = UnsafeSubtype++newtype AsCoercible a = AsCoercible {runAsCoercible :: a}++instance (Coercible a b) => a <: AsCoercible b where+  subtype = UnsafeSubtype++deriving via+  Generically [b]+  instance+    (a <: b) => [a] <: [b]++deriving via+  Generically (a', b')+  instance+    (a <: a', b <: b') => (a, b) <: (a', b')++deriving via+  Generically (Either a' b')+  instance+    (a <: a', b <: b') => Either a b <: Either a' b'++deriving via+  Generically (a', b', c')+  instance+    (a <: a', b <: b', c <: c') => (a, b, c) <: (a', b', c')++instance+  (a' <: a, b <: b', p Data.Type.Ord.<= q) =>+  (a %p -> b) <: (a' %q -> b')+  where+  subtype = UnsafeSubtype++type GSubtype :: (k -> Type) -> (k -> Type) -> Constraint+class GSubtype f g where+  gsubtype :: SubtypeWitness f g++gupcast :: (GSubtype f g) => f a %1 -> g a+gupcast = Unsafe.toLinear unsafeCoerce++instance (a <: b) => GSubtype (K1 i a) (K1 i b) where+  gsubtype = UnsafeSubtype++instance {-# INCOHERENT #-} GSubtype f f where+  gsubtype = UnsafeSubtype++instance (GSubtype f g) => GSubtype (MP1 p f) (MP1 p g) where+  gsubtype = UnsafeSubtype++instance (GSubtype f g) => GSubtype (M1 i c f) (M1 i c g) where+  gsubtype = UnsafeSubtype++instance (GSubtype f f', GSubtype g g') => GSubtype (f :*: g) (f' :*: g') where+  gsubtype = UnsafeSubtype++instance (GSubtype l l', GSubtype r r') => GSubtype (l :+: r) (l' :+: r') where+  gsubtype = UnsafeSubtype++type GenericSubtype a b = (Generic a, Generic b, GSubtype (Rep a) (Rep b))++instance (GenericSubtype a b) => a <: Generically b where+  subtype = UnsafeSubtype++genericUpcast :: (GenericSubtype a b) => a %1 -> b+genericUpcast = to . gupcast . from
+ src/Data/Coerce/Directed/Unsafe.hs view
@@ -0,0 +1,21 @@+{-# LANGUAGE BlockArguments #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE DefaultSignatures #-}+{-# LANGUAGE DerivingVia #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE UndecidableInstances #-}+{-# LANGUAGE NoImplicitPrelude #-}+{-# OPTIONS_GHC -Wno-orphans #-}+{-# OPTIONS_GHC -Wno-redundant-constraints #-}++-- | This module exposes the unsafe internals of subtyping, which is only meant to be used for library implementors.+module Data.Coerce.Directed.Unsafe (+  type (<:) (..),+  SubtypeWitness (..),+  upcast,+  AsCoercible (..),+  GenericSubtype,+  genericUpcast,+) where++import Data.Coerce.Directed.Internal
+ src/Data/Comonad/Linear.hs view
@@ -0,0 +1,26 @@+{-# LANGUAGE DerivingStrategies #-}++module Data.Comonad.Linear (Comonad (..), ComonadApply (..)) where++import Data.Functor.Linear qualified as Data+import Data.Unrestricted.Linear (Ur (..))++class (Data.Functor w) => Comonad w where+  extract :: w a %1 -> a+  duplicate :: w a %1 -> w (w a)++instance Comonad Ur where+  extract (Ur a) = a+  {-# INLINE extract #-}++  duplicate (Ur a) = Ur (Ur a)+  {-# INLINE duplicate #-}++infixl 4 <@>++class (Comonad w) => ComonadApply w where+  (<@>) :: w (a %1 -> b) %1 -> w a %1 -> w b++instance ComonadApply Ur where+  (Ur f) <@> (Ur a) = Ur (f a)+  {-# INLINE (<@>) #-}
+ src/Data/Record/Linear/Borrow/Experimental/PatternMatch.hs view
@@ -0,0 +1,430 @@+{-# LANGUAGE AllowAmbiguousTypes #-}+{-# LANGUAGE BlockArguments #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE DeriveAnyClass #-}+{-# LANGUAGE DerivingStrategies #-}+{-# LANGUAGE DerivingVia #-}+{-# LANGUAGE FunctionalDependencies #-}+{-# LANGUAGE KindSignatures #-}+{-# LANGUAGE LambdaCase #-}+{-# LANGUAGE LinearTypes #-}+{-# LANGUAGE MagicHash #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE OverloadedLabels #-}+{-# LANGUAGE PartialTypeSignatures #-}+{-# LANGUAGE PolyKinds #-}+{-# LANGUAGE QuantifiedConstraints #-}+{-# LANGUAGE TemplateHaskell #-}+{-# LANGUAGE TypeData #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE UnboxedTuples #-}+{-# LANGUAGE UndecidableInstances #-}+{-# LANGUAGE UndecidableSuperClasses #-}+{-# LANGUAGE UnliftedNewtypes #-}+{-# LANGUAGE NoImplicitPrelude #-}++{- |+An experimental module for splitting a borrow of a record by pattern matching on it.+If you want to split out a field gradually and partially, see also "Data.Record.Linear.Borrow.Experimental.Split".++The API is subject to future change.+-}+module Data.Record.Linear.Borrow.Experimental.PatternMatch (+  -- * Label Type+  RecordLabel,++  -- * Single Field Accessor+  (.#),++  -- * #split# Splitting a record borrow into pieces+  -- $record-splitting++  -- ** APIs+  (.@),+  RecordLabels,+  FieldBorrows,+  LabelsOrBorrows (..),++  -- ** Internal APIs+  RecordEliminator (..),+  RecordLabel' (..),+) where++import Control.Monad.Borrow.Pure+import Control.Monad.Borrow.Pure.Affine (Affine (..), AsAffine (..))+import Control.Monad.Borrow.Pure.Affine.Unsafe (unsafeAff)+import Control.Monad.Borrow.Pure.BO+import Control.Monad.Borrow.Pure.BO.Unsafe (unsafeMapAlias)+import Data.Kind (Constraint)+import GHC.Base (TYPE, Type, proxy#)+import GHC.OverloadedLabels (IsLabel (..))+import GHC.Records (HasField (..))+import GHC.TypeError (ErrorMessage (..), Unsatisfiable)+import GHC.TypeLits (KnownSymbol, Symbol, symbolVal')+import Prelude.Linear hiding (All)+import Unsafe.Linear qualified as Unsafe++{- $setup++>>> import Control.Monad.Borrow.Pure.BO.Internal (BorrowKind(..))+-}++{- |+@'RecordLabel' r f a@ witnesses that the record type @r@ has a field named @f@ of type @a@.+Intended to be constructed with @OverloadedLabels@ extension, so that you can construct it by @#f@ syntax when the field @f@ of @a@ is imported in the current scope.++You can also expose 'RecordLabel' only, so that you can allow users to access such fields while internal implementation unexposed.+-}+type RecordLabel a f v = RecordLabel' a '(f, v)++-- | The actual definition of 'RecordLabel' for type-level hacks.+type RecordLabel' :: TYPE rep -> (Symbol, Type) -> Type+data RecordLabel' r fldVal where+  RecLab :: forall field r a. (HasField field r a) => RecordLabel' r '(field, a)++{- $record-splitting+== Overview++'(.#)' is handy when you need only one field of a borrowed record, but not applicable when you need to access more than one fields.+For that purpose, we provide '(.@)' operator for splitting a borrow of a record into FieldBorrows of its fields.+Consider the following:++>>> import Data.Ref.Linear (Ref)+>>> import Data.Vector.Mutable.Linear.Borrow (Vector)+>>> import Control.Monad.Borrow.Pure.BO+>>> data MyRecord = MyRecord { int :: Ref Int, strs :: Vector String, bool :: Ref Bool }++Suppose we have a mutable borrow of some @MyRecord@:++>>> :{+mutRec :: Mut α (MyRecord)+mutRec = undefined+:}++So, let's divide the mutable borrow into several pieces with '(.@)'.+First, we need to enable @OverloadedLabels@ extension to construct 'RecordLabel's:++>>> :set -XOverloadedLabels++First, we just want to divide into all the fields, in arbitrary order:++>>> (mutStrs, mutBool, mutInt) = mutRec .@ (#strs, #bool, #int)+>>> :t mutStrs+mutStrs :: Borrow 'Mut α (Vector String)++>>> :t mutBool+mutBool :: Borrow 'Mut α (Ref Bool)++>>> :t mutInt+mutInt :: Borrow 'Mut α (Ref Int)++Or, we can just divide into some of the fields (say, @bool@ and @strs@):++>>> (mutStrs, mutBool) = mutRec .@ (#strs, #bool)+>>> :t mutStrs+mutStrs :: Borrow 'Mut α (Vector String)++>>> :t mutBool+mutBool :: Borrow 'Mut α (Ref Bool)++Specifying the same field more than once results in a type error:++@+mutRec .@ (#strs, #bool, #strs)+-- error: Split record fields must be distinct, but got duplicate field: "strs"+@++In genral, '(.@)' accepts any /eliminator/ of a record borrow, which is typically one of the following:++    1. A tuple of 'RecordLabel's without duplcations (currently 2 to 5 components), or+    2. A heterogeneous list 'RecordLabels' of 'RecordLabel's, constructed with '(:#-)' and 'RNil', without duplcations on fields.++And fields not listed within the eliminator are not accessible after the split.+The examples so far uses tuples as eliminators, but you can also use 'RecordLabels'  as follows:++>>> mutStrs :#- mutBool :#- RNil = mutRec .@ #strs :#- #bool :#- RNil++'RecordLabels' will be mapped to 'FieldBorrows' after the split, and you can also use '(:#-)' and 'RNil' for pattern-matching.++Indeed, 'RecordLabel' itself is also a 'RecordEliminator', but if you are using `#f` syntax for constructing 'RecordLabel', you cannot use it with `.@` operator without type annotation because of the ambiguity.+If you just want to access one field, you can use '(.#)' operator.+-}++instance (KnownSymbol field) => Show (RecordLabel' r '(field, a)) where+  showsPrec d _ = showsPrec d $ symbolVal' @field proxy#++-- | This allows users to use @#f@ for constructing @'RecordLabel' a f v@.+instance+  (HasField field r a, fldVal ~ '(field, a)) =>+  IsLabel field (RecordLabel' r fldVal)+  where+  fromLabel = RecLab+  {-# INLINE fromLabel #-}++type Fst :: (k, v) -> k+type family Fst kv where+  Fst '(k, v) = k++type Snd :: (k, v) -> v+type family Snd kv where+  Snd '(k, v) = v++class+  ( lab ~ RecordLabel' a '(f, v)+  , RecordOf lab ~ a+  , SelectorOf lab ~ f+  , ValueOf lab ~ v+  ) =>+  IsRecordLabel' a lab f v+    | lab -> f v+  where+  type RecordOf lab :: Type+  type SelectorOf lab :: Symbol+  type ValueOf lab :: Type++instance IsRecordLabel' a (RecordLabel' a '(f, v)) f v where+  type RecordOf (RecordLabel' a '(f, v)) = a+  type SelectorOf (RecordLabel' a '(f, v)) = f+  type ValueOf (RecordLabel' a '(f, v)) = v++{- |+A class for *eliminators* of record, which can split a borrow of the whole record into FieldBorrows of its fields.+Typically, an eliminator is a tuple of 'RecordLabel's or heterogeneous 'RecordLabels'.+-}+class RecordEliminator elim a where+  type SplitBorrow elim (bk :: BorrowKind) (α :: Lifetime) a :: Type+  splitRecord :: elim %1 -> Borrow bk α a %1 -> SplitBorrow elim bk α a++{- |+Divides a borrow of a record into multiple FieldBorrows of its fields, according to the given @elim@inator.++Typically, @elim@ is one of the following:++* A tuple of 'RecordLabel's without duplcations (currently 2 to 5 components):++    @+    (.@) ::+      a %1 ->+      ('RecordLabel' a f1 v1, 'RecordLabel' a f2 v2, 'RecordLabel' a f3 v3) %1 ->+      ('Borrow' bk α v1, 'Borrow' bk α v2, 'Borrow' bk α v3)+    @++* A heterogeneous list of 'RecordLabel's without duplications:++    @+    (.@) ::+      a %1 ->+      'RecordLabels' '[ '(f1, v1), '(f2, v2), '(f3, v3), .. ] %1 ->+      'FieldBorrows' '[ '(f1, v1), '(f2, v2), '(f3, v3) ]+    @+-}+(.@) :: (RecordEliminator elim a) => Borrow bk α a %1 -> elim %1 -> SplitBorrow elim bk α a+(.@) = flip splitRecord+{-# INLINE (.@) #-}++{- |+@recBor '.#' #f@ divides a record borrow @recBor@ into a borrow of the field @f@.++This is '(.@)' specialised to 'RecordLabel' for better type inference.+To access multiple fields, you can use '(.@)' with a tuple of 'RecordLabel's or 'RecordLabels'.+See [Splitting a record borrow into pieces](#split) for more details.+-}+(.#) :: Borrow bk α a %1 -> RecordLabel a field val %1 -> Borrow bk α val+{-# INLINE (.#) #-}+(.#) = (.@)++infixl 4 .@++instance (a ~ r) => RecordEliminator (RecordLabel' r '(field, val)) a where+  type SplitBorrow (RecordLabel' r '(field, val)) bk α a = Borrow bk α val+  splitRecord RecLab = unsafeMapAlias (Unsafe.toLinear $ getField @field)+  {-# INLINE splitRecord #-}++type Distinct' :: Symbol -> Symbol -> Constraint+type family Distinct' l r :: Constraint where+  Distinct' l l = Unsatisfiable ('Text "Split record fields must be distinct, but got duplicate field: " ':<>: 'ShowType l)+  Distinct' l r = ()++class (Distinct' l r) => Distinct l r++instance (Distinct' l r) => Distinct l r++instance+  ( IsRecordLabel' a l f1 v1+  , IsRecordLabel' a r f2 v2+  , Distinct f1 f2+  ) =>+  RecordEliminator (l, r) a+  where+  type+    SplitBorrow (l, r) bk α a =+      (Borrow bk α (ValueOf l), Borrow bk α (ValueOf r))+  splitRecord (RecLab, RecLab) = Unsafe.toLinear \r ->+    ( unsafeMapAlias (Unsafe.toLinear (getField @f1)) r+    , unsafeMapAlias (Unsafe.toLinear (getField @f2)) r+    )++instance+  ( IsRecordLabel' a l1 f1 v1+  , IsRecordLabel' a l2 f2 v2+  , IsRecordLabel' a l3 f3 v3+  , Distinct f1 f2+  , Distinct f1 f3+  , Distinct f2 f3+  ) =>+  RecordEliminator (l1, l2, l3) a+  where+  type+    SplitBorrow (l1, l2, l3) bk α a =+      (Borrow bk α (ValueOf l1), Borrow bk α (ValueOf l2), Borrow bk α (ValueOf l3))+  splitRecord (RecLab, RecLab, RecLab) = Unsafe.toLinear \r ->+    ( unsafeMapAlias (Unsafe.toLinear (getField @f1)) r+    , unsafeMapAlias (Unsafe.toLinear (getField @f2)) r+    , unsafeMapAlias (Unsafe.toLinear (getField @f3)) r+    )++instance+  ( IsRecordLabel' a l1 f1 v1+  , IsRecordLabel' a l2 f2 v2+  , IsRecordLabel' a l3 f3 v3+  , IsRecordLabel' a l4 f4 v4+  , Distinct f1 f2+  , Distinct f1 f3+  , Distinct f1 f4+  , Distinct f2 f3+  , Distinct f2 f4+  , Distinct f3 f4+  ) =>+  RecordEliminator (l1, l2, l3, l4) a+  where+  type+    SplitBorrow (l1, l2, l3, l4) bk α a =+      (Borrow bk α (ValueOf l1), Borrow bk α (ValueOf l2), Borrow bk α (ValueOf l3), Borrow bk α (ValueOf l4))+  splitRecord (RecLab, RecLab, RecLab, RecLab) = Unsafe.toLinear \r ->+    ( unsafeMapAlias (Unsafe.toLinear (getField @f1)) r+    , unsafeMapAlias (Unsafe.toLinear (getField @f2)) r+    , unsafeMapAlias (Unsafe.toLinear (getField @f3)) r+    , unsafeMapAlias (Unsafe.toLinear (getField @f4)) r+    )++instance+  ( IsRecordLabel' a l1 f1 v1+  , IsRecordLabel' a l2 f2 v2+  , IsRecordLabel' a l3 f3 v3+  , IsRecordLabel' a l4 f4 v4+  , IsRecordLabel' a l5 f5 v5+  , Distinct f1 f2+  , Distinct f1 f3+  , Distinct f1 f4+  , Distinct f1 f5+  , Distinct f2 f3+  , Distinct f2 f4+  , Distinct f2 f5+  , Distinct f3 f4+  , Distinct f3 f5+  , Distinct f4 f5+  ) =>+  RecordEliminator (l1, l2, l3, l4, l5) a+  where+  type+    SplitBorrow (l1, l2, l3, l4, l5) bk α a =+      ( Borrow bk α (ValueOf l1)+      , Borrow bk α (ValueOf l2)+      , Borrow bk α (ValueOf l3)+      , Borrow bk α (ValueOf l4)+      , Borrow bk α (ValueOf l5)+      )+  splitRecord (RecLab, RecLab, RecLab, RecLab, RecLab) = Unsafe.toLinear \r ->+    ( unsafeMapAlias (Unsafe.toLinear (getField @f1)) r+    , unsafeMapAlias (Unsafe.toLinear (getField @f2)) r+    , unsafeMapAlias (Unsafe.toLinear (getField @f3)) r+    , unsafeMapAlias (Unsafe.toLinear (getField @f4)) r+    , unsafeMapAlias (Unsafe.toLinear (getField @f5)) r+    )++type data Fun+  = BorrowOf BorrowKind Lifetime+  | RecordLabelOf Type++type Apply :: Fun -> (Symbol, Type) -> Type+type family Apply fun a where+  Apply (BorrowOf bk α) kv = Borrow bk α (Snd kv)+  Apply (RecordLabelOf r) kv = RecordLabel' r '(Fst kv, Snd kv)++type LabelsOrBorrows :: Fun -> [(Symbol, Type)] -> Type+data LabelsOrBorrows h xs where+  RNil :: LabelsOrBorrows h '[]+  (:#-) :: Apply h '(k, v) %1 -> LabelsOrBorrows h xs %1 -> LabelsOrBorrows h ('(k, v) ': xs)++{- |+Heterogeneous record labels. If the record type @a@ is clear from the context, you can construct it with '(':#-')' and 'RNil' with @OverloadedLabels@ extension:++@+  data MyRecord = MyRecord { foo :: Int, bar :: String, buz :: Bool }+  myLabels :: 'RecordLabels' MyRecord _+  myLabels = #foo ':#-' #bar ':#-' #buz ':#-' 'RNil'+@+-}+type RecordLabels a fs = LabelsOrBorrows (RecordLabelOf a) fs++{- |+Heterogeneous FieldBorrows. If the record type @a@ is clear from the context, you can construct it with '(':#-')' and 'RNil' with @OverloadedLabels@ extension:++@+data MyRecord = MyRecord { foo :: Int, bar :: String, buz :: Bool }++mutRec :: t'Control.Monad.Pure.Mut' α MyRecord+mutRec = ...++buzMut ':#-' fooMut ':#-' 'RNil' = mutRec '.@' #buz ':#-' #foo ':#-' 'RNil'+@+-}+type FieldBorrows bk α fs = LabelsOrBorrows (BorrowOf bk α) fs++instance Affine (LabelsOrBorrows h xs) where+  aff = unsafeAff+  {-# INLINE aff #-}++deriving via+  AsAffine (LabelsOrBorrows h xs)+  instance+    Consumable (LabelsOrBorrows h xs)++infixr 5 :#-++instance+  (IsUnique fvs, label ~ RecordLabelOf a) =>+  RecordEliminator (LabelsOrBorrows label fvs) a+  where+  type SplitBorrow (LabelsOrBorrows label fvs) bk α a = LabelsOrBorrows (BorrowOf bk α) fvs+  splitRecord = Unsafe.toLinear \case+    RNil -> (`lseq` RNil)+    lab :#- xs -> Unsafe.toLinear \r ->+      splitRecord lab r :#- splitRecord xs r+  {-# INLINE splitRecord #-}++type family All_ c xs :: Constraint where+  All_ c '[] = ()+  All_ c (x ': xs) = (c x, All c xs)++class (All_ c xs) => All c xs++instance All c '[]++instance (c x, All c xs) => All c (x ': xs)++type IsUnique :: [(Symbol, Type)] -> Constraint++type family IsUnique_ xs :: Constraint where+  IsUnique_ '[] = ()+  IsUnique_ (kv ': xs) = (All (Distinct (Fst kv)) (MapFst xs), IsUnique xs)++class (IsUnique_ xs) => IsUnique xs++instance IsUnique '[]++instance (All (Distinct (Fst kv)) (MapFst xs), IsUnique xs) => IsUnique (kv ': xs)++type family MapFst xs where+  MapFst '[] = '[]+  MapFst ('(k, v) ': xs) = k ': MapFst xs
+ src/Data/Record/Linear/Borrow/Experimental/Split.hs view
@@ -0,0 +1,320 @@+{-# LANGUAGE AllowAmbiguousTypes #-}+{-# LANGUAGE BlockArguments #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE DeriveAnyClass #-}+{-# LANGUAGE DerivingStrategies #-}+{-# LANGUAGE FunctionalDependencies #-}+{-# LANGUAGE KindSignatures #-}+{-# LANGUAGE LinearTypes #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE OverloadedLabels #-}+{-# LANGUAGE PolyKinds #-}+{-# LANGUAGE QuantifiedConstraints #-}+{-# LANGUAGE TemplateHaskell #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE UnboxedTuples #-}+{-# LANGUAGE UndecidableInstances #-}+{-# LANGUAGE UndecidableSuperClasses #-}+{-# LANGUAGE UnliftedNewtypes #-}+{-# LANGUAGE NoImplicitPrelude #-}+{-# OPTIONS_GHC -Wno-redundant-constraints #-}++{- |+An experimental module for splitting a borrow of a record gradually and partially.+To be used when you need to access more than one fields of a borrowed record, and borrow-out each field as you go.+If you can just pattern match on the record borrow once, consider using "Data.Record.Linear.Borrow.Experimental.PatternMatch".++The API is subject to future change.+-}+module Data.Record.Linear.Borrow.Experimental.Split (+  -- * Label Type+  RecordLabel (),++  -- * Single Field Accessor+  (.#),++  -- * #split# Splitting a record borrow into pieces+  -- $record-splitting++  -- ** APIs+  splitRecord,+  SplitRecord (),+  SplittableRecord (),+  (-#),+  (+#),+  (!#),+) where++import Control.Monad.Borrow.Pure.BO.Internal+import Control.Monad.Borrow.Pure.Lifetime+import Data.Kind (Constraint)+import GHC.Base (Multiplicity (..), TYPE, Type)+import GHC.OverloadedLabels (IsLabel (..))+import GHC.Records (HasField (..))+import GHC.TypeError (ErrorMessage (..), Unsatisfiable)+import GHC.TypeLits (Symbol, TypeError)+import Generics.Linear.TH+import Prelude.Linear hiding (All)+import Prelude.Linear.Generically qualified as GL+import Unsafe.Linear qualified as Unsafe++{- |+@'RecordLabel' r field a@ witnesses that the record type @r@ has a field named @field@ of type @a@.+To be used as a label argument for '(.#)', '(-#)', '(+#)', and '(!#)'.++The record label is usually constructed by overloaded labels as `#field` under `OverloadedLabels` extension.+-}+type RecordLabel :: TYPE rep -> Symbol -> Type -> Type+data RecordLabel r field a where+  RecLab :: (HasField field r a) => RecordLabel r field a++instance (HasField field r a, field ~ field') => IsLabel field (RecordLabel r field' a) where+  fromLabel = RecLab+  {-# INLINE fromLabel #-}++{- |+Borrow-level field accessor.+@record '.#' #field@ returns a borrow of the @field@ of the @record@ of the same kind.++@+{\-# LANGUAGE OverloadedLabels #-\}+data MyRecord = MyRecord {field :: Ref Int, otherField :: Vector String}++recordBor :: 'Borrow' bk α MyRecord+recordBor = ...++fieldOfRecordBor :: 'Borrow' bk α (Ref Int)+fieldOfRecordBor = recordBor '.#' #field++otherFieldOfRecordBor :: 'Borrow' bk α (Vector String)+otherFieldOfRecordBor = recordBor '.#' #otherField+@++In above example, we annotate type of the divided field borows for clarity, but the type can be inferred by the record type and labels.++For more complex, partial splitting of a record, see [Splitting a record borrow into pieces](#split) for more detail.+-}+(.#) ::+  forall field r a k α.+  Borrow k α r %1 ->+  RecordLabel r field a ->+  Borrow k α a+UnsafeAlias !r .# RecLab = UnsafeAlias $! Unsafe.toLinear (getField @field @r @a) r++infixl 9 .#++type family Lookup l ls where+  Lookup l '[] = 'Nothing+  Lookup l ('(l, v) ': xs) = 'Just v+  Lookup l ('(l', v) ': xs) = Lookup l xs++type family Delete l ls where+  Delete _ '[] = '[]+  Delete l ('(l, v) ': ls) = ls+  Delete l ('(l', v) ': ls) = '(l', v) ': Delete l ls++{- $record-splitting++== Overview++'(.#)' is handy when you need only one field of a borrowed record, but not applicable when you need to access more than one fields.+For that purpose, we provide 'SplitRecord' machinery and associated combinators '(-#)', '(+#)', and '(!#)' for splitting a borrow of a record into borrows of its fields.++In such cases, however, we must ensure that each field of a record borrow is split out @at most once@.+Here, @'SplitRecord' a bk α fs@ comes int play: it is representationally same as @'Borrow' bk α a@, but only the fields in @fs@ remains unsplit.+That is, a field is borrowed by splitting combinator only if it remains in @fs@ type parameter, and the field is removed from @fs@ after splitting.++A record type can be converted into a 'SplitRecord' by 'splitRecord' function, which requires 'SplittableRecord' instance for the record type.+This can be derived generically by deriving 'GL.Generic' and then 'SplittableRecord' for the record type, as follows:++@+{\-# LANGUAGE TemplateHaskell, DataKinds, TypeFamilies, LinearTypes #-\}+import Generics.Linear.TH ('deriveGeneric')++data MyRecord = MyRecord {field :: 'Data.Ref.Linear.Ref' 'Int', otherField :: 'Data.Vector.Mutable.Linear.Borrow.Vector' 'String'}++'deriveGeneric' ''MyRecord++deriving anyclass instance 'SplittableRecord' MyRecord+@++Once we have 'SplittableRecord' instance derived, we can now split a record borrow partially, step-by-step using '(-#)', '(+#)', and '(!#)' combinators.+Through out this documentation, suppose we have the following record borrow in scope:++@+recordBor :: 'Mut' α MyRecord++splitRec ::+  'SplitRecord' MyRecord v'Mut' α+      '[ '("field", '( 'One, Ref Int)), '("otherField", '( 'One, Vector String))]+splitRec = splitRecord recordBor+@++== Borrows-out a linear field++When you want to borrow-out a single linear field from the record, you can use '(-#)' combinator, as follows:++@+fieldBor :: 'Mut' α (Ref Int)+restBor :: 'SplitRecord' MyRecord Mut α '[ '(otherField, '( 'One, Vector String)))]+(fieldBor, restSplit) = splitRec '-#' #field+@++Here, the borrow to the @field@ of @splitRec@ is borrowed out as @fieldBor@, and the remaining borrow is represented by @restSplit@, where only @otherField@ remain unsplit.+We can no longer borrow-out @field@ from @restSplit@ by the type constraints.++== Consuming a split record++When you no longer need to borrow any field of a split record, you can just 'consume' a split record, or call '(!#)' to borrow out a single field from the split record and discard the rest of the record borrow, as follows:++@+otherFieldBor :: Mut α (Vector String)+otherFieldBor = restSplit '!#' #otherField+@++'(!#)' is analogous to '(.#)', but it acts on 'SplitRecord' instead of borrow of a record.+-}++{- |+@'SplitRecord' a bk α fs@ represents a borrow of a value of type @a@ of borrow kind @bk@ (i.e. 'Share' or 'Mut') for lifetime @α@ with @fs@ remains unsplit.+That is, if the field @f@ is removed by some combinators like '(-#)', then the resulting 'SplitRecord' will have @f@ removed from the @fs@ type-level list.++At any time, you can 'consume' 'SplitRecord' when the remaining fields are no longer of interest.+-}+type SplitRecord :: Type -> BorrowKind -> Lifetime -> [(Symbol, (Multiplicity, Type))] -> Type+newtype SplitRecord a bk α s = SplitRecord (Borrow bk α a)++instance Consumable (SplitRecord a bk α fs) where+  consume (SplitRecord a) = consume a+  {-# INLINE consume #-}++class (Lookup l xs ~ 'Just v) => Member l xs v | l xs -> v++instance (Lookup l xs ~ 'Just v) => Member l xs v++type All_ :: (k -> Constraint) -> [k] -> Constraint+type family All_ c xs where+  All_ c '[] = ()+  All_ c (x ': xs) = (c x, All c xs)++type All :: (k -> Constraint) -> [k] -> Constraint+class (All_ c xs) => All c xs++instance All c '[]++instance (c x, All c xs) => All c (x ': xs)++type family IsFieldOf_ a xs where+  IsFieldOf_ a '(l, '(_, v)) = HasField l a v++class (IsFieldOf_ a x) => IsFieldOf a x++instance (HasField l a v) => IsFieldOf a '(l, '(m, v))++type SplittableRecord :: Type -> Constraint+class (All (IsFieldOf a) (Fields a)) => SplittableRecord a where+  type Fields a :: [(Symbol, (Multiplicity, Type))]+  type Fields a = GFields (GL.Rep a)++type GSplittableRecord :: (Type -> Type) -> Constraint+class GSplittableRecord f where+  type GFields f :: [(Symbol, (Multiplicity, Type))]++type family ls ++ rs where+  '[] ++ rs = rs+  (x ': xs) ++ rs = x ': (xs ++ rs)++instance+  (Unsatisfiable ('Text "A union type cannot be a splittable record")) =>+  GSplittableRecord (f GL.:+: g)+  where+  type GFields (f GL.:+: g) = TypeError ('Text "A union type cannot be a splittable record")++instance (GSplittableRecord f) => GSplittableRecord (GL.D1 i f) where+  type GFields (GL.D1 i f) = GFields f++instance (GSplittableRecord f) => GSplittableRecord (GL.C1 i f) where+  type GFields (GL.C1 i f) = GFields f++instance+  (Unsatisfiable ('Text "A record field must have a name")) =>+  GSplittableRecord (GL.S1 ('GL.MetaSel 'Nothing unp str str') (GL.K1 i c))+  where+  type GFields (GL.S1 ('GL.MetaSel 'Nothing unp str str') (GL.K1 i c)) = TypeError ('Text "A record field must have a name")++type MultOf :: Type -> Multiplicity+type family MultOf c where+  MultOf (Ur x) = 'Many+  MultOf x = 'One++instance+  (GSplittableRecord f) =>+  GSplittableRecord (GL.S1 ('GL.MetaSel ('Just name) unp str str') (GL.K1 i c))+  where+  type GFields (GL.S1 ('GL.MetaSel ('Just name) unp str str') (GL.K1 i c)) = '[ '(name, '((MultOf c), c))]++instance (GSplittableRecord f, GSplittableRecord g) => GSplittableRecord (f GL.:*: g) where+  type GFields (f GL.:*: g) = GFields f ++ GFields g++-- | Start subdividing a borrow of a record.+splitRecord :: (SplittableRecord a) => Borrow bk α a %m -> SplitRecord a bk α (Fields a)+splitRecord !bor = SplitRecord bor+{-# INLINE splitRecord #-}++{- |+Splitting a linear field from a borrow of a record.+@record '-#' #field@  returns a pair of the borrow of a split field and remaining split record, where @field@ is removed from the type-level list of the remaining split record.++Mnemonic: '(-#)' /subtracts/ the field from the record.+-}+(-#) ::+  (SplittableRecord a, Lookup field fs ~ 'Just '( 'One, x)) =>+  SplitRecord a bk α fs %m ->+  RecordLabel a field x ->+  (Borrow bk α x, SplitRecord a bk α (Delete field fs))+(-#) = Unsafe.toLinear \(SplitRecord !bor) lab ->+  let !fieldBor = bor .# lab+      !restBor = SplitRecord bor+   in (fieldBor, restBor)+{-# INLINE (-#) #-}++{- |+Extracting the borrow to the single linear field form a borrow of a record.+@record '!#' #field@ returns a borrow of the @field@ of the @record@, discarding the borrow to the rest of the record.++Mnemonic: '(!#)' /destructs/ a borrow of a record to that of a single field.+-}+(!#) ::+  (SplittableRecord a, Lookup field fs ~ 'Just '( 'One, x)) =>+  SplitRecord a bk α fs %m ->+  RecordLabel a field x ->+  Borrow bk α x+(!#) = Unsafe.toLinear \(SplitRecord !bor) lab ->+  let !fieldBor = bor .# lab+   in bor `lseq` fieldBor+{-# INLINE (!#) #-}++{- |+Skimming the value of a nonlinear (unrestricted) field.+@record '+#' #field@ returns a pair of the /value/ of the @field@ of the @record@ and the original split record.+The returned value of @field@ is wrapped by 'Ur' and can be used more than once.++Mnenonic: '(+#)' you can use nonlinear field /more/ (@+@) than once.+-}+(+#) ::+  (SplittableRecord a, Lookup field fs ~ 'Just '( 'Many, Ur x)) =>+  SplitRecord a bk α fs %m ->+  RecordLabel a field (Ur x) ->+  (Ur x, SplitRecord a bk α fs)+(+#) = Unsafe.toLinear \recd@(SplitRecord !bor) lab ->+  let UnsafeAlias !field = bor .# lab+   in (field, recd)+{-# INLINE (+#) #-}++infix 9 -#, +#, !#++data Hoge = Hoge {foo :: Int, bar :: Ur String, buz :: Bool}++deriveGeneric ''Hoge++deriving anyclass instance SplittableRecord Hoge
+ src/Data/Ref/Linear.hs view
@@ -0,0 +1,97 @@+{-# LANGUAGE BlockArguments #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE MagicHash #-}+{-# LANGUAGE QualifiedDo #-}+{-# LANGUAGE RoleAnnotations #-}+{-# LANGUAGE UnboxedTuples #-}+{-# LANGUAGE UnliftedNewtypes #-}+{-# LANGUAGE NoImplicitPrelude #-}+{-# OPTIONS_GHC -Wno-name-shadowing #-}++module Data.Ref.Linear (+  Ref,+  new,+  free,+  unsafeReadRef,+  unsafeWriteRef,+  atomicModify,+  atomicModify_,+) where++import Control.Functor.Linear qualified as Control+import Control.Monad.Borrow.Pure.Affine+import Control.Monad.Borrow.Pure.Affine.Unsafe (unsafeAff)+import Control.Monad.Borrow.Pure.BO+import Control.Monad.Borrow.Pure.BO.Unsafe (Alias (..))+import Control.Monad.Borrow.Pure.Clone+import Control.Monad.Borrow.Pure.Copyable+import Control.Monad.Borrow.Pure.Lifetime.Token.Internal (+  LinearOnly (..),+  LinearOnlyWitness (..),+ )+import Data.Ref.Linear.Unlifted+import GHC.TypeError+import Prelude.Linear (Consumable (..), Dupable (..))+import Prelude.Linear qualified as PL+import Unsafe.Linear qualified as Unsafe++-- | Linearly owned mutable reference.+data Ref a = Ref (Ref# a)++type role Ref nominal++new :: a %1 -> Linearly %1 -> Ref a+{-# INLINE new #-}+new a lin = Ref (newRef# a lin)++instance LinearOnly (Ref a) where+  linearOnly = UnsafeLinearOnly++instance (Consumable a) => Consumable (Ref a) where+  consume = consume PL.. free+  {-# INLINE consume #-}++instance (PL.Dupable a) => PL.Dupable (Ref a) where+  dup2 = Unsafe.toLinear \ !v ->+    withLinearly v PL.& \(l, !v) ->+      let !v2 = Unsafe.toLinear (\(!_, !v) -> v) PL.$ dup2 PL.$ free v+       in (v, new v2 l)+  {-# INLINE dup2 #-}++instance Affine (Ref a) where+  aff = unsafeAff++atomicModify_ :: (a %1 -> a) %1 -> Ref a %1 -> Ref a+{-# INLINE atomicModify_ #-}+atomicModify_ f (Ref v) = Ref (atomicModify_# f v)++atomicModify :: (a %1 -> (b, a)) %1 -> Ref a %1 -> (b, Ref a)+{-# INLINE atomicModify #-}+atomicModify f (Ref v) = case atomicModify# f v of+  (# b, v' #) -> (b, Ref v')++free :: Ref a %1 -> a+{-# INLINE free #-}+free (Ref v) = freeRef# v++unsafeReadRef :: Ref a %1 -> (a, Ref a)+{-# INLINE unsafeReadRef #-}+unsafeReadRef (Ref v) = case unsafeReadRef# v of+  (# a, v' #) -> (a, Ref v')++unsafeWriteRef :: Ref a %1 -> a %1 -> Ref a+{-# INLINE unsafeWriteRef #-}+unsafeWriteRef (Ref v) a = Ref (unsafeWriteRef# v a)++instance+  (Unsatisfiable (ShowType (Ref a) :<>: Text " cannot be copied!")) =>+  Copyable (Ref a)+  where+  copy = unsatisfiable++instance (Dupable a) => Clone (Ref a) where+  clone = Unsafe.toLinear \(UnsafeAlias ref) -> Control.do+    !a <- Control.pure PL.$ free ref+    !a' <- Unsafe.toLinear (\(!_, !a') -> Control.pure a') PL.$ PL.dup a+    new a' Control.<$> askLinearly+  {-# INLINE clone #-}
+ src/Data/Ref/Linear/Borrow.hs view
@@ -0,0 +1,66 @@+{-# LANGUAGE BlockArguments #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE LinearTypes #-}+{-# LANGUAGE QualifiedDo #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE NoImplicitPrelude #-}+{-# OPTIONS_GHC -Wno-name-shadowing #-}+{-# OPTIONS_GHC -Wno-redundant-constraints #-}++{- |+A reference cell. To mutate, use as @'Mut' α ('Ref' a)@.+This module is inteted to be imported qualified.+-}+module Data.Ref.Linear.Borrow (+  Ref (),+  update,+  modify,+  swap,+  readShare,+  copyRef,+) where++import Control.Functor.Linear qualified as Control+import Control.Monad.Borrow.Pure.BO+import Control.Monad.Borrow.Pure.BO.Unsafe+import Control.Monad.Borrow.Pure.Copyable+import Control.Syntax.DataFlow qualified as DataFlow+import Data.Ref.Linear (Ref)+import Data.Ref.Linear qualified as Ref+import Prelude.Linear+import Unsafe.Linear qualified as Unsafe+import Prelude qualified as NonLinear++update :: (α >= β) => (a %1 -> BO β (b, a)) %1 -> Mut α (Ref a) %1 -> BO β (b, Mut α (Ref a))+{-# INLINE update #-}+update f (UnsafeAlias mv) = DataFlow.do+  -- NOTE: as there is only one reference to @'Ref' a@, we can just use read/write+  -- instead of 'MutVar.atomicModify' (which requires pure function) while retaining atomicity.+  (!a, !mv) <- Ref.unsafeReadRef mv+  f a Control.<&> \(!b, !a) -> DataFlow.do+    !mv <- Ref.unsafeWriteRef mv a+    (b, UnsafeAlias mv)++modify :: (α >= β) => (a %1 -> a) %1 -> Mut α (Ref a) %1 -> BO β (Mut α (Ref a))+modify f ma = Control.do+  ((), ma) <- update (Control.pure . ((),) . f) ma+  Control.pure ma++swap :: (α >= β) => Mut α (Ref a) %1 -> Mut α (Ref a) %1 -> BO β (Mut α (Ref a), Mut α (Ref a))+{-# INLINE swap #-}+swap ma ma' =+  flip update ma' \ !a' -> Control.do+    (a, ma) <- update (\ !a -> Control.pure (a, a')) ma+    Control.pure (ma, a)++readShare :: (α >= β) => Share α (Ref a) %1 -> BO β (Ur (Share α a))+{-# INLINE readShare #-}+readShare = Unsafe.toLinear \(UnsafeAlias mv) ->+  Control.pure $ Ur $! UnsafeAlias NonLinear.$! NonLinear.fst $! Ref.unsafeReadRef mv++copyRef :: (Copyable a, α >= β) => Borrow k α (Ref a) %1 -> BO β a+{-# INLINE copyRef #-}+copyRef bor =+  share bor & \(Ur bor) -> Control.do+    Ur !shr <- readShare bor+    Control.pure $! copy shr
+ src/Data/Ref/Linear/Unlifted.hs view
@@ -0,0 +1,76 @@+{-# LANGUAGE BlockArguments #-}+{-# LANGUAGE MagicHash #-}+{-# LANGUAGE RoleAnnotations #-}+{-# LANGUAGE UnboxedTuples #-}+{-# LANGUAGE UnliftedNewtypes #-}+{-# LANGUAGE NoImplicitPrelude #-}+{-# OPTIONS_GHC -Wno-name-shadowing #-}++module Data.Ref.Linear.Unlifted (+  Ref#,+  newRef#,+  freeRef#,+  unsafeReadRef#,+  unsafeWriteRef#,+  atomicModify_#,+  atomicModify#,+) where++import Control.Monad.Borrow.Pure.Lifetime.Token+import Control.Monad.Borrow.Pure.Lifetime.Token.Unsafe (LinearOnly (..), LinearOnlyWitness (..))+import Control.Monad.Borrow.Pure.Utils (lseq#)+import GHC.Exts+import GHC.Exts qualified as GHC+import Prelude.Linear+import Unsafe.Linear qualified as Unsafe++newtype Ref# a = Ref# (MutVar# RealWorld a)++type role Ref# nominal++newRef# :: a %1 -> Linearly %1 -> Ref# a+{-# NOINLINE newRef# #-}+newRef# = GHC.noinline $ Unsafe.toLinear $ \a lin ->+  lin+    `lseq#` GHC.runRW# \s ->+      case GHC.newMutVar# a s of+        (# !_, !v #) -> Ref# v++-- | This is unsafe, because the ownership of 'a' is duplicated.+unsafeReadRef# :: Ref# a %1 -> (# a, Ref# a #)+unsafeReadRef# = GHC.noinline $ Unsafe.toLinear \(Ref# !mv) ->+  runRW# \s ->+    case GHC.readMutVar# mv s of+      (# !_, !a #) -> (# a, Ref# mv #)++-- | This is unsafe, because the ownership of original 'a' is dropped.+unsafeWriteRef# :: Ref# a %1 -> a %1 -> Ref# a+{-# NOINLINE unsafeWriteRef# #-}+unsafeWriteRef# = GHC.noinline $ Unsafe.toLinear2 \(Ref# mv) !a ->+  runRW# \s ->+    case GHC.writeMutVar# mv a s of+      _ -> Ref# mv++freeRef# :: Ref# a %1 -> a+{-# NOINLINE freeRef# #-}+freeRef# = Unsafe.toLinear \(Ref# a) ->+  runRW# \s ->+    case GHC.readMutVar# a s of+      (# _, !a #) -> a++instance LinearOnly (Ref# a) where+  linearOnly = UnsafeLinearOnly++atomicModify_# :: (a %1 -> a) %1 -> Ref# a %1 -> Ref# a+{-# NOINLINE atomicModify_# #-}+atomicModify_# = GHC.noinline $ Unsafe.toLinear2 \f (Ref# mv) ->+  runRW# \s ->+    case GHC.atomicModifyMutVar2# mv (Unsafe.toLinear f) s of+      (# _, !_, !_ #) -> Ref# mv++atomicModify# :: (a %1 -> (b, a)) %1 -> Ref# a %1 -> (# b, Ref# a #)+{-# NOINLINE atomicModify# #-}+atomicModify# = GHC.noinline $ Unsafe.toLinear2 \f (Ref# mv) ->+  runRW# \s ->+    case GHC.atomicModifyMutVar2# mv (Unsafe.toLinear f) s of+      (# _, !_, (!b, !_) #) -> (# b, Ref# mv #)
+ src/Data/Unique/Linear.hs view
@@ -0,0 +1,96 @@+{-# LANGUAGE BlockArguments #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE DerivingVia #-}+{-# LANGUAGE ImpredicativeTypes #-}+{-# LANGUAGE LambdaCase #-}+{-# LANGUAGE LinearTypes #-}+{-# LANGUAGE PartialTypeSignatures #-}+{-# LANGUAGE QualifiedDo #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TemplateHaskell #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE ViewPatterns #-}+{-# LANGUAGE NoImplicitPrelude #-}+{-# OPTIONS_GHC -Wno-name-shadowing #-}+{-# OPTIONS_GHC -Wno-partial-type-signatures #-}++module Data.Unique.Linear (+  UniqueSource,+  new,+  sample,+  split,+  splitN,+  splitV,+  split3,+  split4,+  split5,+) where++import Control.Monad.Borrow.Pure.Lifetime.Token (Linearly)+import Data.Proxy (Proxy (Proxy))+import Data.V.Linear.Internal hiding (consume)+import Data.Vector qualified as V+import GHC.TypeNats (KnownNat, natVal)+import Prelude.Linear+import Unsafe.Linear qualified as Unsafe+import Prelude qualified as NL++data UniqueSource where+  -- | Seed, multiplier, constant.+  UniqueSource :: !Int %1 -> !Int %1 -> !Int %1 -> UniqueSource+  deriving (Show, NL.Eq, NL.Ord)++instance Consumable UniqueSource where+  consume (UniqueSource seed multiplier constant) =+    seed `lseq`+      multiplier `lseq`+        consume constant+  {-# INLINE consume #-}++new :: Linearly %1 -> UniqueSource+new lin = lin `lseq` UniqueSource 0 1 0++sample :: UniqueSource %1 -> (Int, UniqueSource)+sample =+  Unsafe.toLinear \(UniqueSource x a b) ->+    (x * a + b, UniqueSource (x + 1) a b)++{- | Split a 'UniqueSource' into two, each with non-overlapping ranges.++See also 'splitN' and 'splitV'.+-}+split :: UniqueSource %1 -> (UniqueSource, UniqueSource)+split =+  Unsafe.toLinear \(UniqueSource x a b) ->+    (x `quotRem` 2) & \(q, r) ->+      if r == 0+        then+          ( UniqueSource q (a * 2) b+          , UniqueSource q (a * 2) (a + b)+          )+        else+          ( UniqueSource q (a * 2) (a + b)+          , UniqueSource (q + 1) (a * 2) b+          )++splitN :: Int -> UniqueSource %1 -> V.Vector UniqueSource+{-# INLINE splitN #-}+splitN n = Unsafe.toLinear \(UniqueSource x a b) ->+  let (q, r) = x `quotRem` n+   in V.generate n \((+ r) -> i) ->+        let (offx, offb) = i `quotRem` n+            !x = q + offx+         in UniqueSource x (a * n) (b + a * offb)++splitV :: forall n. (KnownNat n) => UniqueSource %1 -> V n UniqueSource+{-# INLINE splitV #-}+splitV = V . splitN (fromIntegral $ natVal $ Proxy @n)++split3 :: UniqueSource -> (UniqueSource, UniqueSource, UniqueSource)+split3 = elim (,,) . splitV++split4 :: UniqueSource -> (UniqueSource, UniqueSource, UniqueSource, UniqueSource)+split4 = elim (,,,) . splitV++split5 :: UniqueSource -> (UniqueSource, UniqueSource, UniqueSource, UniqueSource, UniqueSource)+split5 = elim (,,,,) . splitV
+ src/Data/Vector/Mutable/Linear/Borrow.hs view
@@ -0,0 +1,402 @@+{-# LANGUAGE BlockArguments #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE ImpredicativeTypes #-}+{-# LANGUAGE LambdaCase #-}+{-# LANGUAGE MultiWayIf #-}+{-# LANGUAGE OverloadedRecordDot #-}+{-# LANGUAGE QualifiedDo #-}+{-# LANGUAGE NoImplicitPrelude #-}+{-# OPTIONS_GHC -Wno-name-shadowing #-}+{-# OPTIONS_GHC -Wno-partial-type-signatures #-}+{-# OPTIONS_GHC -Wno-redundant-constraints #-}++module Data.Vector.Mutable.Linear.Borrow (+  Vector,+  empty,+  constant,+  fromList,+  fromVector,+  unsafeFromVector,+  fromMutable,+  unsafeFromMutable,+  toVector,+  toList,+  size,+  get,+  unsafeGet,+  set,+  unsafeSet,+  update,+  unsafeUpdate,+  modify,+  head,+  unsafeHead,+  last,+  unsafeLast,+  indicesMut,+  unsafeIndicesMut,+  splitAt,+  swap,+  unsafeSwap,+  copyAt,+  copyAtMut,+  inplace,++  -- * An example algorithm implementations+  qsort,++  -- ** Internal functions+  divide,+) where++import Control.Functor.Linear qualified as Control+import Control.Monad qualified as NonLinear+import Control.Monad.Borrow.Pure.BO+import Control.Monad.Borrow.Pure.BO.Unsafe+import Control.Monad.Borrow.Pure.Clone+import Control.Monad.Borrow.Pure.Copyable+import Control.Monad.Borrow.Pure.Lifetime.Token.Unsafe (+  LinearOnly (..),+  LinearOnlyWitness (..),+ )+import Control.Monad.Borrow.Pure.Utils+import Control.Monad.ST.Strict (ST)+import Control.Syntax.DataFlow qualified as DataFlow+import Data.Function qualified as NonLinear+import Data.Functor.Linear qualified as Data+import Data.IntSet qualified as IntSet+import Data.Unrestricted.Linear qualified as Ur+import Data.Vector qualified as V+import Data.Vector.Mutable (RealWorld)+import Data.Vector.Mutable qualified as MV+import GHC.Exts qualified as GHC+import GHC.IO (unsafePerformIO)+import GHC.Stack (HasCallStack)+import GHC.TypeError+import Prelude.Linear hiding (head, last, splitAt)+import Unsafe.Linear qualified as Unsafe+import Prelude qualified as NonLinear++{- |+Linearly owned mutable vector.+Contrary to those in @linear-base@, our 'Vector' owns every element @linearly@.+This is because Pure Borrow can now treat nested mutability safely, so we must allow mutable values to be stored inside 'Vector'.+This manifests in the type of 'set' - it returns the old value, which MUST NOT drop in favour of the new value.+-}+newtype Vector a = Vector {content :: MV.MVector RealWorld a}++empty :: Linearly %1 -> Vector a+{-# NOINLINE empty #-}+empty =+  GHC.noinline \l ->+    l `lseq` do+      Vector (unsafePerformIO $ MV.new 0)++constant :: Int -> a -> Linearly %1 -> Vector a+{-# NOINLINE constant #-}+constant = GHC.noinline \n a l ->+  l `lseq` do+    Vector $!+      unsafePerformIO $!+        MV.replicate n a++fromList :: [a] %1 -> Linearly %1 -> Vector a+{-# NOINLINE fromList #-}+fromList = GHC.noinline $ Unsafe.toLinear \as l ->+  l `lseq` do+    Vector $!+      unsafePerformIO $!+        Unsafe.toLinear V.unsafeThaw $!+          Unsafe.toLinear V.fromList as++-- | Convert a 'V.Vector' (from @vector@ package) to a 'Vector'.+fromVector :: V.Vector a -> Linearly %1 -> Vector a+{-# NOINLINE fromVector #-}+fromVector = GHC.noinline $ Unsafe.toLinear \v l ->+  l `lseq` do+    Vector $!+      unsafePerformIO $!+        Unsafe.toLinear V.thaw v++-- | /O(n)/. Clone a 'V.MVector' from @vector@ package to a 'Vector'.+fromMutable :: MV.MVector s a %1 -> Linearly %1 -> Vector a+{-# NOINLINE fromMutable #-}+fromMutable = GHC.noinline $ Unsafe.toLinear \v l ->+  l `lseq` do+    Vector $!+      unsafePerformIO $!+        Unsafe.toLinear MV.clone (Unsafe.coerce v)++unsafeFromMutable :: MV.MVector s a %1 -> Linearly %1 -> Vector a+unsafeFromMutable v lin =+  lin `lseq` Vector (Unsafe.coerce v)++{-+Note [Unrestricted Materialization of Vector]+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~+We impose 'Copyable' on 'toVector' and 'toList' to ensure elements doesn't bare any essentially linear contents inside, but we don't make use of the constraint internally.+Is it a cheating? Maybe. Think hard about it.+-}++-- | /O(1)/. Freezes @'Vector' a@ to @'V.Vector' a@ from @vector@ package, /without/ copying.+toVector ::+  -- See Note [Unrestricted Materialization of Vector].+  (Copyable a) =>+  Vector a %1 -> Ur (V.Vector a)+{-# NOINLINE toVector #-}+toVector = GHC.noinline $+  Unsafe.toLinear \(Vector v) -> Ur $ unsafePerformIO $ V.unsafeFreeze v++-- Same applies to 'Copyable' here, as in 'toVector'.+toList ::+  -- See Note [Unrestricted Materialization of Vector].+  (Copyable a) =>+  Vector a %1 -> Ur [a]+{-# INLINE toList #-}+toList = Ur.lift V.toList . toVector++{- | Unsafely thaws 'V.Vector' (from @vector@ package) to a 'Vector',+reusing the same memory.+This is highly unsafe+-}+unsafeFromVector :: V.Vector a %1 -> Linearly %1 -> Vector a+{-# NOINLINE unsafeFromVector #-}+unsafeFromVector = Unsafe.toLinear \v l ->+  l `lseq` GHC.noinline do+    Vector $!+      unsafePerformIO $!+        V.unsafeThaw v++size :: Borrow bk α (Vector a) %1 -> (Ur Int, Borrow bk α (Vector a))+{-# INLINE size #-}+size =+  unsafeUnalias >>> Unsafe.toLinear \(Vector v) ->+    (move (MV.length v), UnsafeAlias (Vector v))++{- |+@'set' i a v@ sets the @i@-th element of @v@ to @a@, and returns the old value alongside.+Note that @a@ is bound linearly.+-}+set :: (HasCallStack, α >= β) => Int -> a %1 -> Mut α (Vector a) %1 -> BO β (a, Mut α (Vector a))+{-# INLINE set #-}+set i a v = DataFlow.do+  (len, v) <- size v+  case len of+    Ur len ->+      if i < 0 || i >= len+        then error ("get: index " <> show i <> " out of bound: " <> show len) v a+        else unsafeSet i a v++-- | 'set' without bound check.+unsafeSet :: (α >= β) => Int -> a %1 -> Mut α (Vector a) %1 -> BO β (a, Mut α (Vector a))+unsafeSet = Unsafe.toLinear3 \i a mut@(UnsafeAlias (Vector v)) -> unsafeSystemIOToBO do+  old <- MV.unsafeRead v i+  MV.unsafeWrite v i a+  NonLinear.pure (old, mut)++-- | 'get' without bounds check.+unsafeGet :: (α >= β) => Int -> Borrow bk α (Vector a) %1 -> BO β (Borrow bk α a)+{-# INLINE unsafeGet #-}+unsafeGet i =+  Unsafe.toLinear \v ->+    unsafeUnalias v+      NonLinear.& \(Vector v) ->+        UnsafeAlias+          Control.<$> unsafeSystemIOToBO (MV.unsafeRead v i)++head :: (HasCallStack, α >= β) => Borrow bk α (Vector a) %1 -> BO β (Borrow bk α a)+{-# INLINE head #-}+head = get 0++unsafeHead :: (α >= β) => Borrow bk α (Vector a) %1 -> BO β (Borrow bk α a)+{-# INLINE unsafeHead #-}+unsafeHead = unsafeGet 0++unsafeLast :: (α >= β) => Borrow bk α (Vector a) %1 -> BO β (Borrow bk α a)+{-# INLINE unsafeLast #-}+unsafeLast v = DataFlow.do+  (len, v) <- size v+  case len of+    Ur len -> unsafeGet (len - 1) v++last :: (HasCallStack, α >= β) => Borrow bk α (Vector a) %1 -> BO β (Borrow bk α a)+{-# INLINE last #-}+last v = DataFlow.do+  (len, v) <- size v+  case len of+    Ur len+      | len > 0 -> unsafeGet (len - 1) v+      | otherwise -> error ("last: empty vector") v++get ::+  (HasCallStack, α >= β) =>+  Int -> Borrow bk α (Vector a) %1 -> BO β (Borrow bk α a)+{-# INLINE get #-}+get i v = DataFlow.do+  (len, v) <- size v+  case len of+    Ur len ->+      if i < 0 || i >= len+        then error ("get: index " <> show i <> " out of bound: " <> show len) v+        else unsafeGet i v++unsafeUpdate :: (α >= β) => Int -> (a %1 -> BO β (b, a)) %1 -> Mut α (Vector a) %1 -> BO β (b, Mut α (Vector a))+unsafeUpdate i = Unsafe.toLinear2 \k (UnsafeAlias v) -> Control.do+  a <- unsafeSystemIOToBO $ MV.unsafeRead (content v) i+  (b, a') <- k a+  () <- unsafeSystemIOToBO $ Unsafe.toLinear3 MV.unsafeWrite (content v) i a'+  Control.pure $ (b, UnsafeAlias v)++update :: (α >= β) => Int -> (a %1 -> BO β (b, a)) %1 -> Mut α (Vector a) %1 -> BO β (b, Mut α (Vector a))+update i k v = DataFlow.do+  (len, v) <- size v+  case len of+    Ur len ->+      if i < 0 || i >= len+        then error ("set: index " <> show i <> " out of bound: " <> show len) v k+        else unsafeUpdate i k v++modify :: (α >= β) => Int -> (a %1 -> a) %1 -> Mut α (Vector a) %1 -> BO β (Mut α (Vector a))+modify i f v = Control.do+  ((), ma) <- update i (Control.pure . ((),) . f) v+  Control.pure ma++{- | Get multiple elements at the given indices without bounds and duplication check.+For more safety, use 'indicesMut'.+-}+unsafeIndicesMut :: (α >= β) => Mut α (Vector a) %1 -> [Int] %1 -> BO β [Mut α a]+unsafeIndicesMut = Unsafe.toLinear \v is ->+  Data.traverse+    (\i -> move i & \(Ur i) -> unsafeGet i v)+    is++indicesMut :: (HasCallStack, α >= β) => Mut α (Vector a) %1 -> [Int] %1 -> BO β [Mut α a]+indicesMut = Unsafe.toLinear2 \v is ->+  case size v of+    (Ur len, v) ->+      if+        | any (\i -> move i & \(Ur i) -> i < 0 || i >= len) is ->+            error ("indicesMut: indices out of bound: " <> show is <> " for length " <> show len) v+        | NonLinear.length is > IntSet.size (IntSet.fromList is) ->+            error ("indicesMut: duplicate indices: " <> show is) v+        | otherwise -> unsafeIndicesMut v is++splitAt :: Int %1 -> Borrow bk α (Vector a) %1 -> (Borrow bk α (Vector a), Borrow bk α (Vector a))+{-# INLINE splitAt #-}+splitAt = Unsafe.toLinear2 \i (UnsafeAlias (Vector v)) ->+  let (v1, v2) = MV.splitAt i v+   in (UnsafeAlias (Vector v1), UnsafeAlias (Vector v2))++instance LinearOnly (Vector a) where+  linearOnly = UnsafeLinearOnly+  {-# INLINE linearOnly #-}++instance+  (Unsatisfiable (ShowType (Vector a) :<>: Text " cannot be copied!")) =>+  Copyable (Vector a)+  where+  copy = unsatisfiable++instance (Dupable a) => Clone (Vector a) where+  clone = Unsafe.toLinear \(UnsafeAlias (Vector v)) -> unsafeSystemIOToBO do+    let !n = MV.length v+    !new <- MV.new n+    let go !i = NonLinear.when (i < n) do+          x <- MV.unsafeRead v i+          let (!_, !x') = dup x+          MV.unsafeWrite new i x'+          go (i + 1)+    go 0+    NonLinear.pure (Vector new)+  {-# INLINE clone #-}++unsafeSwap :: (α >= β) => Mut α (Vector a) %1 -> Int -> Int -> BO β (Mut α (Vector a))+unsafeSwap = Unsafe.toLinear3 \(UnsafeAlias v) i j -> Control.do+  () <- unsafeSystemIOToBO $ MV.unsafeSwap v.content i j+  Control.pure $ UnsafeAlias v++swap :: (HasCallStack, α >= β) => Mut α (Vector a) %1 -> Int -> Int -> BO β (Mut α (Vector a))+swap v i j = DataFlow.do+  (len, v) <- size v+  case len of+    Ur len ->+      if i < 0 || i >= len || j < 0 || j >= len+        then error ("swap: index out of bound: " <> show (i, j) <> " for length " <> show len) v+        else unsafeSwap v i j++copyAt :: (Copyable a, α >= β) => Int -> Share α (Vector a) -> BO β (Ur a)+copyAt i v = Control.do Ur s <- move Control.<$> get i v; Control.pure $ Ur $ copy s++copyAtMut :: forall a α β. (Copyable a, α >= β) => Int -> Mut α (Vector a) %1 -> BO β (Ur a, Mut α (Vector a))+copyAtMut i v = upcast $ sharing @_ @α v $ copyAt i++-- | Applies an in-place mutation on 'V.MVector' from @vector@ package.+inplace ::+  (α >= β) =>+  (forall s. V.MVector s a -> ST s ()) %1 ->+  Mut α (Vector a) %1 ->+  BO β (Mut α (Vector a))+{-# INLINE inplace #-}+inplace = Unsafe.toLinear2 \f (UnsafeAlias v) -> Control.do+  !() <- unsafeSTToBO $ f $ content $ coerceLin v+  Control.pure (UnsafeAlias v)++{- | A simple parallel implementation of quicksort.+It uses a sequential divide-and-conquer when size <8,+and parallel divide-and-conquer with 'parBO' otherwise.++This is meant to be a demonstrative implementation and+not practical - you need a genuine parallel scheduler+to scale this up.+-}+qsort ::+  forall a α β.+  (Ord a, Copyable a, α >= β) =>+  {- | Cost for using parallelism. Halved after each recursive call,+  and stops parallelizing when it reaches 1.+  -}+  Word ->+  Mut α (Vector a) %1 ->+  BO β ()+qsort = go+  where+    go :: Word -> Mut α (Vector a) %1 -> BO β ()+    go budget v = case size v of+      (Ur 0, v) -> Control.pure $ consume v+      (Ur 1, v) -> Control.pure $ consume v+      (Ur n, v) -> Control.do+        let i = n `quot` 2+        (Ur pivot, v) <- copyAtMut i v+        (lo, hi) <- divide pivot v 0 n+        let b' = budget `quot` 2+        Control.void $ parIf (b' NonLinear.> 0) (go b' lo) (go b' hi)++parIf :: Bool %1 -> BO α a %1 -> BO α b %1 -> BO α (a, b)+{-# INLINE parIf #-}+parIf p = if p then parBO else Control.liftA2 (,)++divide ::+  (Ord a, Copyable a, α >= β) =>+  a ->+  Mut α (Vector a) %1 ->+  Int ->+  Int ->+  BO β (Mut α (Vector a), Mut α (Vector a))+divide pivot = partUp+  where+    partUp v l u+      | l < u = Control.do+          (Ur e, v) <- copyAtMut l v+          if e < pivot+            then partUp v (l + 1) u+            else partDown v l (u - 1)+      | otherwise = Control.pure $ splitAt l v+    partDown v l u+      | l < u = Control.do+          (Ur e, v) <- copyAtMut u v+          if pivot < e+            then partDown v l (u - 1)+            else Control.do+              v <- unsafeSwap v l u+              partUp v (l + 1) u+      | otherwise = Control.pure $ splitAt l v
+ test/Control/Concurrent/DivideConquer/LinearSpec.hs view
@@ -0,0 +1,59 @@+{-# LANGUAGE BlockArguments #-}+{-# LANGUAGE ImpredicativeTypes #-}+{-# LANGUAGE LambdaCase #-}+{-# LANGUAGE LinearTypes #-}+{-# LANGUAGE QualifiedDo #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE NoImplicitPrelude #-}+{-# OPTIONS_GHC -Wno-name-shadowing #-}++module Control.Concurrent.DivideConquer.LinearSpec (+  module Control.Concurrent.DivideConquer.LinearSpec,+) where++import Control.Concurrent.DivideConquer.Linear+import Control.Functor.Linear qualified as Control+import Control.Monad.Borrow.Pure.BO+import Control.Monad.Borrow.Pure.Copyable+import Control.Syntax.DataFlow qualified as DataFlow+import Data.List qualified as List+import Data.List qualified as NonLinear+import Data.Vector qualified as V+import Data.Vector.Mutable.Linear.Borrow qualified as VL+import Prelude.Linear+import Test.Falsify.Generator qualified as G+import Test.Falsify.Predicate qualified as P+import Test.Falsify.Range qualified as G+import Test.Tasty (TestTree, testGroup)+import Test.Tasty.Falsify (testProperty)+import Test.Tasty.Falsify qualified as F+import Test.Tasty.HUnit (testCase, (@?=))+import Prelude qualified as NonLinear++test_qsort :: TestTree+test_qsort =+  testGroup+    "qsort"+    [ testCase "empty" do+        qsortDCVec (V.empty @Int) @?= V.empty+    , testProperty "coincides with Data.List.sort on Ints" do+        xs <- F.gen $ G.list (G.between (1, 100)) $ G.int $ G.between (-100, 100)+        let v = V.fromList xs+            sorted = qsortDCVec v+        F.collect "length" [ceiling @_ @Int (fromIntegral @_ @Double (V.length v) / 10) * 10]+        F.collect "min" [NonLinear.minimum v `quot` 10 * 10]+        F.collect "max" [NonLinear.maximum v `quot` 10 * 10]+        F.collect "sorted" [V.and $ V.zipWith (NonLinear.<=) v (V.tail v)]+        F.info $ "input: " <> show xs+        F.assert $+          P.expect (V.fromList $ List.sort xs)+            P..$ ("output", sorted)+    ]++qsortDCVec :: (Ord a, Copyable a) => V.Vector a -> V.Vector a+qsortDCVec v = unur $ linearly \lin -> DataFlow.do+  (l1, l2) <- dup lin+  runBO l1 Control.do+    (v, lend) <- borrowM (VL.fromVector v l2)+    Control.void $ qsortDC 10 128 v+    Control.pure $ After (VL.toVector (reclaim lend))
+ test/Control/Monad/Borrow/Pure/Lifetime/TypingCases.hs view
@@ -0,0 +1,50 @@+{-# LANGUAGE ConstraintKinds #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE RequiredTypeArguments #-}+{-# LANGUAGE TypeFamilies #-}+{-# OPTIONS_GHC -O0 #-}+{-# OPTIONS_GHC -Wno-redundant-constraints #-}+{-# OPTIONS_GHC -fdefer-type-errors -Wno-deferred-type-errors #-}++module Control.Monad.Borrow.Pure.Lifetime.TypingCases (+  module Control.Monad.Borrow.Pure.Lifetime.TypingCases,+) where++import Control.Monad.Borrow.Pure.Lifetime.Internal++data Dict c where+  MkDict :: (c) => Dict c++withDict :: Dict c -> ((c) => a) -> a+withDict MkDict x = x++type family L1 :: Lifetime where++type family L2 :: Lifetime where++type family L3 :: Lifetime where++transitive :: (α <= β, β <= γ) => Witness α γ+transitive = witness++infElimL :: forall α β γ -> (α <= β) => Witness (α /\ γ) β+infElimL _ _ _ = witness++infElimR :: forall α β γ -> (α <= β) => Witness (γ /\ α) β+infElimR _ _ _ = witness++infIntro :: forall α β γ -> (α <= β, α <= γ) => Witness α (β /\ γ)+infIntro _ _ _ = witness++infComm :: forall α β -> Witness (α /\ β) (β /\ α)+infComm _ _ = witness++infMonotone :: forall α β γ -> (α <= β) => Witness (α /\ γ) (β /\ γ)+infMonotone _ _ _ = witness++infL :: forall α β -> Witness (α /\ β) α+infL _ _ = witness++infR :: forall α β -> Witness (α /\ β) β+infR _ _ = witness
+ test/Control/Monad/Borrow/Pure/LifetimeSpec.hs view
@@ -0,0 +1,52 @@+{-# LANGUAGE BlockArguments #-}+{-# LANGUAGE TypeFamilies #-}+{-# OPTIONS_GHC -Wno-redundant-constraints -O0 #-}++module Control.Monad.Borrow.Pure.LifetimeSpec (+  module Control.Monad.Borrow.Pure.LifetimeSpec,+) where++import Control.DeepSeq (force)+import Control.Exception (evaluate)+import Control.Monad.Borrow.Pure.Lifetime+import Control.Monad.Borrow.Pure.Lifetime.TypingCases+import Data.Functor+import Test.Tasty (TestTree, testGroup)+import Test.Tasty.ExpectedFailure (expectFailBecause)+import Test.Tasty.HUnit (testCase)+import Unsafe.Coerce (unsafeCoerce)++l1LeqL2 :: Dict (L1 <= L2)+l1LeqL2 = unsafeCoerce $ MkDict @(Static <= Static)++l2LeqL3 :: Dict (L2 <= L3)+l2LeqL3 = unsafeCoerce $ MkDict @(Static <= Static)++l1LeqL3 :: Dict (L1 <= L3)+l1LeqL3 = unsafeCoerce $ MkDict @(Static <= Static)++test_should_pass :: TestTree+test_should_pass =+  testGroup+    "should typechecks"+    [ expectFailBecause "We don't rely on transitivity" $+        testCase "(α <= β, β <= γ) => α <= γ" do+          void $ evaluate $ force $ withDict l1LeqL2 $ withDict l2LeqL3 $ transitive @L1 @L2 @L3+    , expectFailBecause "Monotonicity is not guaranteed and not currently used" $+        testCase "α <= β => α /\\ γ <= β" do+          void $ evaluate $ force $ withDict l1LeqL2 $ infElimL L1 L2 L3+    , expectFailBecause "Monotonicity is not guaranteed and not currently used" $+        testCase "α <= β => γ /\\ α <= β" do+          void $ evaluate $ force $ withDict l1LeqL2 $ infElimR L1 L2 L3+    , expectFailBecause "Monotonicity is not guaranteed and not currently used" $+        testCase "α <= β => α /\\ γ <= β /\\ γ" do+          void $ evaluate $ force $ withDict l1LeqL2 $ infMonotone L1 L2 L3+    , testCase "(α <= β, α <= γ) => α <= β /\\ γ" do+        void $ evaluate $ force $ withDict l1LeqL2 $ withDict l1LeqL3 $ infIntro L1 L2 L3+    , testCase "α /\\ β <= β /\\ α" do+        void $ evaluate $ force $ infComm L1 L2+    , testCase "α /\\ β <= α" do+        void $ evaluate $ force $ infL L1 L2+    , testCase "α /\\ β <= β" do+        void $ evaluate $ force $ infR L1 L2+    ]
+ test/Data/Vector/Mutable/Linear/BorrowSpec.hs view
@@ -0,0 +1,169 @@+{-# LANGUAGE BlockArguments #-}+{-# LANGUAGE ImpredicativeTypes #-}+{-# LANGUAGE LambdaCase #-}+{-# LANGUAGE LinearTypes #-}+{-# LANGUAGE QualifiedDo #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE NoImplicitPrelude #-}+{-# OPTIONS_GHC -Wno-name-shadowing #-}++module Data.Vector.Mutable.Linear.BorrowSpec (+  module Data.Vector.Mutable.Linear.BorrowSpec,+) where++import Control.Functor.Linear qualified as Control+import Control.Monad.Borrow.Pure.BO+import Control.Monad.Borrow.Pure.Copyable+import Control.Syntax.DataFlow qualified as DataFlow+import Data.Bifunctor.Linear qualified as Bi+import Data.List qualified as List+import Data.Vector qualified as V+import Data.Vector.Mutable.Linear.Borrow qualified as VL+import Prelude.Linear+import Test.Falsify.Generator qualified as G+import Test.Falsify.Predicate qualified as P+import Test.Falsify.Property qualified as F+import Test.Falsify.Range qualified as G+import Test.Tasty (TestTree, testGroup)+import Test.Tasty.Falsify (testProperty)+import Test.Tasty.HUnit+import Prelude qualified as NonLinear++qsortVec :: (Ord a, Copyable a) => V.Vector a -> V.Vector a+qsortVec v = unur $ linearly \lin -> DataFlow.do+  (l1, l2) <- dup lin+  runBO l1 Control.do+    (v, lend) <- borrowM (VL.fromVector v l2)+    VL.qsort 8 v+    pureAfter $ VL.toVector (reclaim lend)++divideList :: [Int] -> (Int, [Int])+divideList [] = (0, [])+divideList xs =+  let v0 = (V.fromList xs)+      pivot = v0 V.! (V.length v0 `quot` 2)+   in Bi.second unur $ linearly \lin -> DataFlow.do+        (l1, l2) <- dup lin+        runBO l1 Control.do+          (v, lend) <- borrowM (VL.fromList xs l2)+          VL.size v & \(Ur len, v) -> Control.do+            (lo, hi) <- VL.divide pivot v 0 len+            VL.size lo & \(Ur n, lo) -> DataFlow.do+              consume lo+              consume hi+              pureAfter (n, VL.toList $ reclaim lend)++test_divideList :: TestTree+test_divideList =+  testGroup+    "divideList"+    [ testCase "empty" do+        divideList [] @?= (0, [])+    , testProperty "singleton" do+        x <- F.gen $ G.int $ G.between (-100, 100)+        F.assert $+          P.expect (0, [x])+            P..$ ("answer", divideList [x])+    , testProperty "non-empty" do+        xs <- F.gen $ G.list (G.between (1, 100)) $ G.int $ G.between (0, 100)+        let v = V.fromList xs+            pivot = v V.! (V.length v `quot` 2)+            (off, vs) = divideList xs+            (lo, hi) = V.splitAt off $ V.fromList vs++        F.collect "length" [ceiling @_ @Int (fromIntegral @_ @Double (V.length v) / 10) * 10]+        F.collect "min" [NonLinear.minimum v `quot` 10 * 10]+        F.collect "max" [NonLinear.maximum v `quot` 10 * 10]+        F.info $ "pivot: " <> show pivot+        F.assert $+          P.satisfies ("lo <= " <> show pivot, V.all (NonLinear.<= pivot))+            P..$ ("lo", lo)+        F.assert $+          P.satisfies ("hi >= " <> show pivot, V.all (NonLinear.>= pivot))+            P..$ ("hi", hi)+    ]++test_qsort :: TestTree+test_qsort =+  testGroup+    "qsort"+    [ testCase "empty" do+        qsortVec (V.empty @Int) @?= V.empty+    , testProperty "coincides with Data.List.sort on Ints" do+        xs <- F.gen $ G.list (G.between (1, 100)) $ G.int $ G.between (-100, 100)+        let v = V.fromList xs+            sorted = qsortVec v+        F.collect "length" [ceiling @_ @Int (fromIntegral @_ @Double (V.length v) / 10) * 10]+        F.collect "min" [NonLinear.minimum v `quot` 10 * 10]+        F.collect "max" [NonLinear.maximum v `quot` 10 * 10]+        F.collect "sorted" [V.and $ V.zipWith (NonLinear.<=) v (V.tail v)]+        F.info $ "input: " <> show xs+        F.assert $+          P.expect (V.fromList $ List.sort xs)+            P..$ ("output", sorted)+    ]++example1 :: (Int, [Int])+example1 = linearly \lin -> DataFlow.do+  (lin, lin') <- dup lin+  vec <- VL.fromList [0, 1, 2] lin+  runBO lin' Control.do+    (mvec, lend) <- borrowM vec+    mvec <- VL.modify 0 (+ 3) mvec+    mvec <- VL.modify 2 (+ 5) mvec+    mvec <- VL.modify 0 (* 4) mvec+    let !(Ur svec) = share mvec+    Ur n <- VL.copyAt 0 svec+    pureAfter $ (n, unur $ VL.toList (reclaim lend))++test_example1 :: TestTree+test_example1 =+  testCase "example1" do+    example1 @?= (12, [12, 1, 7])++example2 :: (Int, [Int])+example2 = linearly \lin -> DataFlow.do+  (lin, lin') <- dup lin+  vec <- VL.fromList [0, 1, 2] lin+  runBO lin' Control.do+    (mvec, lend) <- borrowM vec+    let !(mvec1, mvec2) = VL.splitAt 1 mvec+    (mvec, ()) <-+      parBO+        ( Control.do+            mvec1 <- VL.modify 0 (+ 3) mvec1+            VL.modify 0 (* 4) mvec1+        )+        (consume Control.<$> VL.modify 1 (+ 5) mvec2)+    let !(Ur svec) = share mvec+    Ur n <- VL.copyAt 0 svec+    pureAfter $ (n, unur $ VL.toList (reclaim lend))++test_example2 :: TestTree+test_example2 =+  testCase "example2" do+    example2 @?= (12, [12, 1, 7])++example3 :: (Int, [Int])+example3 = linearly \lin -> DataFlow.do+  (lin, lin') <- dup lin+  vec <- VL.fromList [0, 1, 2] lin+  runBO lin' Control.do+    (mvec, lend) <- borrowM vec+    mvec <- reborrowing_ mvec \mvec -> Control.do+      let !(mvec1, mvec2) = VL.splitAt 1 mvec+      consume+        Control.<$> parBO+          ( Control.do+              mvec1 <- VL.modify 0 (+ 3) mvec1+              VL.modify 0 (* 4) mvec1+          )+          (VL.modify 1 (+ 5) mvec2)+    let !(Ur svec) = share mvec+    Ur n <- VL.copyAt 0 svec+    pureAfter $ (n, unur $ VL.toList (reclaim lend))++test_example3 :: TestTree+test_example3 =+  testCase "example3" do+    example3 @?= (12, [12, 1, 7])
+ test/Main.hs view
@@ -0,0 +1,1 @@+{-# OPTIONS_GHC -F -pgmF tasty-discover -optF --tree-display #-}