Dupable wars : implementation

linear-base.cabal

@@ -70,15 +70,20 @@ library
         Data.Set.Mutable.Linear
         Data.Set.Mutable.Linear.Internal
         Data.Tuple.Linear
+        Data.Unrestricted.Linear
         Data.Unrestricted.Internal.Consumable
         Data.Unrestricted.Internal.Dupable
         Data.Unrestricted.Internal.Movable
         Data.Unrestricted.Internal.Instances
         Data.Unrestricted.Internal.Ur
         Data.Unrestricted.Internal.UrT
-        Data.Unrestricted.Linear
+        Data.Replicator.Linear
+        Data.Replicator.Linear.Internal
+        Data.Replicator.Linear.Internal.ReplicationStream
+        Data.Replicator.Linear.Internal.Instances
+        Data.Arity.Linear.Internal.Arity
         Data.V.Linear
-        Data.V.Linear.Internal.V
+        Data.V.Linear.Internal
         Data.V.Linear.Internal.Instances
         Data.Vector.Mutable.Linear
         Data.Vector.Mutable.Linear.Internal

src/Data/Arity/Linear/Internal/Arity.hs

@@ -0,0 +1,21 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE LinearTypes #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE UndecidableInstances #-}
+
+module Data.Arity.Linear.Internal.Arity (Arity) where
+
+import GHC.TypeLits
+
+type family Arity b f where
+  Arity b b = 0
+  Arity b (a %1 -> f) = Arity b f + 1
+  Arity b f =
+    TypeError
+      ( 'Text "Arity: "
+          ':<>: 'ShowType f
+          ':<>: 'Text " isn't a linear function with head "
+          ':<>: 'ShowType b
+          ':<>: 'Text "."
+      )

src/Data/Replicator/Linear.hs

