gistfile1.hs

{-# LANGUAGE EmptyDataDecls, FlexibleContexts, FlexibleInstances, FunctionalDependencies, TypeFamilies, MultiParamTypeClasses, ScopedTypeVariables, TypeOperators, ImplicitParams, RankNTypes, GADTs, GeneralizedNewtypeDeriving, NoImplicitPrelude, TypeSynonymInstances, TypeOperators #-}
module Main where

-- ZOMG failgebra by copumpkin (not intended to be useful, but just as a straggly experiment to see what's possible)

-- TODO: using2 could take a function mapping from common types to wrapper types and maybe reduce ugliness

import Prelude hiding (id, (+), (-), (*), (/), Integral, fromInteger, Real)
import qualified Prelude as P
import Data.Number.CReal 
import Data.Number.Natural
import Data.Ratio

import Control.Applicative

import Control.Functor.Pointed
import Control.Functor.Extras hiding (Natural)
import Control.Functor.Algebra

infixl 7 *
infixl 6 +

type Real = CReal

convert :: (Copointed a, Pointed b) => a :~> b
convert = point . extract

class (Pointed op, Copointed op) => Operation op

newtype Positive a = Positive a deriving (Eq, Show)
newtype Nonnegative a = Nonnegative a deriving (Eq, Show)
newtype Nonpositive a = Nonpositive a deriving (Eq, Show)
newtype Negative a = Negative a deriving (Eq, Show)

newtype Plus a = Plus a deriving (Eq, Show)
newtype Times a = Times a deriving (Eq, Show)
newtype Max a = Max a deriving (Eq, Show)
newtype Min a = Min a deriving (Eq, Show)
newtype And a = And a deriving (Eq, Show)
newtype Or  a = Or a  deriving (Eq, Show)
newtype GCD a = GCD a deriving (Eq, Show)
newtype LCM a = LCM a deriving (Eq, Show)
newtype Append a = Append a deriving (Eq, Show)
newtype Union a = Union a deriving (Eq, Show)
newtype Intersection a = Intersection a deriving (Eq, Show)

instance Pointed Positive where point = Positive
instance Pointed Nonnegative where point = Nonnegative
instance Pointed Nonpositive where point = Nonpositive
instance Pointed Negative where point = Negative

instance Pointed Plus         where point = Plus
instance Pointed Times        where point = Times
instance Pointed Max          where point = Max
instance Pointed Min          where point = Min
instance Pointed And          where point = And
instance Pointed Or           where point = Or
instance Pointed GCD          where point = GCD
instance Pointed LCM          where point = LCM
instance Pointed Append       where point = Append
instance Pointed Union        where point = Union
instance Pointed Intersection where point = Intersection

instance Copointed Positive where extract (Positive a) = a
instance Copointed Nonnegative where extract (Nonnegative a) = a
instance Copointed Nonpositive where extract (Nonpositive a) = a
instance Copointed Negative where extract (Negative a) = a

instance Copointed Plus         where extract (Plus         a) = a
instance Copointed Times        where extract (Times        a) = a
instance Copointed Max          where extract (Max          a) = a
instance Copointed Min          where extract (Min          a) = a
instance Copointed And          where extract (And          a) = a
instance Copointed Or           where extract (Or           a) = a
instance Copointed GCD          where extract (GCD          a) = a
instance Copointed LCM          where extract (LCM          a) = a
instance Copointed Append       where extract (Append       a) = a
instance Copointed Union        where extract (Union        a) = a
instance Copointed Intersection where extract (Intersection a) = a

instance Operation Plus  
instance Operation Times 
instance Operation Max   
instance Operation Min   
instance Operation And   
instance Operation Or    
instance Operation GCD   
instance Operation LCM   
instance Operation Append
instance Operation Union
instance Operation Intersection

instance Functor Positive where fmap f (Positive a) = Positive (f a)
instance Functor Nonnegative where fmap f (Nonnegative a) = Nonnegative (f a)
instance Functor Nonpositive where fmap f (Nonpositive a) = Nonpositive (f a)
instance Functor Negative where fmap f (Negative a) = Negative (f a)

instance Functor Plus    where fmap f (Plus  a) = Plus  (f a)
instance Functor Times   where fmap f (Times a) = Times (f a)
instance Functor Max     where fmap f (Max   a) = Max   (f a)
instance Functor Min     where fmap f (Min   a) = Min   (f a)
instance Functor And     where fmap f (And   a) = And   (f a)
instance Functor Or      where fmap f (Or    a) = Or    (f a)
instance Functor GCD     where fmap f (GCD   a) = GCD   (f a)
instance Functor LCM     where fmap f (LCM   a) = LCM   (f a)

instance Functor Append       where fmap f (Append       a) = Append       (f a)
instance Functor Union        where fmap f (Union        a) = Union        (f a)
instance Functor Intersection where fmap f (Intersection a) = Intersection (f a)


instance Applicative Positive where pure = point; Positive f <*> Positive x = Positive (f x)
instance Applicative Nonnegative where pure = point; Nonnegative f <*> Nonnegative x = Nonnegative (f x)
instance Applicative Nonpositive where pure = point; Nonpositive f <*> Nonpositive x = Nonpositive (f x)
instance Applicative Negative where pure = point; Negative f <*> Negative x = Negative (f x)

instance Applicative Plus  where pure = point; Plus  f <*> Plus  x = Plus  (f x)
instance Applicative Times where pure = point; Times f <*> Times x = Times (f x)
instance Applicative Max   where pure = point; Max   f <*> Max   x = Max   (f x)
instance Applicative Min   where pure = point; Min   f <*> Min   x = Min   (f x)
instance Applicative And   where pure = point; And   f <*> And   x = And   (f x)
instance Applicative Or    where pure = point; Or    f <*> Or    x = Or    (f x)
instance Applicative GCD   where pure = point; GCD   f <*> GCD   x = GCD   (f x)
instance Applicative LCM   where pure = point; LCM   f <*> LCM   x = LCM   (f x)

instance Applicative Append       where pure = point; Append       f <*> Append       x = Append       (f x)
instance Applicative Union        where pure = point; Union        f <*> Union        x = Union        (f x)
instance Applicative Intersection where pure = point; Intersection f <*> Intersection x = Intersection (f x)

class (Operation op) => Magma op a where
  op :: op a -> op a -> op a

using :: (Copointed op) => Coalgebra op a -> op a -> a
using _ = extract

class (Magma op a) => Associative op a

testAssociative :: (Eq a, Associative op a) => op a -> op a -> op a -> Bool
testAssociative x y z = extract ((x `op` y) `op` z) == extract (x `op` (y `op` z))

class (Magma op a) => Commutative op a

testCommutative :: (Eq a, Commutative op a) => op a -> op a -> Bool
testCommutative x y = extract (x `op` y) == extract (y `op` x)

class (Magma op a) => Identity op a where
  id :: op a

testIdentity :: (Eq a, Identity op a) => op a -> Bool
testIdentity x = extract (x `op` id) == extract x

class (Identity op a) => Invertible op a where
  invert :: op a -> op a

testInvertible :: (Eq a, Invertible op a) => op a -> Bool
testInvertible x = extract (x `op` invert x) == extract (id `asTypeOf` x)

class (Magma op a) => Idempotent op a

testIdempotent :: (Eq a, Idempotent op a) => op a -> Bool
testIdempotent x = extract (x `op` x) == extract x

-- Synonyms
class (Associative op a) => Semigroup op a
class (Semigroup op a, Commutative op a) => CommutativeSemigroup op a
class (Semigroup op a, Identity op a) => Monoid op a
class (Monoid op a, Commutative op a) => CommutativeMonoid op a
class (Monoid op a, Invertible op a) => Group op a
class (Group op a, Commutative op a) => CommutativeGroup op a
class (CommutativeSemigroup op a, Idempotent op a) => Semilattice op a
class (Monoid op a, Idempotent op a) => BoundedSemilattice op a

class (Magma f a, Magma s a) => Dimagma f s a

data Element (f :: * -> *) (s :: * -> *) a = Element a
  deriving (Eq, Show)

instance Functor (Element f s) where
  fmap f (Element x) = Element (f x)

instance Pointed (Element f s) where
  point = Element
  
instance Copointed (Element f s) where
  extract (Element a) = a

using2 :: Coalgebra f a -> Coalgebra s a -> Element f s a -> a
using2 _ _ = extract

f2b :: (Operation f) => f a -> Element f s a
f2b = convert

s2b :: (Operation s) => s a -> Element f s a
s2b = convert

b2f :: (Operation f) => Element f s a -> f a
b2f = convert

b2s :: (Operation s) => Element f s a -> s a
b2s = convert

class (Dimagma f s a) => Distributive f s a

-- Oh my!
testDistributive :: forall f s a. (Eq a, Distributive f s a) => Element f s a -> Element f s a -> Element f s a -> Bool
testDistributive a b c = extract (b2s a `op` convert (b2f b `op` b2f c)) == extract ((convert (b2s a `op` b2s b) :: f a) `op` convert (b2s a `op` b2s c))

-- Better name?
class (Dimagma f s a) => Absorbtion f s a

testAbsorbtion :: forall f s a. (Eq a, Distributive f s a) => Element f s a -> Element f s a -> Bool
testAbsorbtion x y = extract (b2f x `op` convert (b2s x `op` b2s y)) == extract x 
                  && extract (b2s x `op` convert (b2f x `op` b2f y)) == extract x

class (Semilattice join a, Semilattice meet a, Absorbtion join meet a) => Lattice join meet a where
  (∨) :: Element join meet a -> Element join meet a -> Element join meet a
  a ∨ b = f2b (b2f a `op` b2f b) 

  (∧) :: Element join meet a -> Element join meet a -> Element join meet a
  a ∧ b = s2b (b2s a `op` b2s b)

class (Lattice join meet a, Distributive join meet a) => DistributiveLattice join meet a -- Synonym
class (Lattice join meet a, BoundedSemilattice join a, BoundedSemilattice meet a) => BoundedLattice join meet a -- Not a synonym, missing additional properties

class (BoundedLattice join meet a) => ComplementedLattice join meet a where
  complement :: Element join meet a -> Element join meet a

class (DistributiveLattice join meet a, ComplementedLattice join meet a) => BooleanAlgebra join meet a

-- TODO: (Semi)Nearrings and asymmetric properties

class (CommutativeMonoid plus a, Monoid times a, Distributive plus times a) => Semiring plus times a where
  zero :: Element plus times a
  zero = f2b id

  (+) :: Element plus times a -> Element plus times a -> Element plus times a
  a + b = f2b (b2f a `op` b2f b)

  one :: Element plus times a
  one = s2b id

  (*) :: Element plus times a -> Element plus times a -> Element plus times a
  a * b = s2b (b2s a `op` b2s b)

class (Semiring plus times a, Idempotent plus a) => Dioid plus times a -- Synonym

class (Semiring plus times a, Invertible plus a) => Ring plus times a where
  (-) :: Element plus times a -> Element plus times a -> Element plus times a
  a - b = f2b $ b2f a `op` invert (b2f b)

class (Ring plus times a, Commutative times a) => CommutativeRing plus times a

class (Ring plus times a, Invertible times a) => DivisionRing plus times a where
  (/) :: Element plus times a -> Element plus times a -> Element plus times a
  a / b = s2b $ b2s a `op` invert (b2s b)

class (CommutativeRing plus times a, Invertible times a) => Field plus times a

-------------------------------------------------------------------------------

class Number a where
  fromInteger :: Integer -> a

instance Number Int where
  fromInteger = P.fromInteger

instance Number Integer where
  fromInteger = P.id
  
instance Number Natural where
  fromInteger = P.fromInteger
  
instance Number Real where
  fromInteger = P.fromInteger
  
instance Number Rational where
  fromInteger = P.fromInteger

instance (Number a) => Number (Element plus times a) where
  fromInteger = point . fromInteger

instance (Number a) => Number (Plus a) where
  fromInteger = point . fromInteger

instance (Number a) => Number (Times a) where
  fromInteger = point . fromInteger

instance (Number a) => Number (Max a) where
  fromInteger = point . fromInteger
  
instance (Number a) => Number (Min a) where
  fromInteger = point . fromInteger
  
instance (P.Integral a, Nat n) => Number (a `Mod` n) where
  fromInteger x | x < natToInteger (undefined :: n) = point $ P.fromInteger x -- point $ P.fromInteger (x `mod` natToInteger (undefined :: n))
                | otherwise = error (show x ++ " is not a valid number mod " ++ show (natToInteger (undefined :: n)))

instance (Number a) => Number (Positive a) where
  fromInteger = point . fromInteger -- TODO: check
  
instance (Number a) => Number (Nonnegative a) where
  fromInteger = point . fromInteger -- TODO: check

instance (Number a) => Number (Nonpositive a) where
  fromInteger = point . fromInteger -- TODO: check

instance (Number a) => Number (Negative a) where
  fromInteger = point . fromInteger -- TODO: check

-------------------------------------------------------------------------------

instance Magma Plus Integer where
  op = liftA2 (P.+)

instance Magma Times Integer where
  op = liftA2 (P.*)

instance Commutative Plus Integer
instance Commutative Times Integer

instance Associative Plus Integer
instance Associative Times Integer

instance Identity Plus Integer where
  id = point 0
  
instance Identity Times Integer where
  id = point 1
  
instance Invertible Plus Integer where
  invert = fmap negate

instance Semigroup Plus Integer
instance Semigroup Times Integer

instance Monoid Plus Integer
instance Monoid Times Integer

instance CommutativeMonoid Plus Integer
instance CommutativeMonoid Times Integer

instance Group Plus Integer
instance CommutativeGroup Plus Integer

instance Dimagma Plus Times Integer

instance Distributive Plus Times Integer

instance Semiring Plus Times Integer

instance Ring Plus Times Integer
instance CommutativeRing Plus Times Integer

-------------------------------------------------------------------------------

instance Magma LCM Natural where
  op = liftA2 lcm

instance Magma GCD Natural where
  op = liftA2 gcd
  
instance Commutative LCM Natural
instance Commutative GCD Natural

instance Associative LCM Natural
instance Associative GCD Natural

instance Identity LCM Natural where
  id = point 1
  
instance Idempotent LCM Natural
instance Idempotent GCD Natural

instance Semigroup LCM Natural
instance Semigroup GCD Natural

instance CommutativeSemigroup LCM Natural
instance CommutativeSemigroup GCD Natural

instance Monoid LCM Natural

instance Dimagma LCM GCD Natural

instance Semilattice LCM Natural
instance Semilattice GCD Natural

instance BoundedSemilattice LCM Natural

instance Absorbtion LCM GCD Natural
instance Distributive LCM GCD Natural

instance Lattice LCM GCD Natural

instance DistributiveLattice LCM GCD Natural

-------------------------------------------------------------------------------

instance Magma Or Bool where
  op = liftA2 (||)
  
instance Magma And Bool where
  op = liftA2 (&&)
  
instance Commutative Or Bool
instance Commutative And Bool

instance Associative Or Bool
instance Associative And Bool

instance Identity Or Bool where
  id = point False
  
instance Identity And Bool where
  id = point True

instance Idempotent Or Bool
instance Idempotent And Bool

instance Semigroup Or Bool
instance Semigroup And Bool

instance CommutativeSemigroup Or Bool
instance CommutativeSemigroup And Bool

instance Monoid Or Bool
instance Monoid And Bool

instance CommutativeMonoid Or Bool
instance CommutativeMonoid And Bool

instance Semilattice Or Bool
instance Semilattice And Bool

instance BoundedSemilattice Or Bool
instance BoundedSemilattice And Bool

instance Dimagma Or And Bool

instance Semiring Or And Bool

instance Absorbtion Or And Bool

instance Lattice Or And Bool
instance BoundedLattice Or And Bool

instance Distributive Or And Bool
instance DistributiveLattice Or And Bool

instance ComplementedLattice Or And Bool where
  complement = fmap not

instance BooleanAlgebra Or And Bool

-------------------------------------------------------------------------------

instance Magma Plus Real where
  op = liftA2 (P.+)
  
instance Magma Times Real where
  op = liftA2 (P.*)

instance Commutative Plus Real
instance Commutative Times Real

instance Associative Plus Real
instance Associative Times Real

instance Identity Plus Real where
  id = point 0

instance Identity Times Real where
  id = point 1

instance Semigroup Plus Real
instance Semigroup Times Real

instance CommutativeSemigroup Plus Real
instance CommutativeSemigroup Times Real

instance Monoid Plus Real
instance Monoid Times Real

instance CommutativeMonoid Plus Real
instance CommutativeMonoid Times Real

instance Invertible Plus Real where
  invert = fmap negate

instance Invertible Times Real where
  invert = fmap (1 P./)
  
instance Group Plus Real
instance Group Times Real

instance CommutativeGroup Plus Real
instance CommutativeGroup Times Real

instance Dimagma Plus Times Real

instance Distributive Plus Times Real

instance Semiring Plus Times Real
instance Ring Plus Times Real
instance CommutativeRing Plus Times Real
instance DivisionRing Plus Times Real
instance Field Plus Times Real

-------------------------------------------------------------------------------

instance Magma Max Integer where
  op = liftA2 max
  
instance Magma Min Integer where
  op = liftA2 min

instance Associative Max Integer
instance Associative Min Integer

instance Semigroup Max Integer
instance Semigroup Min Integer

instance Commutative Max Integer
instance Commutative Min Integer

instance CommutativeSemigroup Max Integer
instance CommutativeSemigroup Min Integer

-------------------------------------------------------------------------------

instance Magma Max Natural where
  op = liftA2 max
  
instance Magma Min Natural where
  op = liftA2 min
  
instance Associative Max Natural
instance Associative Min Natural

instance Semigroup Max Natural
instance Semigroup Min Natural

instance Commutative Max Natural
instance Commutative Min Natural

instance CommutativeSemigroup Max Natural
instance CommutativeSemigroup Min Natural

instance Identity Max Natural where
  id = point 0
  
instance Monoid Max Natural
instance CommutativeMonoid Max Natural

-------------------------------------------------------------------------------

instance Magma Max Real where
  op = liftA2 max
  
instance Magma Min Real where
  op = liftA2 min

instance Associative Max Real
instance Associative Min Real

instance Semigroup Max Real
instance Semigroup Min Real

instance Commutative Max Real
instance Commutative Min Real

instance CommutativeSemigroup Max Real
instance CommutativeSemigroup Min Real

instance Dimagma Max Plus Real
instance Dimagma Min Plus Real
instance Dimagma Max Times Real
instance Dimagma Min Times Real

instance Distributive Max Plus Real
instance Distributive Min Plus Real
instance Distributive Max Times Real
instance Distributive Min Times Real

-------------------------------------------------------------------------------


instance Magma Plus Natural where
  op = liftA2 (P.+)
  
instance Magma Times Natural where
  op = liftA2 (P.*)
  
instance Associative Plus Natural
instance Associative Times Natural

instance Semigroup Plus Natural
instance Semigroup Times Natural

instance Commutative Plus Natural
instance Commutative Times Natural

instance CommutativeSemigroup Plus Natural
instance CommutativeSemigroup Times Natural

instance Identity Plus Natural where
  id = point 0
  
instance Identity Times Natural where
  id = point 1

instance Monoid Plus Natural
instance Monoid Times Natural

instance CommutativeMonoid Plus Natural
instance CommutativeMonoid Times Natural

instance Dimagma Plus Times Natural

instance Distributive Plus Times Natural

instance Semiring Plus Times Natural

-------------------------------------------------------------------------------

-- Don't want to be too general, so limit to plus and times and max and min
instance (Magma Plus a) => Magma Plus (Nonnegative a) where
  (Plus (Nonnegative a)) `op` (Plus (Nonnegative b)) = point . convert $ (point a :: Plus a) `op` point b
  
instance (Magma Times a) => Magma Times (Nonnegative a) where
  (Times (Nonnegative a)) `op` (Times (Nonnegative b)) = point . convert $ (point a :: Times a) `op` point b

instance (Magma Plus a) => Magma Plus (Nonpositive a) where
  (Plus (Nonpositive a)) `op` (Plus (Nonpositive b)) = point . convert $ (point a :: Plus a) `op` point b

instance (Magma Times a) => Magma Times (Nonpositive a) where
  (Times (Nonpositive a)) `op` (Times (Nonpositive b)) = point . convert $ (point a :: Times a) `op` point b


instance (Magma Max a) => Magma Max (Nonnegative a) where
  (Max (Nonnegative a)) `op` (Max (Nonnegative b)) = point . convert $ (point a :: Max a) `op` point b

instance (Magma Max a) => Magma Max (Nonpositive a) where
  (Max (Nonpositive a)) `op` (Max (Nonpositive b)) = point . convert $ (point a :: Max a) `op` point b

instance (Magma Min a) => Magma Min (Nonnegative a) where
  (Min (Nonnegative a)) `op` (Min (Nonnegative b)) = point . convert $ (point a :: Min a) `op` point b

instance (Magma Min a) => Magma Min (Nonpositive a) where
  (Min (Nonpositive a)) `op` (Min (Nonpositive b)) = point . convert $ (point a :: Min a) `op` point b


instance (Associative Plus a) => Associative Plus (Nonnegative a)
instance (Associative Times a) => Associative Times (Nonnegative a)
instance (Associative Plus a) => Associative Plus (Nonpositive a)
instance (Associative Times a) => Associative Times (Nonpositive a)

instance (Associative Max a) => Associative Max (Nonnegative a)
instance (Associative Max a) => Associative Max (Nonpositive a)
instance (Associative Min a) => Associative Min (Nonnegative a)
instance (Associative Min a) => Associative Min (Nonpositive a)


instance (Semigroup Plus a) => Semigroup Plus (Nonnegative a)
instance (Semigroup Times a) => Semigroup Times (Nonnegative a)
instance (Semigroup Plus a) => Semigroup Plus (Nonpositive a)
instance (Semigroup Times a) => Semigroup Times (Nonpositive a)

instance (Semigroup Max a) => Semigroup Max (Nonnegative a)
instance (Semigroup Max a) => Semigroup Max (Nonpositive a)
instance (Semigroup Min a) => Semigroup Min (Nonnegative a)
instance (Semigroup Min a) => Semigroup Min (Nonpositive a)

instance (Commutative Plus a) => Commutative Plus (Nonnegative a)
instance (Commutative Times a) => Commutative Times (Nonnegative a)
instance (Commutative Plus a) => Commutative Plus (Nonpositive a)
instance (Commutative Times a) => Commutative Times (Nonpositive a)

instance (Commutative Max a) => Commutative Max (Nonnegative a)
instance (Commutative Max a) => Commutative Max (Nonpositive a)
instance (Commutative Min a) => Commutative Min (Nonnegative a)
instance (Commutative Min a) => Commutative Min (Nonpositive a)

instance (CommutativeSemigroup Plus a) => CommutativeSemigroup Plus (Nonnegative a)
instance (CommutativeSemigroup Times a) => CommutativeSemigroup Times (Nonnegative a)
instance (CommutativeSemigroup Plus a) => CommutativeSemigroup Plus (Nonpositive a)
instance (CommutativeSemigroup Times a) => CommutativeSemigroup Times (Nonpositive a)

instance (CommutativeSemigroup Max a) => CommutativeSemigroup Max (Nonnegative a)
instance (CommutativeSemigroup Max a) => CommutativeSemigroup Max (Nonpositive a)
instance (CommutativeSemigroup Min a) => CommutativeSemigroup Min (Nonnegative a)
instance (CommutativeSemigroup Min a) => CommutativeSemigroup Min (Nonpositive a)

instance (Identity Plus a) => Identity Plus (Nonnegative a) where
  id = point $ convert (id :: Plus a)
  
instance (Identity Times a) => Identity Times (Nonnegative a) where
  id = point $ convert (id :: Times a)

instance (Identity Plus a) => Identity Plus (Nonpositive a) where
  id = point $ convert (id :: Plus a)

instance (Identity Times a) => Identity Times (Nonpositive a) where
  id = point $ convert (id :: Times a)


instance (Monoid Plus a) => Monoid Plus (Nonnegative a)
instance (Monoid Times a) => Monoid Times (Nonnegative a)
instance (Monoid Plus a) => Monoid Plus (Nonpositive a)
instance (Monoid Times a) => Monoid Times (Nonpositive a)

instance (CommutativeMonoid Plus a) => CommutativeMonoid Plus (Nonnegative a)
instance (CommutativeMonoid Times a) => CommutativeMonoid Times (Nonnegative a)
instance (CommutativeMonoid Plus a) => CommutativeMonoid Plus (Nonpositive a)
instance (CommutativeMonoid Times a) => CommutativeMonoid Times (Nonpositive a)


instance (Dimagma Plus Times a) => Dimagma Plus Times (Nonnegative a)

instance (Distributive Plus Times a) => Distributive Plus Times (Nonnegative a)

instance (Semiring Plus Times a) => Semiring Plus Times (Nonnegative a)

-------------------------------------------------------------------------------

instance Identity Max (Nonnegative Real) where
  id = point . point $ 0
  
instance Monoid Max (Nonnegative Real)
instance CommutativeMonoid Max (Nonnegative Real)

instance Dimagma Max Plus (Nonnegative Real)
instance Dimagma Max Times (Nonnegative Real)

instance Distributive Max Plus (Nonnegative Real)
instance Distributive Max Times (Nonnegative Real)

instance Semiring Max Plus (Nonnegative Real)
instance Semiring Max Times (Nonnegative Real)

-------------------------------------------------------------------------------

instance Identity Min (Nonpositive Real) where
  id = point . point $ 0
  
instance Monoid Min (Nonpositive Real)
instance CommutativeMonoid Min (Nonpositive Real)

instance Dimagma Min Plus (Nonpositive Real)
instance Dimagma Min Times (Nonpositive Real)

instance Distributive Min Plus (Nonpositive Real)
instance Distributive Min Times (Nonpositive Real)

instance Semiring Min Plus (Nonpositive Real)
instance Semiring Min Times (Nonpositive Real)

-------------------------------------------------------------------------------

instance Magma Plus Rational where
  op = liftA2 (P.+)
  
instance Magma Times Rational where
  op = liftA2 (P.*)

instance Commutative Plus Rational
instance Commutative Times Rational

instance Associative Plus Rational
instance Associative Times Rational

instance Identity Plus Rational where
  id = point 0

instance Identity Times Rational where
  id = point 1

instance Semigroup Plus Rational
instance Semigroup Times Rational

instance CommutativeSemigroup Plus Rational
instance CommutativeSemigroup Times Rational

instance Monoid Plus Rational
instance Monoid Times Rational

instance CommutativeMonoid Plus Rational
instance CommutativeMonoid Times Rational

instance Invertible Plus Rational where
  invert = fmap negate

instance Invertible Times Rational where
  invert = fmap (1 P./)
  
instance Group Plus Rational
instance Group Times Rational

instance CommutativeGroup Plus Rational
instance CommutativeGroup Times Rational

instance Dimagma Plus Times Rational

instance Distributive Plus Times Rational

instance Semiring Plus Times Rational
instance Ring Plus Times Rational
instance CommutativeRing Plus Times Rational
instance DivisionRing Plus Times Rational
instance Field Plus Times Rational

-------------------------------------------------------------------------------

instance Magma Append [a] where
  op = liftA2 (++)
  
instance Associative Append [a]
instance Semigroup Append [a]

instance Identity Append [a] where
  id = point []

instance Monoid Append [a]

-------------------------------------------------------------------------------

data Z = Z
newtype S n = S n

newtype I x = I { unI :: x } 
newtype K x y = K { unK :: x }

class Nat n where
  caseNat :: forall r. n -> (n ~ Z => r) -> (forall p. (n ~ S p, Nat p) => p -> r) -> r
  
instance Nat Z where
  caseNat _ z _ = z

instance Nat n => Nat (S n) where
  caseNat (S n) _ s = s n

induction :: forall p n. Nat n => n -> p Z -> (forall x. Nat x => p x -> p (S x)) -> p n
induction n z s = caseNat n isZ isS where 
   isZ :: n ~ Z => p n 
   isZ = z 
   isS :: forall x. (n ~ S x, Nat x) => x -> p n 
   isS x = s (induction x z s)

-- witnessNat = unI $ induction (witnessNat :: n) (I Z) (I . S . unI)
witnessNat :: forall n. Nat n => n 
witnessNat = theWitness where 
  theWitness = unI $ induction theWitness (I Z) (I . S . unI)

data AnyNat where 
  AnyNat :: Nat n => n -> AnyNat 
  
data IsNat n where 
  IsNat :: Nat n => IsNat n

mkNat :: Integer -> AnyNat 
mkNat x | x < 0 = error "Nat must be >= 0" 
mkNat 0 = AnyNat Z 
mkNat x = case (mkNat (pred x)) of (AnyNat n) -> AnyNat (S n)

natToInteger :: Nat n => n -> Integer 
natToInteger n = unK $ induction n (K 0) (K . succ . unK)

instance Eq AnyNat where
  (==) = eqAnyNat

eqAnyNat :: AnyNat -> AnyNat -> Bool
eqAnyNat (AnyNat n) (AnyNat m) = caseNat n (caseNat m True (const False)) (\x -> caseNat m False (\y -> eqAnyNat (AnyNat x) (AnyNat y)))

instance Show AnyNat where 
  showsPrec p (AnyNat n) = showParen (p > 11) (shows (natToInteger n)) 

data Vec a n where
  Nil :: Vec a Z
  Cons :: Nat n => a -> Vec a n -> Vec a (S n)

replicateVec :: (Nat n) => a -> Vec a n
replicateVec a = induction witnessNat Nil (Cons a)

-- Sadly parameter order must be this way to get useful instances, but we can keep the flip around for other stuff
data FlipMod n s = Mod s deriving Eq
type s `Mod` n = FlipMod n s

instance (Show a, Nat n) => Show (a `Mod` n) where
  showsPrec p (Mod x) = showParen (p > 11) (\y -> y ++ (show x ++ " mod " ++ show (AnyNat (undefined :: n))))

instance (Nat n) => Functor (FlipMod n) where
  fmap f (Mod a) = Mod (f a)
  
instance (Nat n) => Pointed (FlipMod n) where
  point = Mod
  
instance (Nat n) => Copointed (FlipMod n) where
  extract (Mod a) = a
  
instance (Nat n) => Applicative (FlipMod n) where
  pure = point
  Mod f <*> Mod a = Mod (f a)
  
-------------------------------------------------------------------------------

instance (Nat n) => Magma Plus (Natural `Mod` n) where
  op = liftA2 (liftA2 (\x y -> (x P.+ y) `mod` (fromIntegral (natToInteger (undefined :: n)))))

instance (Nat n) => Magma Times (Natural `Mod` n) where
  op = liftA2 (liftA2 (\x y -> (x P.* y) `mod` (fromIntegral (natToInteger (undefined :: n)))))

instance (Nat n) => Associative Plus (Natural `Mod` n)
instance (Nat n) => Associative Times (Natural `Mod` n)

instance (Nat n) => Commutative Plus (Natural `Mod` n)
instance (Nat n) => Commutative Times (Natural `Mod` n)

instance (Nat n) => Semigroup Plus (Natural `Mod` n)
instance (Nat n) => Semigroup Times (Natural `Mod` n)

instance (Nat n) => CommutativeSemigroup Plus (Natural `Mod` n)
instance (Nat n) => CommutativeSemigroup Times (Natural `Mod` n)

instance (Nat n) => Identity Plus (Natural `Mod` n) where
  id = point . point $ 0
  
instance (Nat n) => Identity Times (Natural `Mod` n) where
  id = point . point $ 1

instance (Nat n) => Monoid Plus (Natural `Mod` n)
instance (Nat n) => Monoid Times (Natural `Mod` n)

instance (Nat n) => CommutativeMonoid Plus (Natural `Mod` n)
instance (Nat n) => CommutativeMonoid Times (Natural `Mod` n)

instance (Nat n) => Invertible Plus (Natural `Mod` n) where
  invert = fmap . fmap $ \x -> P.fromIntegral ((-(P.fromIntegral x)) `mod` natToInteger (undefined :: n))

-- Stolen from cdsmith's blog!
inverse :: Natural -> Natural -> Natural
inverse q 1 = 1
inverse q p = (n P.* q P.+ 1) `div` p
    where n = p P.- inverse p (q `mod` p)

instance (Nat n) => Invertible Times (Natural `Mod` n) where
  invert = fmap . fmap $ inverse (P.fromIntegral (natToInteger (undefined :: n)))

instance (Nat n) => Group Plus (Natural `Mod` n)
instance (Nat n) => Group Times (Natural `Mod` n)

instance (Nat n) => CommutativeGroup Plus (Natural `Mod` n)
instance (Nat n) => CommutativeGroup Times (Natural `Mod` n)

instance (Nat n) => Dimagma Plus Times (Natural `Mod` n)

instance (Nat n) => Distributive Plus Times (Natural `Mod` n)

instance (Nat n) => Semiring Plus Times (Natural `Mod` n)
instance (Nat n) => Ring Plus Times (Natural `Mod` n)
instance (Nat n) => CommutativeRing Plus Times (Natural `Mod` n)
instance (Nat n) => DivisionRing Plus Times (Natural `Mod` n)
instance (Nat n) => Field Plus Times (Natural `Mod` n)

-------------------------------------------------------------------------------

data Quaternion = Quaternion Real Real Real Real

instance Magma Plus Quaternion where
  Plus (Quaternion a1 b1 c1 d1) `op` Plus (Quaternion a2 b2 c2 d2) = point $ Quaternion (a1 P.+ a2) (b1 P.+ b2) (c1 P.+ c2) (d1 P.+ d2)

instance Magma Times Quaternion where
  Times (Quaternion a1 b1 c1 d1) `op` Times (Quaternion a2 b2 c2 d2) = point $
    Quaternion (a1 P.* a2 P.- b1 P.* b2 P.- c1 P.* c2 P.- d1 P.* d2)
               (a1 P.* b2 P.+ b1 P.* a2 P.+ c1 P.* d2 P.- d1 P.* c2)
               (a1 P.* c2 P.- b1 P.* d2 P.+ c1 P.* a2 P.+ d1 P.* b2)
               (a1 P.* d2 P.+ b1 P.* c2 P.- c1 P.* b2 P.+ d1 P.* a2)

instance Associative Plus Quaternion
instance Associative Times Quaternion

instance Semigroup Plus Quaternion
instance Semigroup Times Quaternion

instance Commutative Plus Quaternion

instance Identity Plus Quaternion where
  id = point (Quaternion 0 0 0 0)
  
instance Identity Times Quaternion where
  id = point (Quaternion 1 0 0 0)
  
instance Monoid Plus Quaternion
instance Monoid Times Quaternion

instance CommutativeSemigroup Plus Quaternion

instance CommutativeMonoid Plus Quaternion

instance Invertible Plus Quaternion where
  invert (Plus (Quaternion a b c d)) = point (Quaternion (-a) (-b) (-c) (-d))

instance Invertible Times Quaternion where
  invert (Times (Quaternion a b c d)) = point (Quaternion (a P./ alpha) (b P./ alpha) (c P./ alpha) (d P./ alpha))
    where alpha = a P.* a P.+ b P.* b P.+ c P.* c P.+ d P.* d

instance Group Plus Quaternion
instance Group Times Quaternion

instance CommutativeGroup Plus Quaternion

instance Dimagma Plus Times Quaternion

instance Distributive Plus Times Quaternion
instance Semiring Plus Times Quaternion
instance Ring Plus Times Quaternion
instance DivisionRing Plus Times Quaternion
instance Field Plus Times Quaternion