linear-base-0.2.0: src/Data/Unrestricted/Linear/Internal/Movable.hs
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DerivingVia #-}
{-# LANGUAGE EmptyCase #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE LinearTypes #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE Trustworthy #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE NoImplicitPrelude #-}
{-# OPTIONS_HADDOCK hide #-}
module Data.Unrestricted.Linear.Internal.Movable
( -- * Movable
Movable (..),
GMovable,
genericMove,
)
where
import qualified Data.Functor.Linear.Internal.Applicative as Data
import qualified Data.Functor.Linear.Internal.Functor as Data
import Data.List.NonEmpty (NonEmpty (..))
import qualified Data.Semigroup as Semigroup
import Data.Unrestricted.Linear.Internal.Dupable
import Data.Unrestricted.Linear.Internal.Ur
import GHC.Tuple (Solo)
import GHC.Types (Multiplicity (..))
import Generics.Linear
import Prelude.Linear.Generically
import Prelude.Linear.Internal
import qualified Unsafe.Linear as Unsafe
import Prelude (Bool (..), Char, Double, Float, Int, Ordering (..), Word)
import qualified Prelude as Prelude
-- | Use @'Movable' a@ to represent a type which can be used many times even
-- when given linearly. Simple data types such as 'Bool' or @[]@ are 'Movable'.
-- Though, bear in mind that this typically induces a deep copy of the value.
--
-- Formally, @'Movable' a@ is the class of
-- [coalgebras](https://ncatlab.org/nlab/show/coalgebra+over+a+comonad) of the
-- 'Ur' comonad. That is
--
-- * @unur (move x) = x@
-- * @move \@(Ur a) (move \@a x) = fmap (move \@a) $ move \@a x@
--
-- Additionally, a 'Movable' instance must be compatible with its 'Dupable' parent instance. That is:
--
-- * @case move x of {Ur _ -> ()} = consume x@
-- * @case move x of {Ur x -> (x, x)} = dup2 x@
class Dupable a => Movable a where
move :: a %1 -> Ur a
-- -------------
-- Instances
deriving via
Generically Bool
instance
Movable Bool
deriving via
Generically Char
instance
Movable Char
deriving via
Generically Double
instance
Movable Double
deriving via
Generically Float
instance
Movable Float
deriving via
Generically Int
instance
Movable Int
deriving via
Generically Word
instance
Movable Word
deriving via
Generically Prelude.Ordering
instance
Movable Prelude.Ordering
instance Movable () where
move () = Ur ()
deriving via
Generically (Solo a)
instance
Movable a => Movable (Solo a)
deriving via
Generically (a, b)
instance
(Movable a, Movable b) => Movable (a, b)
deriving via
Generically (a, b, c)
instance
(Movable a, Movable b, Movable c) => Movable (a, b, c)
deriving via
Generically (a, b, c, d)
instance
(Movable a, Movable b, Movable c, Movable d) => Movable (a, b, c, d)
deriving via
Generically (a, b, c, d, e)
instance
(Movable a, Movable b, Movable c, Movable d, Movable e) => Movable (a, b, c, d, e)
instance Movable a => Movable (Prelude.Maybe a) where
move (Prelude.Nothing) = Ur Prelude.Nothing
move (Prelude.Just x) = Data.fmap Prelude.Just (move x)
instance (Movable a, Movable b) => Movable (Prelude.Either a b) where
move (Prelude.Left a) = Data.fmap Prelude.Left (move a)
move (Prelude.Right b) = Data.fmap Prelude.Right (move b)
instance Movable a => Movable [a] where
-- The explicit go function lets this specialize.
move = go
where
go :: [a] %1 -> Ur [a]
go [] = Ur []
go (a : l) = (:) Data.<$> move a Data.<*> go l
instance Movable a => Movable (NonEmpty a) where
move (x :| xs) = (:|) Data.<$> move x Data.<*> move xs
instance Movable (Ur a) where
move (Ur a) = Ur (Ur a)
-- Some stock instances
deriving newtype instance Movable a => Movable (Semigroup.Sum a)
deriving newtype instance Movable a => Movable (Semigroup.Product a)
deriving newtype instance Movable Semigroup.All
deriving newtype instance Movable Semigroup.Any
-- -------------
-- Generic deriving
instance (Generic a, GMovable (Rep a)) => Movable (Generically a) where
move = Data.fmap (Generically . to) . gmove . from . unGenerically
genericMove :: (Generic a, GMovable (Rep a)) => a %1 -> Ur a
genericMove = Data.fmap to . gmove . from
class GDupable f => GMovable f where
gmove :: f p %1 -> Ur (f p)
instance GMovable V1 where
gmove = \case {}
instance GMovable U1 where
gmove U1 = Ur U1
instance (GMovable f, GMovable g) => GMovable (f :+: g) where
gmove (L1 a) = gmove a & \case (Ur x) -> Ur (L1 x)
gmove (R1 a) = gmove a & \case (Ur x) -> Ur (R1 x)
instance (GMovable f, GMovable g) => GMovable (f :*: g) where
gmove (a :*: b) =
gmove a & \case
(Ur x) ->
gmove b & \case
(Ur y) -> Ur (x :*: y)
instance Movable c => GMovable (K1 i c) where
gmove (K1 c) = lcoerce (move c)
instance GMovable f => GMovable (M1 i t f) where
gmove (M1 a) = lcoerce (gmove a)
instance GMovable (MP1 'Many f) where
gmove (MP1 x) = Ur (MP1 x)
instance GMovable f => GMovable (MP1 'One f) where
gmove (MP1 a) = gmove a & \case Ur x -> Ur (MP1 x)
instance GMovable UChar where
gmove (UChar c) = Unsafe.toLinear (\x -> Ur (UChar x)) c
instance GMovable UDouble where
gmove (UDouble c) = Unsafe.toLinear (\x -> Ur (UDouble x)) c
instance GMovable UFloat where
gmove (UFloat c) = Unsafe.toLinear (\x -> Ur (UFloat x)) c
instance GMovable UInt where
gmove (UInt c) = Unsafe.toLinear (\x -> Ur (UInt x)) c
instance GMovable UWord where
gmove (UWord c) = Unsafe.toLinear (\x -> Ur (UWord x)) c