@@ -0,0 +1,44 @@
+{-# LANGUAGE MagicHash #-}
+{-# LANGUAGE NoImplicitPrelude #-}
+
+-- | This module defines a stream-like type named 'Replicator', which is
+-- mainly used in the definition of the 'Data.Unrestricted.Dupable' class
+-- to provide efficient linear duplication.
+-- The API of 'Replicator' is close to the one of an infinite stream: it
+-- can either produce a new value linearly (with 'next' or 'next#'), or be
+-- linearly discarded (with 'consume' or 'extract').
+--
+-- A crucial aspect, from a performance standpoint, is that the 'pure' function
+-- (which takes an unrestricted argument) is implemented efficiently: the
+-- 'Replicator' returns /the same/ value on each call to 'next'. That is, the
+-- pointer is always shared. This will allow 'Data.Unrestricted.Movable' types
+-- to be given an efficient instance of 'Data.Unrestricted.Dupable'. Instances
+-- of both 'Data.Unrestricted.Movable' and 'Data.Unrestricted.Dupable' typically
+-- involve deep copies. The implementation of 'pure' lets us make sure that, for
+-- @Movable@ types, only one deep copy is performed, rather than one per
+-- additional replica.
+--
+-- Strictly speaking, the implementation of '(<*>)' plays a role in all this as
+-- well:
+-- For two 'pure' 'Replicators' @fs@ and @as@, @fs \<*\> as@  is a pure
+-- 'Replicator'. Together, 'pure' and '(<*>)' form the
+-- 'Data.Functor.Linear.Applicative' instance of 'Replicator'.
+module Data.Replicator.Linear
+  ( Replicator,
+    consume,
+    duplicate,
+    map,
+    pure,
+    (<*>),
+    next,
+    next#,
+    take,
+    extract,
+    extend,
+    Elim,
+    elim,
+  )
+where
+
+import Data.Replicator.Linear.Internal
+import Data.Replicator.Linear.Internal.Instances ()

src/Data/Replicator/Linear/Internal.hs

@@ -0,0 +1,149 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE FunctionalDependencies #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE LambdaCase #-}
+{-# LANGUAGE LinearTypes #-}
+{-# LANGUAGE MagicHash #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE StandaloneKindSignatures #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE UnboxedTuples #-}
+{-# LANGUAGE UndecidableInstances #-}
+{-# LANGUAGE NoImplicitPrelude #-}
+{-# OPTIONS_HADDOCK hide #-}
+
+module Data.Replicator.Linear.Internal
+  ( Replicator (..),
+    consume,
+    duplicate,
+    map,
+    pure,
+    (<*>),
+    next,
+    next#,
+    take,
+    extract,
+    extend,
+    Elim (..),
+  )
+where
+
+import Data.Arity.Linear.Internal.Arity
+import Data.Kind (Constraint, Type)
+import Data.Replicator.Linear.Internal.ReplicationStream (ReplicationStream (..))
+import qualified Data.Replicator.Linear.Internal.ReplicationStream as ReplicationStream
+import GHC.TypeLits
+import Prelude.Linear.Internal
+import Prelude ((-))
+import qualified Prelude
+
+-- | 'Replicator' is a stream-like data structure used to linearly duplicate
+-- values.
+data Replicator a where
+  Moved :: a -> Replicator a
+  Streamed :: ReplicationStream a %1 -> Replicator a
+
+consume :: Replicator a %1 -> ()
+consume (Moved _) = ()
+consume (Streamed stream) = ReplicationStream.consume stream
+
+duplicate :: Replicator a %1 -> Replicator (Replicator a)
+duplicate = \case
+  Moved x -> Moved (Moved x)
+  Streamed stream -> Streamed $ ReplicationStream.map Streamed (ReplicationStream.duplicate stream)
+
+map :: (a %1 -> b) -> Replicator a %1 -> Replicator b
+map f = \case
+  Moved x -> Moved (f x)
+  Streamed stream -> Streamed $ ReplicationStream.map f stream
+
+pure :: a -> Replicator a
+pure = Moved
+
+(<*>) :: Replicator (a %1 -> b) %1 -> Replicator a %1 -> Replicator b
+(Moved f) <*> (Moved x) = Moved (f x)
+sf <*> sx = Streamed (toStream sf ReplicationStream.<*> toStream sx)
+  where
+    toStream :: Replicator a %1 -> ReplicationStream a
+    toStream = \case
+      Moved x -> ReplicationStream.pure x
+      Streamed stream -> stream
+
+-- | Extracts the next item from the \"infinite stream\" @'Replicator' a@.
+next :: Replicator a %1 -> (a, Replicator a)
+next (Moved x) = (x, Moved x)
+next (Streamed (ReplicationStream s give dups consumes)) =
+  dups s & \case
+    (s1, s2) -> (give s1, Streamed (ReplicationStream s2 give dups consumes))
+
+-- | Extracts the next item from the \"infinite stream\" @'Replicator' a@.
+-- Same function as 'next', but returning an unboxed tuple.
+next# :: Replicator a %1 -> (# a, Replicator a #)
+next# (Moved x) = (# x, Moved x #)
+next# (Streamed (ReplicationStream s give dups consumes)) =
+  dups s & \case
+    (s1, s2) -> (# give s1, Streamed (ReplicationStream s2 give dups consumes) #)
+
+-- | @'take' n as@ is a list of size @n@, containing @n@ replicas from @as@.
+take :: Prelude.Int -> Replicator a %1 -> [a]
+take 0 r =
+  consume r & \case
+    () -> []
+take 1 r = [extract r]
+take n r =
+  next r & \case
+    (a, r') -> a : take (n - 1) r'
+
+-- | Returns the next item from @'Replicator' a@ and efficiently consumes
+-- the replicator at the same time.
+extract :: Replicator a %1 -> a
+extract (Moved x) = x
+extract (Streamed (ReplicationStream s give _ _)) = give s
+
+-- | Comonadic 'extend' function.
+--
+-- > extend f = map f . duplicate
+extend :: (Replicator a %1 -> b) -> Replicator a %1 -> Replicator b
+extend f = map f . duplicate
+
+-- | @'Elim' n a b f@ asserts that @f@ is a function taking @n@ linear arguments
+-- of type @a@ and then returning a value of type @b@.
+--
+-- It is solely used to define the type of the 'elim' function.
+type Elim :: Nat -> Type -> Type -> Type -> Constraint
+class (n ~ Arity b f) => Elim n a b f | n a b -> f, f b -> n where
+  -- | Takes a function of type @a %1 -> a %1 -> ... %1 -> a %1 -> b@, and
+  -- returns a @b@ . The replicator is used to supply all the items of type @a@
+  -- required by the function.
+  --
+  -- For instance:
+  --
+  -- > elim @1 :: (a %1 -> b) %1 -> Replicator a %1 -> b
+  -- > elim @2 :: (a %1 -> a %1 -> b) %1 -> Replicator a %1 -> b
+  -- > elim @3 :: (a %1 -> a %1 -> a %1 -> b) %1 -> Replicator a %1 -> b
+  --
+  -- It is not always necessary to give the arity argument. It can be
+  -- inferred from the function argument.
+  --
+  -- > elim (,) :: Replicator a %1 -> (a, a)
+  -- > elim (,,) :: Replicator a %1 -> (a, a, a)
+  elim :: f %1 -> Replicator a %1 -> b
+
+instance Elim 0 a b b where
+  elim b r =
+    consume r & \case
+      () -> b
+  {-# INLINE elim #-}
+
+instance (Arity b (a %1 -> b) ~ 1) => Elim 1 a b (a %1 -> b) where
+  elim f r = f (extract r)
+  {-# INLINE elim #-}
+
+instance {-# OVERLAPPABLE #-} (n ~ Arity b (a %1 -> f), Elim (n - 1) a b f) => Elim n a b (a %1 -> f) where
+  elim g r =
+    next r & \case
+      (a, r') -> elim (g a) r'
+  {-# INLINE elim #-}

src/Data/Replicator/Linear/Internal/Instances.hs

@@ -0,0 +1,24 @@
+{-# OPTIONS -Wno-orphans #-}
+{-# OPTIONS_HADDOCK hide #-}
+
+module Data.Replicator.Linear.Internal.Instances where
+
+import qualified Data.Functor.Linear as Data
+import Data.Replicator.Linear.Internal
+import qualified Data.Replicator.Linear.Internal as Replicator
+import Data.Replicator.Linear.Internal.ReplicationStream
+import qualified Data.Replicator.Linear.Internal.ReplicationStream as ReplicationStream
+
+instance Data.Functor ReplicationStream where
+  fmap = ReplicationStream.map
+
+instance Data.Applicative ReplicationStream where
+  pure = ReplicationStream.pure
+  f <*> x = f ReplicationStream.<*> x
+
+instance Data.Functor Replicator where
+  fmap = Replicator.map
+
+instance Data.Applicative Replicator where
+  pure = Replicator.pure
+  f <*> x = f Replicator.<*> x

src/Data/Replicator/Linear/Internal/ReplicationStream.hs

@@ -0,0 +1,77 @@
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE LambdaCase #-}
+{-# LANGUAGE LinearTypes #-}
+{-# LANGUAGE NoImplicitPrelude #-}
+{-# OPTIONS_HADDOCK hide #-}
+
+module Data.Replicator.Linear.Internal.ReplicationStream
+  ( ReplicationStream (..),
+    consume,
+    duplicate,
+    map,
+    pure,
+    (<*>),
+  )
+where
+
+import Data.Unrestricted.Internal.Ur
+import Prelude.Linear.Internal
+
+-- | @'ReplicatorStream' s g dup2 c@ is the infinite linear stream
+-- @repeat (g s)@ where @dup2@ is used to make as many copies of @s@ as
+-- necessary, and @c@ is used to consume @s@ when consuming the stream.
+--
+-- Although it isn't enforced at type level, @dup2@ should abide by the same
+-- laws as 'Data.Unrestricted.Dupable.dup2':
+-- * @first c (dup2 a) ≃ a ≃ second c (dup2 a)@ (neutrality)
+-- * @first dup2 (dup2 a) ≃ (second dup2 (dup2 a))@ (associativity)
+--
+-- This type is solely used to implement 'Data.Replicator.Linear'
+data ReplicationStream a where
+  ReplicationStream ::
+    s %1 ->
+    (s %1 -> a) ->
+    (s %1 -> (s, s)) ->
+    (s %1 -> ()) ->
+    ReplicationStream a
+
+consume :: ReplicationStream a %1 -> ()
+consume (ReplicationStream s _ _ consumes) = consumes s
+
+duplicate :: ReplicationStream a %1 -> ReplicationStream (ReplicationStream a)
+duplicate (ReplicationStream s give dups consumes) =
+  ReplicationStream
+    s
+    (\s' -> ReplicationStream s' give dups consumes)
+    dups
+    consumes
+
+map :: (a %1 -> b) -> ReplicationStream a %1 -> ReplicationStream b
+map f (ReplicationStream s give dups consumes) =
+  ReplicationStream s (f . give) dups consumes
+
+pure :: a -> ReplicationStream a
+pure x =
+  ReplicationStream
+    (Ur x)
+    unur
+    ( \case
+        Ur x' -> (Ur x', Ur x')
+    )
+    ( \case
+        Ur _ -> ()
+    )
+
+(<*>) :: ReplicationStream (a %1 -> b) %1 -> ReplicationStream a %1 -> ReplicationStream b
+(ReplicationStream sf givef dupsf consumesf) <*> (ReplicationStream sx givex dupsx consumesx) =
+  ReplicationStream
+    (sf, sx)
+    (\(sf', sx') -> givef sf' (givex sx'))
+    ( \(sf', sx') ->
+        (dupsf sf', dupsx sx') & \case
+          ((sf1, sf2), (sx1, sx2)) -> ((sf1, sx1), (sf2, sx2))
+    )
+    ( \(sf', sx') ->
+        consumesf sf' & \case
+          () -> consumesx sx'
+    )