```{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DerivingVia #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE LinearTypes #-}
{-# LANGUAGE NoImplicitPrelude #-}
{-# LANGUAGE StandaloneDeriving #-}

-- | This module provides a linear 'Num' class with instances.
-- Import this module to use linear versions of @(+)@, @(-)@, etc, on numeric
-- types like 'Int' and 'Double'.
--
-- == The Typeclass Hierarchy
--
-- The 'Num' class is broken up into several instances. Here is the basic
-- hierarchy:
--
-- * MultIdentity ⊆ MultIdentity
-- * (AddIdentity ∩ MultIdentity) ⊆ Semiring
-- * (AdditiveGroup ∩ Semiring) ⊆ Ring
-- * (FromInteger ∩ Ring) ⊆ Num
--
module Data.Num.Linear
(
-- * Num and sub-classes
Num(..)
, Multiplicative(..)
, MultIdentity(..)
, Semiring
, Ring
, FromInteger(..)
-- * Mechanisms for deriving instances
, Multiplying(..), getMultiplied
)
where

-- TODO: flesh out laws
import qualified Prelude
import Data.Unrestricted.Linear
import qualified Unsafe.Linear as Unsafe
import Data.Monoid.Linear

-- | A type that can be added linearly.  The operation @(+)@ is associative and
-- commutative, i.e., for all @a@, @b@, @c@
--
-- > (a + b) + c = a + (b + c)
-- > a + b = b + c
(+) :: a %1-> a %1-> a

-- | An 'Additive' type with an identity on @(+)@.
zero :: a

-- | An 'AddIdentity' with inverses that satisfies
-- the laws of an [abelian group](https://en.wikipedia.org/wiki/Abelian_group)
{-# MINIMAL negate | (-) #-}
negate :: a %1-> a
negate a
x = a
forall a. AddIdentity a => a
zero a %1 -> a %1 -> a
forall a. AdditiveGroup a => a %1 -> a %1 -> a
- a
x
(-) :: a %1-> a %1-> a
a
x - a
y = a
x a %1 -> a %1 -> a
forall a. Additive a => a %1 -> a %1 -> a
+ a %1 -> a
forall a. AdditiveGroup a => a %1 -> a
negate a
y

-- | A numeric type with an associative @(*)@ operation
class Multiplicative a where
(*) :: a %1-> a %1-> a

-- | A 'Multipcative' type with an identity for @(*)@
class Multiplicative a => MultIdentity a where
one :: a

-- | A [semiring](https://en.wikipedia.org/wiki/Semiring) class. This is
-- basically a numeric type with mutliplication, addition and with identities
-- for each. The laws:
--
-- > zero * x = zero
-- > a * (b + c) = (a * b) + (a * c)
class (AddIdentity a, MultIdentity a) => Semiring a where

-- Note:
-- Having a linear (*) means we can't short-circuit multiplication by zero

-- | A 'Ring' instance is a numeric type with @(+)@, @(-)@, @(*)@ and all
-- the following properties: a group with @(+)@ and a 'MultIdentity' with @(*)@
-- along with distributive laws.
class (AdditiveGroup a, Semiring a) => Ring a where

-- | A numeric type that 'Integer's can be embedded into while satisfying
-- all the typeclass laws @Integer@s obey. That is, if there's some property
-- like commutivity of integers @x + y == y + x@, then we must have:
--
-- > fromInteger x + fromInteger y == fromInteger y + fromInteger x
--
-- For mathy folk: @fromInteger@ should be a homomorphism over @(+)@ and @(*)@.
class FromInteger a where
fromInteger :: Prelude.Integer %1-> a

-- XXX: subclass of Prelude.Num? subclass of Eq?
class (Ring a, FromInteger a) => Num a where
{-# MINIMAL abs, signum #-}
-- XXX: is it fine to insist abs,signum are linear? I think it is
abs :: a %1-> a
signum :: a %1-> a

newtype MovableNum a = MovableNum a
deriving (MovableNum a %1 -> ()
(MovableNum a %1 -> ()) -> Consumable (MovableNum a)
forall a. Consumable a => MovableNum a %1 -> ()
forall a. (a %1 -> ()) -> Consumable a
consume :: MovableNum a %1 -> ()
\$cconsume :: forall a. Consumable a => MovableNum a %1 -> ()
Consumable, Consumable (MovableNum a)
Consumable (MovableNum a)
-> (forall (n :: Nat).
KnownNat n =>
MovableNum a %1 -> V n (MovableNum a))
-> (MovableNum a %1 -> (MovableNum a, MovableNum a))
-> Dupable (MovableNum a)
MovableNum a %1 -> (MovableNum a, MovableNum a)
forall (n :: Nat).
KnownNat n =>
MovableNum a %1 -> V n (MovableNum a)
forall a.
Consumable a
-> (forall (n :: Nat). KnownNat n => a %1 -> V n a)
-> (a %1 -> (a, a))
-> Dupable a
forall {a}. Dupable a => Consumable (MovableNum a)
forall a.
Dupable a =>
MovableNum a %1 -> (MovableNum a, MovableNum a)
forall a (n :: Nat).
(Dupable a, KnownNat n) =>
MovableNum a %1 -> V n (MovableNum a)
dup2 :: MovableNum a %1 -> (MovableNum a, MovableNum a)
\$cdup2 :: forall a.
Dupable a =>
MovableNum a %1 -> (MovableNum a, MovableNum a)
dupV :: forall (n :: Nat).
KnownNat n =>
MovableNum a %1 -> V n (MovableNum a)
\$cdupV :: forall a (n :: Nat).
(Dupable a, KnownNat n) =>
MovableNum a %1 -> V n (MovableNum a)
Dupable, Dupable (MovableNum a)
Dupable (MovableNum a)
-> (MovableNum a %1 -> Ur (MovableNum a)) -> Movable (MovableNum a)
MovableNum a %1 -> Ur (MovableNum a)
forall a. Dupable a -> (a %1 -> Ur a) -> Movable a
forall {a}. Movable a => Dupable (MovableNum a)
forall a. Movable a => MovableNum a %1 -> Ur (MovableNum a)
move :: MovableNum a %1 -> Ur (MovableNum a)
\$cmove :: forall a. Movable a => MovableNum a %1 -> Ur (MovableNum a)
Movable, Integer -> MovableNum a
MovableNum a -> MovableNum a
MovableNum a -> MovableNum a -> MovableNum a
(MovableNum a -> MovableNum a -> MovableNum a)
-> (MovableNum a -> MovableNum a -> MovableNum a)
-> (MovableNum a -> MovableNum a -> MovableNum a)
-> (MovableNum a -> MovableNum a)
-> (MovableNum a -> MovableNum a)
-> (MovableNum a -> MovableNum a)
-> (Integer -> MovableNum a)
-> Num (MovableNum a)
forall a. Num a => Integer -> MovableNum a
forall a. Num a => MovableNum a -> MovableNum a
forall a. Num a => MovableNum a -> MovableNum a -> MovableNum a
forall a.
(a -> a -> a)
-> (a -> a -> a)
-> (a -> a -> a)
-> (a -> a)
-> (a -> a)
-> (a -> a)
-> (Integer -> a)
-> Num a
fromInteger :: Integer -> MovableNum a
\$cfromInteger :: forall a. Num a => Integer -> MovableNum a
signum :: MovableNum a -> MovableNum a
\$csignum :: forall a. Num a => MovableNum a -> MovableNum a
abs :: MovableNum a -> MovableNum a
\$cabs :: forall a. Num a => MovableNum a -> MovableNum a
negate :: MovableNum a -> MovableNum a
\$cnegate :: forall a. Num a => MovableNum a -> MovableNum a
* :: MovableNum a -> MovableNum a -> MovableNum a
\$c* :: forall a. Num a => MovableNum a -> MovableNum a -> MovableNum a
- :: MovableNum a -> MovableNum a -> MovableNum a
\$c- :: forall a. Num a => MovableNum a -> MovableNum a -> MovableNum a
+ :: MovableNum a -> MovableNum a -> MovableNum a
\$c+ :: forall a. Num a => MovableNum a -> MovableNum a -> MovableNum a
Prelude.Num)

instance (Movable a, Prelude.Num a) => Additive (MovableNum a) where
+ :: MovableNum a %1 -> MovableNum a %1 -> MovableNum a
(+) = (MovableNum a -> MovableNum a -> MovableNum a)
%1 -> MovableNum a %1 -> MovableNum a %1 -> MovableNum a
forall a b c.
(Movable a, Movable b) =>
(a -> b -> c) %1 -> a %1 -> b %1 -> c
liftU2 MovableNum a -> MovableNum a -> MovableNum a
forall a. Num a => a -> a -> a
(Prelude.+)

instance (Movable a, Prelude.Num a) => AddIdentity (MovableNum a) where
zero :: MovableNum a
zero = a -> MovableNum a
forall a. a -> MovableNum a
MovableNum a
0

instance (Movable a, Prelude.Num a) => AdditiveGroup (MovableNum a) where
(-) = (MovableNum a -> MovableNum a -> MovableNum a)
%1 -> MovableNum a %1 -> MovableNum a %1 -> MovableNum a
forall a b c.
(Movable a, Movable b) =>
(a -> b -> c) %1 -> a %1 -> b %1 -> c
liftU2 MovableNum a -> MovableNum a -> MovableNum a
forall a. Num a => a -> a -> a
(Prelude.-)

instance (Movable a, Prelude.Num a) => Multiplicative (MovableNum a) where
* :: MovableNum a %1 -> MovableNum a %1 -> MovableNum a
(*) = (MovableNum a -> MovableNum a -> MovableNum a)
%1 -> MovableNum a %1 -> MovableNum a %1 -> MovableNum a
forall a b c.
(Movable a, Movable b) =>
(a -> b -> c) %1 -> a %1 -> b %1 -> c
liftU2 MovableNum a -> MovableNum a -> MovableNum a
forall a. Num a => a -> a -> a
(Prelude.*)

instance (Movable a, Prelude.Num a) => MultIdentity (MovableNum a) where
one :: MovableNum a
one = a -> MovableNum a
forall a. a -> MovableNum a
MovableNum a
1

instance (Movable a, Prelude.Num a) => Semiring (MovableNum a) where
instance (Movable a, Prelude.Num a) => Ring (MovableNum a) where

instance (Movable a, Prelude.Num a) => FromInteger (MovableNum a) where
fromInteger :: Integer %1 -> MovableNum a
fromInteger = (Integer -> MovableNum a) %1 -> Integer %1 -> MovableNum a
forall a b (p :: Multiplicity). (a %p -> b) %1 -> a %1 -> b
Unsafe.toLinear Integer -> MovableNum a
forall a. Num a => Integer -> a
Prelude.fromInteger

instance (Movable a, Prelude.Num a) => Num (MovableNum a) where
abs :: MovableNum a %1 -> MovableNum a
abs = (MovableNum a -> MovableNum a)
%1 -> MovableNum a %1 -> MovableNum a
forall a b. Movable a => (a -> b) %1 -> a %1 -> b
liftU MovableNum a -> MovableNum a
forall a. Num a => a -> a
Prelude.abs
signum :: MovableNum a %1 -> MovableNum a
signum = (MovableNum a -> MovableNum a)
%1 -> MovableNum a %1 -> MovableNum a
forall a b. Movable a => (a -> b) %1 -> a %1 -> b
liftU MovableNum a -> MovableNum a
forall a. Num a => a -> a
Prelude.signum

liftU :: (Movable a) => (a -> b) %1-> (a %1-> b)
liftU :: forall a b. Movable a => (a -> b) %1 -> a %1 -> b
liftU a -> b
f a
x = (a -> b) %1 -> Ur a %1 -> b
forall a b. (a -> b) %1 -> Ur a %1 -> b
lifted a -> b
f (a %1 -> Ur a
forall a. Movable a => a %1 -> Ur a
move a
x)
where lifted :: (a -> b) %1-> (Ur a %1-> b)
lifted :: forall a b. (a -> b) %1 -> Ur a %1 -> b
lifted a -> b
g (Ur a
a) = a -> b
g a
a

liftU2 :: (Movable a, Movable b) => (a -> b -> c) %1-> (a %1-> b %1-> c)
liftU2 :: forall a b c.
(Movable a, Movable b) =>
(a -> b -> c) %1 -> a %1 -> b %1 -> c
liftU2 a -> b -> c
f a
x b
y = (a -> b -> c) %1 -> Ur a %1 -> Ur b %1 -> c
forall a b c. (a -> b -> c) %1 -> Ur a %1 -> Ur b %1 -> c
lifted a -> b -> c
f (a %1 -> Ur a
forall a. Movable a => a %1 -> Ur a
move a
x) (b %1 -> Ur b
forall a. Movable a => a %1 -> Ur a
move b
y)
where lifted :: (a -> b -> c) %1-> (Ur a %1-> Ur b %1-> c)
lifted :: forall a b c. (a -> b -> c) %1 -> Ur a %1 -> Ur b %1 -> c
lifted a -> b -> c
g (Ur a
a) (Ur b
b) = a -> b -> c
g a
a b
b

-- A newtype wrapper to give the underlying monoid for an additive structure.
-> (forall b. Integral b => b -> Adding a -> Adding a)
forall b. Integral b => b -> Adding a -> Adding a
forall a.
(a -> a -> a)
-> (NonEmpty a -> a)
-> (forall b. Integral b => b -> a -> a)
-> Semigroup a
stimes :: forall b. Integral b => b -> Adding a -> Adding a
\$cstimes :: forall a b. (Additive a, Integral b) => b -> Adding a -> Adding a

x) = a
x

b = a %1 -> Adding a
forall a. a -> Adding a
a a %1 -> a %1 -> a
forall a. Additive a => a %1 -> a %1 -> a
+ a
b)
mempty = a -> Adding a
forall a. a -> Adding a
forall a. AddIdentity a => a
zero

-- A newtype wrapper to give the underlying monoid for a multiplicative structure.
newtype Multiplying a = Multiplying a
deriving NonEmpty (Multiplying a) -> Multiplying a
Multiplying a -> Multiplying a -> Multiplying a
(Multiplying a -> Multiplying a -> Multiplying a)
-> (NonEmpty (Multiplying a) -> Multiplying a)
-> (forall b. Integral b => b -> Multiplying a -> Multiplying a)
-> Semigroup (Multiplying a)
forall b. Integral b => b -> Multiplying a -> Multiplying a
forall a.
Multiplicative a =>
NonEmpty (Multiplying a) -> Multiplying a
forall a.
Multiplicative a =>
Multiplying a -> Multiplying a -> Multiplying a
forall a b.
(Multiplicative a, Integral b) =>
b -> Multiplying a -> Multiplying a
forall a.
(a -> a -> a)
-> (NonEmpty a -> a)
-> (forall b. Integral b => b -> a -> a)
-> Semigroup a
stimes :: forall b. Integral b => b -> Multiplying a -> Multiplying a
\$cstimes :: forall a b.
(Multiplicative a, Integral b) =>
b -> Multiplying a -> Multiplying a
sconcat :: NonEmpty (Multiplying a) -> Multiplying a
\$csconcat :: forall a.
Multiplicative a =>
NonEmpty (Multiplying a) -> Multiplying a
<> :: Multiplying a -> Multiplying a -> Multiplying a
\$c<> :: forall a.
Multiplicative a =>
Multiplying a -> Multiplying a -> Multiplying a
Prelude.Semigroup via NonLinear (Multiplying a)

getMultiplied :: Multiplying a %1-> a
getMultiplied :: forall a. Multiplying a %1 -> a
getMultiplied (Multiplying a
x) = a
x

instance Multiplicative a => Semigroup (Multiplying a) where
Multiplying a
a <> :: Multiplying a %1 -> Multiplying a %1 -> Multiplying a
<> Multiplying a
b = a %1 -> Multiplying a
forall a. a -> Multiplying a
Multiplying (a
a a %1 -> a %1 -> a
forall a. Multiplicative a => a %1 -> a %1 -> a
* a
b)
instance MultIdentity a => Prelude.Monoid (Multiplying a) where
mempty :: Multiplying a
mempty = a -> Multiplying a
forall a. a -> Multiplying a
Multiplying a
forall a. MultIdentity a => a
one
instance MultIdentity a => Monoid (Multiplying a)

deriving via MovableNum Prelude.Int instance Additive Prelude.Int
deriving via MovableNum Prelude.Double instance Additive Prelude.Double
deriving via MovableNum Prelude.Int instance AddIdentity Prelude.Int
deriving via MovableNum Prelude.Double instance AddIdentity Prelude.Double
deriving via MovableNum Prelude.Int instance AdditiveGroup Prelude.Int
deriving via MovableNum Prelude.Double instance AdditiveGroup Prelude.Double
deriving via MovableNum Prelude.Int instance Multiplicative Prelude.Int
deriving via MovableNum Prelude.Double instance Multiplicative Prelude.Double
deriving via MovableNum Prelude.Int instance MultIdentity Prelude.Int
deriving via MovableNum Prelude.Double instance MultIdentity Prelude.Double
deriving via MovableNum Prelude.Int instance Semiring Prelude.Int
deriving via MovableNum Prelude.Double instance Semiring Prelude.Double
deriving via MovableNum Prelude.Int instance Ring Prelude.Int
deriving via MovableNum Prelude.Double instance Ring Prelude.Double
deriving via MovableNum Prelude.Int instance FromInteger Prelude.Int
deriving via MovableNum Prelude.Double instance FromInteger Prelude.Double
deriving via MovableNum Prelude.Int instance Num Prelude.Int
deriving via MovableNum Prelude.Double instance Num Prelude.Double
```