diff --git a/CHANGELOG.md b/CHANGELOG.md new file mode 100644 --- /dev/null +++ b/CHANGELOG.md @@ -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. diff --git a/LICENSE b/LICENSE new file mode 100644 --- /dev/null +++ b/LICENSE @@ -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. diff --git a/README.md b/README.md new file mode 100644 --- /dev/null +++ b/README.md @@ -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. diff --git a/app/artifact-runner.hs b/app/artifact-runner.hs new file mode 100644 --- /dev/null +++ b/app/artifact-runner.hs @@ -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 diff --git a/app/convert-qsort-bench-csv.hs b/app/convert-qsort-bench-csv.hs new file mode 100644 --- /dev/null +++ b/app/convert-qsort-bench-csv.hs @@ -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 diff --git a/app/qsort.hs b/app/qsort.hs new file mode 100644 --- /dev/null +++ b/app/qsort.hs @@ -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 diff --git a/bench/qsort.hs b/bench/qsort.hs new file mode 100644 --- /dev/null +++ b/bench/qsort.hs @@ -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 diff --git a/dockerfiles/artifact/Dockerfile b/dockerfiles/artifact/Dockerfile new file mode 100644 --- /dev/null +++ b/dockerfiles/artifact/Dockerfile @@ -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"] diff --git a/doctests/doctests.hs b/doctests/doctests.hs new file mode 100644 --- /dev/null +++ b/doctests/doctests.hs @@ -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 diff --git a/internal-src/qsort-bench-suites/PureBorrow/Internal/Bench/QSort.hs b/internal-src/qsort-bench-suites/PureBorrow/Internal/Bench/QSort.hs new file mode 100644 --- /dev/null +++ b/internal-src/qsort-bench-suites/PureBorrow/Internal/Bench/QSort.hs @@ -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 diff --git a/internal-src/qsort-demo-impl/PureBorrow/Demo/QSort.hs b/internal-src/qsort-demo-impl/PureBorrow/Demo/QSort.hs new file mode 100644 --- /dev/null +++ b/internal-src/qsort-demo-impl/PureBorrow/Demo/QSort.hs @@ -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 diff --git a/pure-borrow.cabal b/pure-borrow.cabal new file mode 100644 --- /dev/null +++ b/pure-borrow.cabal @@ -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 diff --git a/scripts/genplot.gnuplot b/scripts/genplot.gnuplot new file mode 100644 --- /dev/null +++ b/scripts/genplot.gnuplot @@ -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 diff --git a/src/Control/Concurrent/DivideConquer/Linear.hs b/src/Control/Concurrent/DivideConquer/Linear.hs new file mode 100644 --- /dev/null +++ b/src/Control/Concurrent/DivideConquer/Linear.hs @@ -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 + } diff --git a/src/Control/Concurrent/DivideConquer/Utils/OnceChan/Linear.hs b/src/Control/Concurrent/DivideConquer/Utils/OnceChan/Linear.hs new file mode 100644 --- /dev/null +++ b/src/Control/Concurrent/DivideConquer/Utils/OnceChan/Linear.hs @@ -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 diff --git a/src/Control/Concurrent/DivideConquer/Utils/OnceChan/Linear/Unlifted.hs b/src/Control/Concurrent/DivideConquer/Utils/OnceChan/Linear/Unlifted.hs new file mode 100644 --- /dev/null +++ b/src/Control/Concurrent/DivideConquer/Utils/OnceChan/Linear/Unlifted.hs @@ -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 diff --git a/src/Control/Concurrent/DivideConquer/Utils/QueuePool.hs b/src/Control/Concurrent/DivideConquer/Utils/QueuePool.hs new file mode 100644 --- /dev/null +++ b/src/Control/Concurrent/DivideConquer/Utils/QueuePool.hs @@ -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) diff --git a/src/Control/Concurrent/STM/TMDeque.hs b/src/Control/Concurrent/STM/TMDeque.hs new file mode 100644 --- /dev/null +++ b/src/Control/Concurrent/STM/TMDeque.hs @@ -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 diff --git a/src/Control/Concurrent/STM/TMDequeRingBuffer.hs b/src/Control/Concurrent/STM/TMDequeRingBuffer.hs new file mode 100644 --- /dev/null +++ b/src/Control/Concurrent/STM/TMDequeRingBuffer.hs @@ -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 diff --git a/src/Control/Monad/Borrow/Pure.hs b/src/Control/Monad/Borrow/Pure.hs new file mode 100644 --- /dev/null +++ b/src/Control/Monad/Borrow/Pure.hs @@ -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". +-} diff --git a/src/Control/Monad/Borrow/Pure/Affine.hs b/src/Control/Monad/Borrow/Pure/Affine.hs new file mode 100644 --- /dev/null +++ b/src/Control/Monad/Borrow/Pure/Affine.hs @@ -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 diff --git a/src/Control/Monad/Borrow/Pure/Affine/Internal.hs b/src/Control/Monad/Borrow/Pure/Affine/Internal.hs new file mode 100644 --- /dev/null +++ b/src/Control/Monad/Borrow/Pure/Affine/Internal.hs @@ -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 #-} diff --git a/src/Control/Monad/Borrow/Pure/Affine/Unsafe.hs b/src/Control/Monad/Borrow/Pure/Affine/Unsafe.hs new file mode 100644 --- /dev/null +++ b/src/Control/Monad/Borrow/Pure/Affine/Unsafe.hs @@ -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 diff --git a/src/Control/Monad/Borrow/Pure/BO.hs b/src/Control/Monad/Borrow/Pure/BO.hs new file mode 100644 --- /dev/null +++ b/src/Control/Monad/Borrow/Pure/BO.hs @@ -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 diff --git a/src/Control/Monad/Borrow/Pure/BO/Internal.hs b/src/Control/Monad/Borrow/Pure/BO/Internal.hs new file mode 100644 --- /dev/null +++ b/src/Control/Monad/Borrow/Pure/BO/Internal.hs @@ -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 #-} diff --git a/src/Control/Monad/Borrow/Pure/BO/Unsafe.hs b/src/Control/Monad/Borrow/Pure/BO/Unsafe.hs new file mode 100644 --- /dev/null +++ b/src/Control/Monad/Borrow/Pure/BO/Unsafe.hs @@ -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 diff --git a/src/Control/Monad/Borrow/Pure/Clone.hs b/src/Control/Monad/Borrow/Pure/Clone.hs new file mode 100644 --- /dev/null +++ b/src/Control/Monad/Borrow/Pure/Clone.hs @@ -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) diff --git a/src/Control/Monad/Borrow/Pure/Copyable.hs b/src/Control/Monad/Borrow/Pure/Copyable.hs new file mode 100644 --- /dev/null +++ b/src/Control/Monad/Borrow/Pure/Copyable.hs @@ -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) diff --git a/src/Control/Monad/Borrow/Pure/Experimental/Borrows.hs b/src/Control/Monad/Borrow/Pure/Experimental/Borrows.hs new file mode 100644 --- /dev/null +++ b/src/Control/Monad/Borrow/Pure/Experimental/Borrows.hs @@ -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' #-} diff --git a/src/Control/Monad/Borrow/Pure/Experimental/Loop.hs b/src/Control/Monad/Borrow/Pure/Experimental/Loop.hs new file mode 100644 --- /dev/null +++ b/src/Control/Monad/Borrow/Pure/Experimental/Loop.hs @@ -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 diff --git a/src/Control/Monad/Borrow/Pure/Experimental/Reborrowable.hs b/src/Control/Monad/Borrow/Pure/Experimental/Reborrowable.hs new file mode 100644 --- /dev/null +++ b/src/Control/Monad/Borrow/Pure/Experimental/Reborrowable.hs @@ -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 diff --git a/src/Control/Monad/Borrow/Pure/Lifetime.hs b/src/Control/Monad/Borrow/Pure/Lifetime.hs new file mode 100644 --- /dev/null +++ b/src/Control/Monad/Borrow/Pure/Lifetime.hs @@ -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 diff --git a/src/Control/Monad/Borrow/Pure/Lifetime/Internal.hs b/src/Control/Monad/Borrow/Pure/Lifetime/Internal.hs new file mode 100644 --- /dev/null +++ b/src/Control/Monad/Borrow/Pure/Lifetime/Internal.hs @@ -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'' #-} diff --git a/src/Control/Monad/Borrow/Pure/Lifetime/Token.hs b/src/Control/Monad/Borrow/Pure/Lifetime/Token.hs new file mode 100644 --- /dev/null +++ b/src/Control/Monad/Borrow/Pure/Lifetime/Token.hs @@ -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 diff --git a/src/Control/Monad/Borrow/Pure/Lifetime/Token/Internal.hs b/src/Control/Monad/Borrow/Pure/Lifetime/Token/Internal.hs new file mode 100644 --- /dev/null +++ b/src/Control/Monad/Borrow/Pure/Lifetime/Token/Internal.hs @@ -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 #-} diff --git a/src/Control/Monad/Borrow/Pure/Lifetime/Token/Unsafe.hs b/src/Control/Monad/Borrow/Pure/Lifetime/Token/Unsafe.hs new file mode 100644 --- /dev/null +++ b/src/Control/Monad/Borrow/Pure/Lifetime/Token/Unsafe.hs @@ -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 diff --git a/src/Control/Monad/Borrow/Pure/Utils.hs b/src/Control/Monad/Borrow/Pure/Utils.hs new file mode 100644 --- /dev/null +++ b/src/Control/Monad/Borrow/Pure/Utils.hs @@ -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) diff --git a/src/Control/Syntax/DataFlow.hs b/src/Control/Syntax/DataFlow.hs new file mode 100644 --- /dev/null +++ b/src/Control/Syntax/DataFlow.hs @@ -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 diff --git a/src/Data/Coerce/Directed.hs b/src/Data/Coerce/Directed.hs new file mode 100644 --- /dev/null +++ b/src/Data/Coerce/Directed.hs @@ -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 diff --git a/src/Data/Coerce/Directed/Internal.hs b/src/Data/Coerce/Directed/Internal.hs new file mode 100644 --- /dev/null +++ b/src/Data/Coerce/Directed/Internal.hs @@ -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 diff --git a/src/Data/Coerce/Directed/Unsafe.hs b/src/Data/Coerce/Directed/Unsafe.hs new file mode 100644 --- /dev/null +++ b/src/Data/Coerce/Directed/Unsafe.hs @@ -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 diff --git a/src/Data/Comonad/Linear.hs b/src/Data/Comonad/Linear.hs new file mode 100644 --- /dev/null +++ b/src/Data/Comonad/Linear.hs @@ -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 (<@>) #-} diff --git a/src/Data/Record/Linear/Borrow/Experimental/PatternMatch.hs b/src/Data/Record/Linear/Borrow/Experimental/PatternMatch.hs new file mode 100644 --- /dev/null +++ b/src/Data/Record/Linear/Borrow/Experimental/PatternMatch.hs @@ -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 diff --git a/src/Data/Record/Linear/Borrow/Experimental/Split.hs b/src/Data/Record/Linear/Borrow/Experimental/Split.hs new file mode 100644 --- /dev/null +++ b/src/Data/Record/Linear/Borrow/Experimental/Split.hs @@ -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 diff --git a/src/Data/Ref/Linear.hs b/src/Data/Ref/Linear.hs new file mode 100644 --- /dev/null +++ b/src/Data/Ref/Linear.hs @@ -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 #-} diff --git a/src/Data/Ref/Linear/Borrow.hs b/src/Data/Ref/Linear/Borrow.hs new file mode 100644 --- /dev/null +++ b/src/Data/Ref/Linear/Borrow.hs @@ -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 diff --git a/src/Data/Ref/Linear/Unlifted.hs b/src/Data/Ref/Linear/Unlifted.hs new file mode 100644 --- /dev/null +++ b/src/Data/Ref/Linear/Unlifted.hs @@ -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 #) diff --git a/src/Data/Unique/Linear.hs b/src/Data/Unique/Linear.hs new file mode 100644 --- /dev/null +++ b/src/Data/Unique/Linear.hs @@ -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 diff --git a/src/Data/Vector/Mutable/Linear/Borrow.hs b/src/Data/Vector/Mutable/Linear/Borrow.hs new file mode 100644 --- /dev/null +++ b/src/Data/Vector/Mutable/Linear/Borrow.hs @@ -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 diff --git a/test/Control/Concurrent/DivideConquer/LinearSpec.hs b/test/Control/Concurrent/DivideConquer/LinearSpec.hs new file mode 100644 --- /dev/null +++ b/test/Control/Concurrent/DivideConquer/LinearSpec.hs @@ -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)) diff --git a/test/Control/Monad/Borrow/Pure/Lifetime/TypingCases.hs b/test/Control/Monad/Borrow/Pure/Lifetime/TypingCases.hs new file mode 100644 --- /dev/null +++ b/test/Control/Monad/Borrow/Pure/Lifetime/TypingCases.hs @@ -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 diff --git a/test/Control/Monad/Borrow/Pure/LifetimeSpec.hs b/test/Control/Monad/Borrow/Pure/LifetimeSpec.hs new file mode 100644 --- /dev/null +++ b/test/Control/Monad/Borrow/Pure/LifetimeSpec.hs @@ -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 + ] diff --git a/test/Data/Vector/Mutable/Linear/BorrowSpec.hs b/test/Data/Vector/Mutable/Linear/BorrowSpec.hs new file mode 100644 --- /dev/null +++ b/test/Data/Vector/Mutable/Linear/BorrowSpec.hs @@ -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]) diff --git a/test/Main.hs b/test/Main.hs new file mode 100644 --- /dev/null +++ b/test/Main.hs @@ -0,0 +1,1 @@ +{-# OPTIONS_GHC -F -pgmF tasty-discover -optF --tree-display #-}