{-# 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:
--
-- * Additive ⊆ AddIdentity ⊆ AdditiveGroup
-- * MultIdentity ⊆ MultIdentity
-- * (AddIdentity ∩ MultIdentity) ⊆ Semiring
-- * (AdditiveGroup ∩ Semiring) ⊆ Ring
-- * (FromInteger ∩ Ring) ⊆ Num
--
module Data.Num.Linear
  (
  -- * Num and sub-classes
    Num(..)
  , Additive(..)
  , AddIdentity(..)
  , AdditiveGroup(..)
  , Multiplicative(..)
  , MultIdentity(..)
  , Semiring
  , Ring
  , FromInteger(..)
  -- * Mechanisms for deriving instances
  , Adding(..), getAdded
  , 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
class Additive a where
  (+) :: a %1-> a %1-> a

-- | An 'Additive' type with an identity on @(+)@.
class Additive a => AddIdentity a where
  zero :: a

-- | An 'AddIdentity' with inverses that satisfies
-- the laws of an [abelian group](https://en.wikipedia.org/wiki/Abelian_group)
class AddIdentity a => AdditiveGroup a where
  {-# 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.
newtype Adding a = Adding a
  deriving NonEmpty (Adding a) -> Adding a
Adding a -> Adding a -> Adding a
(Adding a -> Adding a -> Adding a)
-> (NonEmpty (Adding a) -> Adding a)
-> (forall b. Integral b => b -> Adding a -> Adding a)
-> Semigroup (Adding a)
forall b. Integral b => b -> Adding a -> Adding a
forall a. Additive a => NonEmpty (Adding a) -> Adding a
forall a. Additive a => Adding a -> Adding a -> Adding a
forall a b. (Additive a, 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
sconcat :: NonEmpty (Adding a) -> Adding a
$csconcat :: forall a. Additive a => NonEmpty (Adding a) -> Adding a
<> :: Adding a -> Adding a -> Adding a
$c<> :: forall a. Additive a => Adding a -> Adding a -> Adding a
Prelude.Semigroup via NonLinear (Adding a)

getAdded :: Adding a %1-> a
getAdded :: forall a. Adding a %1 -> a
getAdded (Adding a
x) = a
x

instance Additive a => Semigroup (Adding a) where
  Adding a
a <> :: Adding a %1 -> Adding a %1 -> Adding a
<> Adding a
b = a %1 -> Adding a
forall a. a -> Adding a
Adding (a
a a %1 -> a %1 -> a
forall a. Additive a => a %1 -> a %1 -> a
+ a
b)
instance AddIdentity a => Prelude.Monoid (Adding a) where
  mempty :: Adding a
mempty = a -> Adding a
forall a. a -> Adding a
Adding a
forall a. AddIdentity a => a
zero
instance AddIdentity a => Monoid (Adding a)

-- 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