{-# LANGUAGE TypeApplications #-}
module Noether.Algebra.Single.Cancellative where

import qualified Prelude                 as P

import           Noether.Algebra.Tags
import           Noether.Lemmata.Prelude hiding (Num)
import           Noether.Lemmata.TypeFu

data CancellativeE
  = CancellativeNum
  | CancellativeFractional
  | CancellativeNamed Symbol CancellativeE
  | CancellativeTagged Type CancellativeE

class CancellativeK (op :: k) a (s :: CancellativeE) where
  cancelK :: Proxy op -> Proxy s -> a -> a

instance P.Num a => CancellativeK Add a CancellativeNum where
  cancelK _ _ = (0 P.-)

instance P.Fractional a => CancellativeK Mul a CancellativeFractional where
  cancelK _ _ = (1 P./)

instance (KnownSymbol sym, CancellativeK op a s) =>
         CancellativeK op a (CancellativeNamed sym s) where
  cancelK opP _ = cancelK opP (Proxy @s)

instance CancellativeK op a s =>
         CancellativeK op (i -> a) (CancellativeTagged FunctionLift s) where
  cancelK o _ f = cancelK' . f
    where
      cancelK' = cancelK o (Proxy @s)

type Cancellative op a = CancellativeK op a (CancellativeS op a)

type family CancellativeS (op :: k) (a :: Type) = (r :: CancellativeE)