Algebra.hs

{-# LANGUAGE CPP,MagicHash,UnboxedTuples #-}
{-# OPTIONS_GHC -fno-warn-missing-methods #-}
{-# OPTIONS_GHC -fno-warn-incomplete-patterns #-}
{-# OPTIONS_GHC -fno-warn-orphans #-}

-- | This module defines the algebraic type-classes used in subhask.
-- The class hierarchies are significantly more general than those in the standard Prelude.
module SubHask.Algebra
    (
    -- * Comparisons
    Logic
    , ValidLogic
    , ClassicalLogic
    , Eq_ (..)
    , Eq
    , ValidEq
    , law_Eq_reflexive
    , law_Eq_symmetric
    , law_Eq_transitive
    , defn_Eq_noteq
    , POrd_ (..)
    , POrd
    , law_POrd_commutative
    , law_POrd_associative
    , theorem_POrd_idempotent
    , Lattice_ (..)
    , Lattice
    , isChain
    , isAntichain
    , POrdering (..)
    , law_Lattice_commutative
    , law_Lattice_associative
    , theorem_Lattice_idempotent
    , law_Lattice_infabsorption
    , law_Lattice_supabsorption
    , law_Lattice_reflexivity
    , law_Lattice_antisymmetry
    , law_Lattice_transitivity
    , defn_Lattice_greaterthan
    , MinBound_ (..)
    , MinBound
    , law_MinBound_inf
    , Bounded (..)
    , law_Bounded_sup
    , supremum
    , supremum_
    , infimum
    , infimum_
    , Complemented (..)
    , law_Complemented_not
    , Heyting (..)
    , modusPonens
    , law_Heyting_maxbound
    , law_Heyting_infleft
    , law_Heyting_infright
    , law_Heyting_distributive
    , Boolean
    , law_Boolean_infcomplement
    , law_Boolean_supcomplement
    , law_Boolean_infdistributivity
    , law_Boolean_supdistributivity
    , Ord_ (..)
    , law_Ord_totality
    , law_Ord_min
    , law_Ord_max
    , Ord
    , Ordering (..)
    , min
    , max
    , maximum
    , maximum_
    , minimum
    , minimum_
    , argmin
    , argmax
    , Graded (..)
    , law_Graded_fromEnum
    , law_Graded_pred
    , defn_Graded_predN
    , (>.)
    , (<.)
    , Enum (..)
    , law_Enum_toEnum
    , law_Enum_succ
    , defn_Enum_succN

    -- ** Boolean helpers
    , (||)
    , (&&)
    , true
    , false
    , and
    , or

    -- * Set-like
    , Elem
    , infDisjoint
    , SetElem
    , Container (..)
    , law_Container_preservation

    , Constructible (..)
    , Constructible0
    , law_Constructible_singleton
    , defn_Constructible_cons
    , defn_Constructible_snoc
    , defn_Constructible_fromList
    , defn_Constructible_fromListN
    , theorem_Constructible_cons
    , fromString
    , fromList
    , fromListN
    , generate
    , insert
    , empty
    , isEmpty

    , Foldable (..)
    , law_Foldable_sum
    , theorem_Foldable_tofrom
    , defn_Foldable_foldr
    , defn_Foldable_foldr'
    , defn_Foldable_foldl
    , defn_Foldable_foldl'
    , defn_Foldable_foldr1
    , defn_Foldable_foldr1'
    , defn_Foldable_foldl1
    , defn_Foldable_foldl1'

    , foldtree1
    , convertUnfoldable
    , length
    , reduce
    , concat
    , headMaybe
    , tailMaybe
    , lastMaybe
    , initMaybe

    -- *** indexed containers
    , Index
    , SetIndex

    , IxContainer (..)
    , law_IxContainer_preservation
    , defn_IxContainer_bang
    , defn_IxContainer_findWithDefault
    , defn_IxContainer_hasIndex
    , (!?)

    , Sliceable (..)
    , law_Sliceable_restorable
    , law_Sliceable_preservation

    , IxConstructible (..)
    , law_IxConstructible_lookup
    , defn_IxConstructible_consAt
    , defn_IxConstructible_snocAt
    , defn_IxConstructible_fromIxList
    , theorem_IxConstructible_preservation
    , insertAt

    -- * Types
    , CanError (..)
    , Maybe' (..)
    , justs'
    , Labeled' (..)

    -- * Number-like
    -- ** Classes with one operator
    , Semigroup (..)
    , law_Semigroup_associativity
    , defn_Semigroup_plusequal
    , associator
    , cycle
    , Actor
    , Action (..)
    , law_Action_compatibility
    , defn_Action_dotplusequal
    , (+.)
    , Cancellative (..)
    , law_Cancellative_rightminus1
    , law_Cancellative_rightminus2
    , defn_Cancellative_plusequal
    , Monoid (..)
    , isZero
    , notZero
    , law_Monoid_leftid
    , law_Monoid_rightid
    , defn_Monoid_isZero
    , Abelian
    , law_Abelian_commutative
    , Group (..)
    , law_Group_leftinverse
    , law_Group_rightinverse
    , defn_Group_negateminus

    -- ** Classes with two operators
    , Rg(..)
    , law_Rg_multiplicativeAssociativity
    , law_Rg_multiplicativeCommutivity
    , law_Rg_annihilation
    , law_Rg_distributivityLeft
    , theorem_Rg_distributivityRight
    , defn_Rg_timesequal
    , Rig(..)
    , isOne
    , notOne
    , law_Rig_multiplicativeId
    , Rng
    , defn_Ring_fromInteger
    , Ring(..)
    , indicator
    , Integral(..)
    , law_Integral_divMod
    , law_Integral_quotRem
    , law_Integral_toFromInverse
    , roundUpToNearest
--     , roundUpToNearestBase2
    , fromIntegral
    , Field(..)
    , OrdField
    , RationalField(..)
    , convertRationalField
    , toFloat
    , toDouble
    , BoundedField(..)
    , infinity
    , negInfinity
    , ExpRing (..)
    , (^)
    , ExpField (..)
    , Real (..)
    , QuotientField(..)

    -- ** Sizes
    , Normed (..)
    , abs
    , Metric (..)
    , isFartherThan
    , lb2distanceUB
    , law_Metric_nonnegativity
    , law_Metric_indiscernables
    , law_Metric_symmetry
    , law_Metric_triangle

    -- ** Linear algebra
    , Scalar
    , IsScalar
    , HasScalar
    , type (><)
    , Cone (..)
    , Module (..)
    , law_Module_multiplication
    , law_Module_addition
    , law_Module_action
    , law_Module_unital
    , defn_Module_dotstarequal
    , (*.)
    , FreeModule (..)
    , law_FreeModule_commutative
    , law_FreeModule_associative
    , law_FreeModule_id
    , defn_FreeModule_dotstardotequal
    , FiniteModule (..)
    , VectorSpace (..)
    , Reisz (..)
    , Banach (..)
    , law_Banach_distance
    , law_Banach_size
    , Hilbert (..)
    , squaredInnerProductNorm
    , innerProductDistance
    , innerProductNorm
    , TensorAlgebra (..)

    -- * Spatial programming
    , Any (..)
    , All

    -- * Helper functions
    , simpleMutableDefn
    , module SubHask.Mutable
    )
    where

import qualified Prelude as P
import qualified Data.Number.Erf as P
import qualified Math.Gamma as P
import qualified Data.List as L

import Control.Monad hiding (liftM)
import Control.Monad.ST
import Data.Ratio
import Data.Typeable
import Test.QuickCheck (frequency)

import Control.Parallel.Strategies

import GHC.Prim hiding (Any)
import GHC.Types

import SubHask.Internal.Prelude
import SubHask.Category
import SubHask.Mutable


-------------------------------------------------------------------------------
-- Helper functions

-- | Creates a quickcheck property for a simple mutable operator defined using "immutable2mutable"
simpleMutableDefn :: (Eq_ a, IsMutable a)
    => (Mutable (ST s) a -> b -> ST s ()) -- ^ mutable function
    -> (a -> b -> a)              -- ^ create a mutable function using "immutable2mutable"
    -> (a -> b -> Logic a)        -- ^ the output property
simpleMutableDefn mf f a b = unsafeRunMutableProperty $ do
    ma1 <- thaw a
    ma2 <- thaw a
    mf ma1 b
    immutable2mutable f ma2 b
    a1 <- freeze ma1
    a2 <- freeze ma2
    return $ a1==a2

-------------------------------------------------------------------------------
-- relational classes

-- | Every type has an associated logic.
-- Most types use classical logic, which corresponds to the Bool type.
-- But types can use any logical system they want.
-- Functions, for example, use an infinite logic.
-- You probably want your logic to be an instance of "Boolean", but this is not required.
--
-- See wikipedia's articles on <https://en.wikipedia.org/wiki/Algebraic_logic algebraic logic>,
-- and <https://en.wikipedia.org/wiki/Infinitary_logic infinitary logic> for more details.
type family Logic a :: *
type instance Logic Bool = Bool
type instance Logic Char = Bool
type instance Logic Int = Bool
type instance Logic Integer = Bool
type instance Logic Rational = Bool
type instance Logic Float = Bool
type instance Logic Double = Bool
type instance Logic (a->b) = a -> Logic b
type instance Logic () = ()

-- FIXME:
-- This type is only needed to due an apparent ghc bug.
-- See [#10592](https://ghc.haskell.org/trac/ghc/ticket/10592).
-- But there seems to be a workaround now.
type ValidLogic a = Complemented (Logic a)

-- | Classical logic is implemented using the Prelude's Bool type.
type ClassicalLogic a = Logic a ~ Bool

-- | Defines equivalence classes over the type.
-- The values need not have identical representations in the machine to be equal.
--
-- See <https://en.wikipedia.org/wiki/Equivalence_class wikipedia>
-- and <http://ncatlab.org/nlab/show/equivalence+class ncatlab> for more details.
class Eq_ a where

    infix 4 ==
    (==) :: a -> a -> Logic a

    -- | In order to have the "not equals to" relation, your logic must have a notion of "not", and therefore must be "Boolean".
    {-# INLINE (/=) #-}
    infix 4 /=
    (/=) :: ValidLogic a => a -> a -> Logic a
    (/=) = not (==)

law_Eq_reflexive :: Eq a => a -> Logic a
law_Eq_reflexive a = a==a

law_Eq_symmetric :: Eq a => a -> a -> Logic a
law_Eq_symmetric a1 a2 = (a1==a2)==(a2==a1)

law_Eq_transitive :: Eq a => a -> a -> a -> Logic a
law_Eq_transitive a1 a2 a3 = (a1==a2&&a2==a3) ==> (a1==a3)

defn_Eq_noteq :: (Complemented (Logic a), Eq a) => a -> a -> Logic a
defn_Eq_noteq a1 a2 = (a1/=a2) == (not $ a1==a2)

instance Eq_ () where
    {-# INLINE (==) #-}
    () == () = ()

    {-# INLINE (/=) #-}
    () /= () = ()

instance Eq_ Bool     where (==) = (P.==); (/=) = (P./=); {-# INLINE (==) #-}; {-# INLINE (/=) #-}
instance Eq_ Char     where (==) = (P.==); (/=) = (P./=); {-# INLINE (==) #-}; {-# INLINE (/=) #-}
instance Eq_ Int      where (==) = (P.==); (/=) = (P./=); {-# INLINE (==) #-}; {-# INLINE (/=) #-}
instance Eq_ Integer  where (==) = (P.==); (/=) = (P./=); {-# INLINE (==) #-}; {-# INLINE (/=) #-}
instance Eq_ Rational where (==) = (P.==); (/=) = (P./=); {-# INLINE (==) #-}; {-# INLINE (/=) #-}
instance Eq_ Float    where (==) = (P.==); (/=) = (P./=); {-# INLINE (==) #-}; {-# INLINE (/=) #-}
instance Eq_ Double   where (==) = (P.==); (/=) = (P./=); {-# INLINE (==) #-}; {-# INLINE (/=) #-}

instance Eq_ b => Eq_ (a -> b) where
    {-# INLINE (==) #-}
    (f==g) a = f a == g a

type Eq a = (Eq_ a, Logic a~Bool)
type ValidEq a = (Eq_ a, ValidLogic a)

-- class (Eq_ a, Logic a ~ Bool) => Eq a
-- instance (Eq_ a, Logic a ~ Bool) => Eq a
--
-- class (Eq_ a, ValidLogic a) => ValidEq a
-- instance (Eq_ a, ValidLogic a) => ValidEq a

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

-- | This is more commonly known as a "meet" semilattice
class Eq_ b => POrd_ b where
    inf :: b -> b -> b

    {-# INLINE (<=) #-}
    infix 4 <=
    (<=) :: b -> b -> Logic b
    b1 <= b2 = inf b1 b2 == b1

    {-# INLINE (<) #-}
    infix 4 <
    (<) :: Complemented (Logic b) => b -> b -> Logic b
    b1 < b2 = inf b1 b2 == b1 && b1 /= b2

type POrd a = (Eq a, POrd_ a)
-- class (Eq b, POrd_ b) => POrd b
-- instance (Eq b, POrd_ b) => POrd b

law_POrd_commutative :: (Eq b, POrd_ b) => b -> b -> Bool
law_POrd_commutative b1 b2 = inf b1 b2 == inf b2 b1

law_POrd_associative :: (Eq b, POrd_ b) => b -> b -> b -> Bool
law_POrd_associative b1 b2 b3 = inf (inf b1 b2) b3 == inf b1 (inf b2 b3)

theorem_POrd_idempotent :: (Eq b, POrd_ b) => b -> Bool
theorem_POrd_idempotent b = inf b b == b

#define mkPOrd_(x) \
instance POrd_ x where \
    inf = (P.min) ;\
    (<=) = (P.<=) ;\
    (<) = (P.<) ;\
    {-# INLINE inf #-} ;\
    {-# INLINE (<=) #-} ;\
    {-# INLINE (<) #-}

mkPOrd_(Bool)
mkPOrd_(Char)
mkPOrd_(Int)
mkPOrd_(Integer)
mkPOrd_(Float)
mkPOrd_(Double)
mkPOrd_(Rational)

instance POrd_ () where
    {-# INLINE inf #-}
    inf () () = ()

instance POrd_ b => POrd_ (a -> b) where
    {-# INLINE inf #-}
    inf f g = \x -> inf (f x) (g x)

    {-# INLINE (<) #-}
    (f<=g) a = f a <= g a

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

-- | Most Lattice literature only considers 'Bounded' lattices, but here we have both upper and lower bounded lattices.
--
-- prop> minBound <= b || not (minBound > b)
--
class POrd_ b => MinBound_ b where
    minBound :: b

type MinBound a = (Eq a, MinBound_ a)
-- class (Eq b, MinBound_ b) => MinBound b
-- instance (Eq b, MinBound_ b) => MinBound b

law_MinBound_inf :: (Eq b, MinBound_ b) => b -> Bool
law_MinBound_inf b = inf b minBound == minBound

-- | "false" is an upper bound because `a && false = false` for all a.
{-# INLINE false #-}
false :: MinBound_ b => b
false = minBound

instance MinBound_ ()       where minBound = ()         ; {-# INLINE minBound #-}
instance MinBound_ Bool     where minBound = False      ; {-# INLINE minBound #-}
instance MinBound_ Char     where minBound = P.minBound ; {-# INLINE minBound #-}
instance MinBound_ Int      where minBound = P.minBound ; {-# INLINE minBound #-}
instance MinBound_ Float    where minBound = -1/0       ; {-# INLINE minBound #-}
instance MinBound_ Double   where minBound = -1/0       ; {-# INLINE minBound #-}
-- FIXME: should be a primop for this

instance MinBound_ b => MinBound_ (a -> b) where minBound = \_ -> minBound ; {-# INLINE minBound #-}

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

-- | Represents all the possible ordering relations in a classical logic (i.e. Logic a ~ Bool)
data POrdering
    = PLT
    | PGT
    | PEQ
    | PNA
    deriving (Read,Show)

type instance Logic POrdering = Bool

instance Arbitrary POrdering where
    arbitrary = frequency
        [ (1, P.return PLT)
        , (1, P.return PGT)
        , (1, P.return PEQ)
        , (1, P.return PNA)
        ]

instance Eq_ POrdering where
    {-# INLINE (==) #-}
    PLT == PLT = True
    PGT == PGT = True
    PEQ == PEQ = True
    PNA == PNA = True
    _ == _ = False

-- | FIXME: there are many semigroups over POrdering;
-- how should we represent the others? newtypes?
instance Semigroup POrdering where
    {-# INLINE (+) #-}
    PEQ + x = x
    PLT + _ = PLT
    PGT + _ = PGT
    PNA + _ = PNA

type instance Logic Ordering = Bool

instance Eq_ Ordering where
    {-# INLINE (==) #-}
    EQ == EQ = True
    LT == LT = True
    GT == GT = True
    _  == _  = False

instance Semigroup Ordering where
    {-# INLINE (+) #-}
    EQ + x = x
    LT + _ = LT
    GT + _ = GT

instance Monoid POrdering where
    {-# INLINE zero #-}
    zero = PEQ

instance Monoid Ordering where
    {-# INLINE zero #-}
    zero = EQ


-- |
--
--
-- See <https://en.wikipedia.org/wiki/Lattice_%28order%29 wikipedia> for more details.
class POrd_ b => Lattice_ b where
    sup :: b -> b -> b

    {-# INLINE (>=) #-}
    infix 4 >=
    (>=) :: b -> b -> Logic b
    b1 >= b2 = sup b1 b2 == b1

    {-# INLINE (>) #-}
    infix 4 >
    (>) :: Boolean (Logic b) => b -> b -> Logic b
    b1 > b2 = sup b1 b2 == b1 && b1 /= b2

    -- | This function does not make sense on non-classical logics
    --
    -- FIXME: there are probably related functions for all these other logics;
    -- is there a nice way to represent them all?
    {-# INLINABLE pcompare #-}
    pcompare :: Logic b ~ Bool => b -> b -> POrdering
    pcompare a b = if a==b
        then PEQ
        else if a < b
            then PLT
            else if a > b
                then PGT
                else PNA

type Lattice a = (Eq a, Lattice_ a)
-- class (Eq b, Lattice_ b) => Lattice b
-- instance (Eq b, Lattice_ b) => Lattice b

law_Lattice_commutative :: (Eq b, Lattice_ b) => b -> b -> Bool
law_Lattice_commutative b1 b2 = sup b1 b2 == sup b2 b1

law_Lattice_associative :: (Eq b, Lattice_ b) => b -> b -> b -> Bool
law_Lattice_associative b1 b2 b3 = sup (sup b1 b2) b3 == sup b1 (sup b2 b3)

theorem_Lattice_idempotent :: (Eq b, Lattice_ b) => b -> Bool
theorem_Lattice_idempotent b = sup b b == b

law_Lattice_infabsorption :: (Eq b, Lattice b) => b -> b -> Bool
law_Lattice_infabsorption b1 b2 = inf b1 (sup b1 b2) == b1

law_Lattice_supabsorption :: (Eq b, Lattice b) => b -> b -> Bool
law_Lattice_supabsorption b1 b2 = sup b1 (inf b1 b2) == b1

law_Lattice_reflexivity :: Lattice a => a -> Logic a
law_Lattice_reflexivity a = a<=a

law_Lattice_antisymmetry :: Lattice a => a -> a -> Logic a
law_Lattice_antisymmetry a1 a2
    | a1 <= a2 && a2 <= a1 = a1 == a2
    | otherwise = true

law_Lattice_transitivity :: Lattice a => a -> a -> a -> Logic a
law_Lattice_transitivity  a1 a2 a3
    | a1 <= a2 && a2 <= a3 = a1 <= a3
    | a1 <= a3 && a3 <= a2 = a1 <= a2
    | a2 <= a1 && a1 <= a3 = a2 <= a3
    | a2 <= a3 && a3 <= a1 = a2 <= a1
    | a3 <= a2 && a2 <= a1 = a3 <= a1
    | a3 <= a1 && a1 <= a2 = a3 <= a2
    | otherwise = true

defn_Lattice_greaterthan :: Lattice a => a -> a -> Logic a
defn_Lattice_greaterthan a1 a2
    | a1 < a2 = a2 >= a1
    | a1 > a2 = a2 <= a1
    | otherwise = true

#define mkLattice_(x)\
instance Lattice_ x where \
    sup = (P.max) ;\
    (>=) = (P.>=) ;\
    (>) = (P.>) ;\
    {-# INLINE sup #-} ;\
    {-# INLINE (>=) #-} ;\
    {-# INLINE (>) #-}

mkLattice_(Bool)
mkLattice_(Char)
mkLattice_(Int)
mkLattice_(Integer)
mkLattice_(Float)
mkLattice_(Double)
mkLattice_(Rational)

instance Lattice_ () where
    {-# INLINE sup #-}
    sup () () = ()

instance Lattice_ b => Lattice_ (a -> b) where
    {-# INLINE sup #-}
    sup f g = \x -> sup (f x) (g x)

    {-# INLINE (>=) #-}
    (f>=g) a = f a >= g a

{-# INLINE (&&) #-}
infixr 3 &&
(&&) :: Lattice_ b => b -> b -> b
(&&) = inf

{-# INLINE (||) #-}
infixr 2 ||
(||) :: Lattice_ b => b -> b -> b
(||) = sup

-- | A chain is a collection of elements all of which can be compared
{-# INLINABLE isChain #-}
isChain :: Lattice a => [a] -> Logic a
isChain [] = true
isChain (x:xs) = all (/=PNA) (map (pcompare x) xs) && isChain xs

-- | An antichain is a collection of elements none of which can be compared
--
-- See <http://en.wikipedia.org/wiki/Antichain wikipedia> for more details.
--
-- See also the article on <http://en.wikipedia.org/wiki/Dilworth%27s_theorem Dilward's Theorem>.
{-# INLINABLE isAntichain #-}
isAntichain :: Lattice a => [a] -> Logic a
isAntichain [] = true
isAntichain (x:xs) = all (==PNA) (map (pcompare x) xs) && isAntichain xs

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

-- | An element of a graded lattice has a unique predecessor.
--
-- See <https://en.wikipedia.org/wiki/Graded_poset wikipedia> for more details.
class Lattice b => Graded b where
    -- | Algebrists typically call this function the "rank" of the element in the poset;
    -- however we use the name from the standard prelude instead
    fromEnum :: b -> Int

    -- | The predecessor in the ordering
    pred :: b -> b

    -- | Repeatedly apply the "pred" function
    predN :: Int -> b -> b
    predN i b
        | i  < 0 = error $ "predN called on negative number "++show i
        | i == 0 = b
        | i  > 0 = predN (i-1) $ pred b

law_Graded_fromEnum :: (Lattice b, Graded b) => b -> b -> Bool
law_Graded_fromEnum b1 b2
    | b1 <  b2  = fromEnum b1 <  fromEnum b2
    | b1 >  b2  = fromEnum b1 >  fromEnum b2
    | b1 == b2  = fromEnum b1 == fromEnum b2
    | otherwise = True

law_Graded_pred :: Graded b => b -> b -> Bool
law_Graded_pred b1 _ = fromEnum (pred b1) == fromEnum b1-1
                     || fromEnum (pred b1) == fromEnum b1

defn_Graded_predN :: Graded b => Int -> b -> Bool
defn_Graded_predN i b
    | i < 0 = true
    | otherwise = go i b == predN i b
    where
        go 0 b' = b'
        go i' b' = go (i'-1) $ pred b'

instance Graded Bool where
    {-# INLINE pred #-}
    pred True = False
    pred False = False

    {-# INLINE fromEnum #-}
    fromEnum True = 1
    fromEnum False = 0

instance Graded Int where
    {-# INLINE pred #-}
    pred i = if i == minBound
        then i
        else i-1

    {-# INLINE predN #-}
    predN n i = if i-n <= i
        then i-n
        else minBound

    {-# INLINE fromEnum #-}
    fromEnum = id

instance Graded Char where
    {-# INLINE pred #-}
    pred c = if c=='\NUL'
        then '\NUL'
        else P.pred c

    {-# INLINE fromEnum #-}
    fromEnum = P.fromEnum

instance Graded Integer where
    {-# INLINE pred #-}
    pred = P.pred

    {-# INLINE predN #-}
    predN n i = i - toInteger n

    {-# INLINE fromEnum #-}
    fromEnum = P.fromEnum

{-# INLINE (<.) #-}
(<.) :: (Lattice b, Graded b) => b -> b -> Bool
b1 <. b2 = b1 == pred b2

-- | In a well founded ordering, every element (except possibly the "maxBound" if it exists) has a successor element.
-- We use the "Enum" to represent well founded orderings to maintain consistency with the standard Prelude.
--
-- See <http://ncatlab.org/nlab/show/well-founded+relation ncatlab> for more info.
class (Graded b, Ord_ b) => Enum b where
    -- | The next element in the ordering
    succ :: b -> b

    -- | Advance many elements into the ordering.
    -- This value may be negative to move backwards.
    succN :: Int -> b -> b
    succN i b = toEnum $ fromEnum b + i

    -- | Given an index (also called a rank) of an element, return the element
    toEnum :: Int -> b

law_Enum_toEnum :: Enum b => b -> Bool
law_Enum_toEnum b = toEnum (fromEnum b) == b

law_Enum_succ :: Enum b => b -> b -> Bool
law_Enum_succ b1 _ = fromEnum (succ b1) == fromEnum b1+1
                   || fromEnum (succ b1) == fromEnum b1

defn_Enum_succN :: Enum b => Int -> b -> Logic b
defn_Enum_succN i b = succN i b == toEnum (fromEnum b + i)

instance Enum Bool where
    {-# INLINE succ #-}
    succ True = True
    succ False = True

    {-# INLINE toEnum #-}
    toEnum i
        | i > 0 = True
        | otherwise = False

instance Enum Int where
    {-# INLINE succ #-}
    succ i = if i == maxBound
        then i
        else i+1

    {-# INLINE toEnum #-}
    toEnum = id

instance Enum Char where
    {-# INLINE succ #-}
    succ = P.succ

    {-# INLINE toEnum #-}
    toEnum i = if i < 0
        then P.toEnum 0
        else P.toEnum i

instance Enum Integer where
    {-# INLINE succ #-}
    succ = P.succ

    {-# INLINE toEnum #-}
    toEnum = P.toEnum


{-# INLINE (>.) #-}
(>.) :: (Lattice b, Enum b) => b -> b -> Bool
b1 >. b2 = b1 == succ b2

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

-- | This is the class of total orderings.
--
-- See https://en.wikipedia.org/wiki/Total_order
class Lattice_ a => Ord_ a where
    compare :: (Logic a~Bool, Ord_ a) => a -> a -> Ordering
    compare a1 a2 = case pcompare a1 a2 of
        PLT -> LT
        PGT -> GT
        PEQ -> EQ
        PNA -> error "PNA given by pcompare on a totally ordered type"

law_Ord_totality :: Ord a => a -> a -> Bool
law_Ord_totality a1 a2 = a1 <= a2 || a2 <= a1

law_Ord_min :: Ord a => a -> a -> Bool
law_Ord_min a1 a2 = min a1 a2 == a1
                 || min a1 a2 == a2

law_Ord_max :: Ord a => a -> a -> Bool
law_Ord_max a1 a2 = max a1 a2 == a1
                 || max a1 a2 == a2

{-# INLINE min #-}
min :: Ord_ a => a -> a -> a
min = inf

{-# INLINE max #-}
max :: Ord_ a => a -> a -> a
max = sup

type Ord a = (Eq a, Ord_ a)

instance Ord_ ()
instance Ord_ Char      where compare = P.compare ; {-# INLINE compare #-}
instance Ord_ Int       where compare = P.compare ; {-# INLINE compare #-}
instance Ord_ Integer   where compare = P.compare ; {-# INLINE compare #-}
instance Ord_ Float     where compare = P.compare ; {-# INLINE compare #-}
instance Ord_ Double    where compare = P.compare ; {-# INLINE compare #-}
instance Ord_ Rational  where compare = P.compare ; {-# INLINE compare #-}
instance Ord_ Bool      where compare = P.compare ; {-# INLINE compare #-}

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

-- | A Bounded lattice is a lattice with both a minimum and maximum element
--
class (Lattice_ b, MinBound_ b) => Bounded b where
    maxBound :: b

law_Bounded_sup :: (Eq b, Bounded b) => b -> Bool
law_Bounded_sup b = sup b maxBound == maxBound

-- | "true" is an lower bound because `a && true = true` for all a.
{-# INLINE true #-}
true :: Bounded b => b
true = maxBound

instance Bounded ()     where maxBound = ()         ; {-# INLINE maxBound #-}
instance Bounded Bool   where maxBound = True       ; {-# INLINE maxBound #-}
instance Bounded Char   where maxBound = P.maxBound ; {-# INLINE maxBound #-}
instance Bounded Int    where maxBound = P.maxBound ; {-# INLINE maxBound #-}
instance Bounded Float  where maxBound = 1/0        ; {-# INLINE maxBound #-}
instance Bounded Double where maxBound = 1/0        ; {-# INLINE maxBound #-}
-- FIXME: should be a primop for infinity

instance Bounded b => Bounded (a -> b) where
    {-# INLINE maxBound #-}
    maxBound = \_ -> maxBound

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

class Bounded b => Complemented b where
    not :: b -> b

law_Complemented_not :: (ValidLogic b, Complemented b) => b -> Logic b
law_Complemented_not b = not (true  `asTypeOf` b) == false
                      && not (false `asTypeOf` b) == true

instance Complemented ()   where
    {-# INLINE not #-}
    not () = ()

instance Complemented Bool where
    {-# INLINE not #-}
    not = P.not

instance Complemented b => Complemented (a -> b) where
    {-# INLINE not #-}
    not f = \x -> not $ f x

-- | Heyting algebras are lattices that support implication, but not necessarily the law of excluded middle.
--
-- ==== Laws
-- There is a single, simple law that Heyting algebras must satisfy:
--
-- prop> a ==> b = c   ===>   a && c < b
--
-- ==== Theorems
-- From the laws, we automatically get the properties of:
--
-- distributivity
--
-- See <https://en.wikipedia.org/wiki/Heyting_algebra wikipedia> for more details.
--
-- Note that while Heyting algebras are abelian semigroups with respect to &&, they are not in general cancellative.
class Bounded b => Heyting b where
    -- | FIXME: think carefully about infix
    infixl 3 ==>
    (==>) :: b -> b -> b

law_Heyting_maxbound :: (Eq b, Heyting b) => b -> Bool
law_Heyting_maxbound b = (b ==> b) == maxBound

law_Heyting_infleft :: (Eq b, Heyting b) => b -> b -> Bool
law_Heyting_infleft b1 b2 = (b1 && (b1 ==> b2)) == (b1 && b2)

law_Heyting_infright :: (Eq b, Heyting b) => b -> b -> Bool
law_Heyting_infright b1 b2 = (b2 && (b1 ==> b2)) == b2

law_Heyting_distributive :: (Eq b, Heyting b) => b -> b -> b -> Bool
law_Heyting_distributive b1 b2 b3 = (b1 ==> (b2 && b3)) == ((b1 ==> b2) && (b1 ==> b3))

-- | FIXME: add the axioms for intuitionist logic, which are theorems based on these laws
--

-- | Modus ponens gives us a default definition for "==>" in a "Boolean" algebra.
-- This formula is guaranteed to not work in a "Heyting" algebra that is not "Boolean".
--
-- See <https://en.wikipedia.org/wiki/Modus_ponens wikipedia> for more details.
modusPonens :: Boolean b => b -> b -> b
modusPonens b1 b2 = not b1 || b2

instance Heyting ()   where
    {-# INLINE (==>) #-}
    () ==> () = ()

instance Heyting Bool where
    {-# INLINE (==>) #-}
    (==>) = modusPonens

instance Heyting b => Heyting (a -> b) where
    {-# INLINE (==>) #-}
    (f==>g) a = f a ==> g a

-- | Generalizes Boolean variables.
--
-- See <https://en.wikipedia.org/wiki/Boolean_algebra_%28structure%29 wikipedia> for more details.
class (Complemented b, Heyting b) => Boolean b where

law_Boolean_infcomplement :: (Eq b, Boolean b) => b -> Bool
law_Boolean_infcomplement b = (b || not b) == true

law_Boolean_supcomplement :: (Eq b, Boolean b) => b -> Bool
law_Boolean_supcomplement b = (b && not b) == false

law_Boolean_infdistributivity :: (Eq b, Boolean b) => b -> b -> b -> Bool
law_Boolean_infdistributivity b1 b2 b3 = (b1 || (b2 && b3)) == ((b1 || b2) && (b1 || b3))

law_Boolean_supdistributivity :: (Eq b, Boolean b) => b -> b -> b -> Bool
law_Boolean_supdistributivity b1 b2 b3 = (b1 && (b2 || b3)) == ((b1 && b2) || (b1 && b3))

instance Boolean ()
instance Boolean Bool
instance Boolean b => Boolean (a -> b)

-------------------------------------------------------------------------------
-- numeric classes

class IsMutable g => Semigroup g where
    {-# MINIMAL (+) | (+=) #-}

    {-# INLINE (+) #-}
    infixl 6 +
    (+) :: g -> g -> g
    (+) = mutable2immutable (+=)

    {-# INLINE (+=) #-}
    infixr 5 +=
    (+=) :: (PrimBase m) => Mutable m g -> g -> m ()
    (+=) = immutable2mutable (+)

law_Semigroup_associativity :: (Eq g, Semigroup g ) => g -> g -> g -> Logic g
law_Semigroup_associativity g1 g2 g3 = g1 + (g2 + g3) == (g1 + g2) + g3

defn_Semigroup_plusequal :: (Eq_ g, Semigroup g, IsMutable g) => g -> g -> Logic g
defn_Semigroup_plusequal = simpleMutableDefn (+=) (+)

-- | Measures the degree to which a Semigroup obeys the associative law.
--
-- FIXME: Less-than-perfect associativity should be formalized in the class laws somehow.
associator :: (Semigroup g, Metric g) => g -> g -> g -> Scalar g
associator g1 g2 g3 = distance ((g1+g2)+g3) (g1+(g2+g3))

-- | A generalization of 'Data.List.cycle' to an arbitrary 'Semigroup'.
-- May fail to terminate for some values in some semigroups.
cycle :: Semigroup m => m -> m
cycle xs = xs' where xs' = xs + xs'

instance Semigroup Int      where (+) = (P.+) ; {-# INLINE (+) #-}
instance Semigroup Integer  where (+) = (P.+) ; {-# INLINE (+) #-}
instance Semigroup Float    where (+) = (P.+) ; {-# INLINE (+) #-}
instance Semigroup Double   where (+) = (P.+) ; {-# INLINE (+) #-}
instance Semigroup Rational where (+) = (P.+) ; {-# INLINE (+) #-}

instance Semigroup () where
    {-# INLINE (+) #-}
    ()+() = ()

instance Semigroup   b => Semigroup   (a -> b) where
    {-# INLINE (+) #-}
    f+g = \a -> f a + g a

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

-- | This type class is only used by the "Action" class.
-- It represents the semigroup that acts on our type.
type family Actor s

-- | Semigroup actions let us apply a semigroup to a set.
-- The theory of Modules is essentially the theory of Ring actions.
-- (See <http://mathoverflow.net/questions/100565/why-are-ring-actions-much-harder-to-find-than-group-actions mathoverflow>.)
-- That is why the two classes use similar notation.
--
-- See <https://en.wikipedia.org/wiki/Semigroup_action wikipedia> for more detail.
--
-- FIXME: These types could probably use a more expressive name.
--
-- FIXME: We would like every Semigroup to act on itself, but this results in a class cycle.
class (IsMutable s, Semigroup (Actor s)) => Action s where
    {-# MINIMAL (.+) | (.+=) #-}

    {-# INLINE (.+) #-}
    infixl 6 .+
    (.+) :: s -> Actor s -> s
    (.+) = mutable2immutable (.+=)

    {-# INLINE (.+=) #-}
    infixr 5 .+=
    (.+=) :: (PrimBase m) => Mutable m s -> Actor s -> m ()
    (.+=) = immutable2mutable (.+)

law_Action_compatibility :: (Eq_ s, Action s) => Actor s -> Actor s -> s -> Logic s
law_Action_compatibility a1 a2 s = (a1+a2) +. s == a1 +. a2 +. s

defn_Action_dotplusequal :: (Eq_ s, Action s, Logic (Actor s)~Logic s) => s -> Actor s -> Logic s
defn_Action_dotplusequal = simpleMutableDefn (.+=) (.+)

-- | > s .+ a = a +. s
{-# INLINE (+.) #-}
infixr 6 +.
(+.) :: Action s => Actor s -> s -> s
a +. s = s .+ a

type instance Actor Int      = Int
type instance Actor Integer  = Integer
type instance Actor Float    = Float
type instance Actor Double   = Double
type instance Actor Rational = Rational
type instance Actor ()       = ()
type instance Actor (a->b)   = a->Actor b

instance Action Int      where (.+) = (+) ; {-# INLINE (.+) #-}
instance Action Integer  where (.+) = (+) ; {-# INLINE (.+) #-}
instance Action Float    where (.+) = (+) ; {-# INLINE (.+) #-}
instance Action Double   where (.+) = (+) ; {-# INLINE (.+) #-}
instance Action Rational where (.+) = (+) ; {-# INLINE (.+) #-}
instance Action ()       where (.+) = (+) ; {-# INLINE (.+) #-}

instance Action b => Action (a->b) where
    {-# INLINE (.+) #-}
    f.+g = \x -> f x.+g x

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

class Semigroup g => Monoid g where
    zero :: g

-- | FIXME: this should be in the Monoid class, but putting it there requires a lot of changes to Eq
isZero :: (Monoid g, ValidEq g) => g -> Logic g
isZero = (==zero)

-- | FIXME: this should be in the Monoid class, but putting it there requires a lot of changes to Eq
notZero :: (Monoid g, ValidEq g) => g -> Logic g
notZero = (/=zero)

law_Monoid_leftid :: (Monoid g, Eq g) => g -> Bool
law_Monoid_leftid g = zero + g == g

law_Monoid_rightid :: (Monoid g, Eq g) => g -> Bool
law_Monoid_rightid g = g + zero == g

defn_Monoid_isZero :: (Monoid g, Eq g) => g -> Bool
defn_Monoid_isZero g = (isZero $ zero `asTypeOf` g)
                    && (g /= zero ==> not isZero g)

---------

instance Monoid Int       where zero = 0 ; {-# INLINE zero #-}
instance Monoid Integer   where zero = 0 ; {-# INLINE zero #-}
instance Monoid Float     where zero = 0 ; {-# INLINE zero #-}
instance Monoid Double    where zero = 0 ; {-# INLINE zero #-}
instance Monoid Rational  where zero = 0 ; {-# INLINE zero #-}

instance Monoid () where
    {-# INLINE zero #-}
    zero = ()

instance Monoid b => Monoid (a -> b) where
    {-# INLINE zero #-}
    zero = \_ -> zero

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

-- | In a cancellative semigroup,
--
-- 1)
--
-- > a + b = a + c   ==>   b = c
-- so
-- > (a + b) - b = a + (b - b) = a
--
-- 2)
--
-- > b + a = c + a   ==>   b = c
-- so
-- > -b + (b + a) = (-b + b) + a = a
--
-- This allows us to define "subtraction" in the semigroup.
-- If the semigroup is embeddable in a group, subtraction can be thought of as performing the group subtraction and projecting the result back into the domain of the cancellative semigroup.
-- It is an open problem to fully characterize which cancellative semigroups can be embedded into groups.
--
-- See <http://en.wikipedia.org/wiki/Cancellative_semigroup wikipedia> for more details.
class Semigroup g => Cancellative g where
    {-# MINIMAL (-) | (-=) #-}

    {-# INLINE (-) #-}
    infixl 6 -
    (-) :: g -> g -> g
    (-) = mutable2immutable (-=)

    {-# INLINE (-=) #-}
    infixr 5 -=
    (-=) :: (PrimBase m) => Mutable m g -> g -> m ()
    (-=) = immutable2mutable (-)


law_Cancellative_rightminus1 :: (Eq g, Cancellative g) => g -> g -> Bool
law_Cancellative_rightminus1 g1 g2 = (g1 + g2) - g2 == g1

law_Cancellative_rightminus2 :: (Eq g, Cancellative g) => g -> g -> Bool
law_Cancellative_rightminus2 g1 g2 = g1 + (g2 - g2) == g1

defn_Cancellative_plusequal :: (Eq_ g, Cancellative g) => g -> g -> Logic g
defn_Cancellative_plusequal = simpleMutableDefn (-=) (-)

instance Cancellative Int        where (-) = (P.-) ; {-# INLINE (-) #-}
instance Cancellative Integer    where (-) = (P.-) ; {-# INLINE (-) #-}
instance Cancellative Float      where (-) = (P.-) ; {-# INLINE (-) #-}
instance Cancellative Double     where (-) = (P.-) ; {-# INLINE (-) #-}
instance Cancellative Rational   where (-) = (P.-) ; {-# INLINE (-) #-}

instance Cancellative () where
    {-# INLINE (-) #-}
    ()-() = ()

instance Cancellative b => Cancellative (a -> b) where
    {-# INLINE (-) #-}
    f-g = \a -> f a - g a

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

class (Cancellative g, Monoid g) => Group g where
    {-# INLINE negate #-}
    negate :: g -> g
    negate g = zero - g

defn_Group_negateminus :: (Eq g, Group g) => g -> g -> Bool
defn_Group_negateminus g1 g2 = g1 + negate g2 == g1 - g2

law_Group_leftinverse :: (Eq g, Group g) => g -> Bool
law_Group_leftinverse g = negate g + g == zero

law_Group_rightinverse :: (Eq g, Group g) => g -> Bool
law_Group_rightinverse g = g + negate g == zero

instance Group Int        where negate = P.negate ; {-# INLINE negate #-}
instance Group Integer    where negate = P.negate ; {-# INLINE negate #-}
instance Group Float      where negate = P.negate ; {-# INLINE negate #-}
instance Group Double     where negate = P.negate ; {-# INLINE negate #-}
instance Group Rational   where negate = P.negate ; {-# INLINE negate #-}

instance Group () where
    {-# INLINE negate #-}
    negate () = ()

instance Group b => Group (a -> b) where
    {-# INLINE negate #-}
    negate f = negate . f

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

class Semigroup m => Abelian m

law_Abelian_commutative :: (Abelian g, Eq g) => g -> g -> Bool
law_Abelian_commutative g1 g2 = g1 + g2 == g2 + g1

instance Abelian Int
instance Abelian Integer
instance Abelian Float
instance Abelian Double
instance Abelian Rational

instance Abelian ()

instance Abelian b => Abelian (a -> b)

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

-- | A Rg is a Ring without multiplicative identity or negative numbers.
-- (Hence the removal of the i and n from the name.)
--
-- There is no standard terminology for this structure.
-- They might also be called \"semirings without identity\", \"pre-semirings\", or \"hemirings\".
-- See <http://math.stackexchange.com/questions/359437/name-for-a-semiring-minus-multiplicative-identity-requirement this stackexchange question> for a discussion on naming.
--
class (Abelian r, Monoid r) => Rg r where
    {-# MINIMAL (*) | (*=) #-}

    {-# INLINE (*) #-}
    infixl 7 *
    (*) :: r -> r -> r
    (*) = mutable2immutable (*=)

    {-# INLINE (*=) #-}
    infixr 5 *=
    (*=) :: (PrimBase m) => Mutable m r -> r -> m ()
    (*=) = immutable2mutable (*)

law_Rg_multiplicativeAssociativity :: (Eq r, Rg r) => r -> r -> r -> Bool
law_Rg_multiplicativeAssociativity r1 r2 r3 = (r1 * r2) * r3 == r1 * (r2 * r3)

law_Rg_multiplicativeCommutivity :: (Eq r, Rg r) => r -> r -> Bool
law_Rg_multiplicativeCommutivity r1 r2 = r1*r2 == r2*r1

law_Rg_annihilation :: (Eq r, Rg r) => r -> Bool
law_Rg_annihilation r = r * zero == zero

law_Rg_distributivityLeft :: (Eq r, Rg r) => r -> r -> r -> Bool
law_Rg_distributivityLeft r1 r2 r3 = r1*(r2+r3) == r1*r2+r1*r3

theorem_Rg_distributivityRight :: (Eq r, Rg r) => r -> r -> r -> Bool
theorem_Rg_distributivityRight r1 r2 r3 = (r2+r3)*r1 == r2*r1+r3*r1

defn_Rg_timesequal :: (Eq_ g, Rg g) => g -> g -> Logic g
defn_Rg_timesequal = simpleMutableDefn (*=) (*)

instance Rg Int         where (*) = (P.*) ; {-# INLINE (*) #-}
instance Rg Integer     where (*) = (P.*) ; {-# INLINE (*) #-}
instance Rg Float       where (*) = (P.*) ; {-# INLINE (*) #-}
instance Rg Double      where (*) = (P.*) ; {-# INLINE (*) #-}
instance Rg Rational    where (*) = (P.*) ; {-# INLINE (*) #-}

instance Rg b => Rg (a -> b) where
    {-# INLINE (*) #-}
    f*g = \a -> f a * g a

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

-- | A Rig is a Rg with multiplicative identity.
-- They are also known as semirings.
--
-- See <https://en.wikipedia.org/wiki/Semiring wikipedia>
-- and <http://ncatlab.org/nlab/show/rig ncatlab>
-- for more details.
class (Monoid r, Rg r) => Rig r where
    -- | the multiplicative identity
    one :: r

-- | FIXME: this should be in the Rig class, but putting it there requires a lot of changes to Eq
isOne :: (Rig g, ValidEq g) => g -> Logic g
isOne = (==one)

-- | FIXME: this should be in the Rig class, but putting it there requires a lot of changes to Eq
notOne :: (Rig g, ValidEq g) => g -> Logic g
notOne = (/=one)

law_Rig_multiplicativeId :: (Eq r, Rig r) => r -> Bool
law_Rig_multiplicativeId r = r * one == r && one * r == r

instance Rig Int         where one = 1 ; {-# INLINE one #-}
instance Rig Integer     where one = 1 ; {-# INLINE one #-}
instance Rig Float       where one = 1 ; {-# INLINE one #-}
instance Rig Double      where one = 1 ; {-# INLINE one #-}
instance Rig Rational    where one = 1 ; {-# INLINE one #-}

instance Rig b => Rig (a -> b) where
    {-# INLINE one #-}
    one = \_ -> one

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

-- | A "Ring" without identity.
type Rng r = (Rg r, Group r)

-- |
--
-- It is not part of the standard definition of rings that they have a "fromInteger" function.
-- It follows from the definition, however, that we can construct such a function.
-- The "slowFromInteger" function is this standard construction.
--
-- See <https://en.wikipedia.org/wiki/Ring_%28mathematics%29 wikipedia>
-- and <http://ncatlab.org/nlab/show/ring ncatlab>
-- for more details.
--
-- FIXME:
-- We can construct a "Module" from any ring by taking (*)=(.*.).
-- Thus, "Module" should be a superclass of "Ring".
-- Currently, however, this creates a class cycle, so we can't do it.
-- A number of type signatures are therefore more complicated than they need to be.
class (Rng r, Rig r) => Ring r where
    fromInteger :: Integer -> r
    fromInteger = slowFromInteger

defn_Ring_fromInteger :: (Eq r, Ring r) => r -> Integer -> Bool
defn_Ring_fromInteger r i = fromInteger i `asTypeOf` r
                         == slowFromInteger i

-- | Here we construct an element of the Ring based on the additive and multiplicative identities.
-- This function takes O(n) time, where n is the size of the Integer.
-- Most types should be able to compute this value significantly faster.
--
-- FIXME: replace this with peasant multiplication.
slowFromInteger :: forall r. (Rng r, Rig r) => Integer -> r
slowFromInteger i = if i>0
    then          foldl' (+) zero $ P.map (const (one::r)) [1..        i]
    else negate $ foldl' (+) zero $ P.map (const (one::r)) [1.. negate i]

instance Ring Int         where fromInteger = P.fromInteger ; {-# INLINE fromInteger #-}
instance Ring Integer     where fromInteger = P.fromInteger ; {-# INLINE fromInteger #-}
instance Ring Float       where fromInteger = P.fromInteger ; {-# INLINE fromInteger #-}
instance Ring Double      where fromInteger = P.fromInteger ; {-# INLINE fromInteger #-}
instance Ring Rational    where fromInteger = P.fromInteger ; {-# INLINE fromInteger #-}

instance Ring b => Ring (a -> b) where
    {-# INLINE fromInteger #-}
    fromInteger i = \_ -> fromInteger i

{-# INLINABLE indicator #-}
indicator :: Ring r => Bool -> r
indicator True = 1
indicator False = 0

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

-- | 'Integral' numbers can be formed from a wide class of things that behave
-- like integers, but intuitively look nothing like integers.
--
-- FIXME: All Fields are integral domains; should we make it a subclass?  This would have the (minor?) problem of making the Integral class have to be an approximate embedding.
-- FIXME: Not all integral domains are homomorphic to the integers (e.g. a field)
--
-- See wikipedia on <https://en.wikipedia.org/wiki/Integral_element integral elements>,
--  <https://en.wikipedia.org/wiki/Integral_domain integral domains>,
-- and the <https://en.wikipedia.org/wiki/Ring_of_integers ring of integers>.
class Ring a => Integral a where
    toInteger :: a -> Integer

    infixl 7  `quot`, `rem`

    -- | truncates towards zero
    {-# INLINE quot #-}
    quot :: a -> a -> a
    quot a1 a2 = fst (quotRem a1 a2)

    {-# INLINE rem #-}
    rem :: a -> a -> a
    rem a1 a2 = snd (quotRem a1 a2)

    quotRem :: a -> a -> (a,a)


    infixl 7 `div`, `mod`

    -- | truncates towards negative infinity
    {-# INLINE div #-}
    div :: a -> a -> a
    div a1 a2 = fst (divMod a1 a2)

    {-# INLINE mod #-}
    mod :: a -> a -> a
    mod a1 a2 = snd (divMod a1 a2)

    divMod :: a -> a -> (a,a)


law_Integral_divMod :: (Eq a, Integral a) => a -> a -> Bool
law_Integral_divMod a1 a2 = if a2 /= 0
    then a2 * (a1 `div` a2) + (a1 `mod` a2) == a1
    else True

law_Integral_quotRem :: (Eq a, Integral a) => a -> a -> Bool
law_Integral_quotRem a1 a2 = if a2 /= 0
    then a2 * (a1 `quot` a2) + (a1 `rem` a2) == a1
    else True

law_Integral_toFromInverse :: (Eq a, Integral a) => a -> Bool
law_Integral_toFromInverse a = fromInteger (toInteger a) == a

{-# INLINE[1] fromIntegral #-}
fromIntegral :: (Integral a, Ring b) => a -> b
fromIntegral = fromInteger . toInteger

-- | FIXME:
-- This should be moved into the class hierarchy and generalized.
--
-- FIXME:
-- There are more efficient implementations available if you restrict m to powers of 2.
-- Is GHC smart enough to convert `rem` into bit shifts?
-- See for more possibilities:
-- http://stackoverflow.com/questions/3407012/c-rounding-up-to-the-nearest-multiple-of-a-number
{-# INLINE roundUpToNearest #-}
roundUpToNearest :: Int -> Int -> Int
roundUpToNearest m x = x + m - 1 - (x-1)`rem`m
-- roundUpToNearest m x = if s==0
--     then
--     else x+r
--     where
--         s = x`rem`m
--         r = if s==0 then 0 else m-s

-- FIXME:
-- need more RULES; need tests
{-# RULES
"subhask/fromIntegral/Int->Int" fromIntegral = id :: Int -> Int
    #-}

instance Integral Int where
    {-# INLINE div #-}
    {-# INLINE mod #-}
    {-# INLINE divMod #-}
    {-# INLINE quot #-}
    {-# INLINE rem #-}
    {-# INLINE quotRem #-}
    {-# INLINE toInteger #-}
    div = P.div
    mod = P.mod
    divMod = P.divMod
    quot = P.quot
    rem = P.rem
    quotRem = P.quotRem
    toInteger = P.toInteger

instance Integral Integer where
    {-# INLINE div #-}
    {-# INLINE mod #-}
    {-# INLINE divMod #-}
    {-# INLINE quot #-}
    {-# INLINE rem #-}
    {-# INLINE quotRem #-}
    {-# INLINE toInteger #-}
    div = P.div
    mod = P.mod
    divMod = P.divMod
    quot = P.quot
    rem = P.rem
    quotRem = P.quotRem
    toInteger = P.toInteger

instance Integral b => Integral (a -> b) where
    {-# INLINE div #-}
    {-# INLINE mod #-}
    {-# INLINE divMod #-}
    {-# INLINE quot #-}
    {-# INLINE rem #-}
    {-# INLINE quotRem #-}
    {-# INLINE toInteger #-}
    quot f1 f2 = \a -> quot (f1 a) (f2 a)
    rem f1 f2 = \a -> rem (f1 a) (f2 a)
    quotRem f1 f2 = (quot f1 f2, rem f1 f2)

    div f1 f2 = \a -> div (f1 a) (f2 a)
    mod f1 f2 = \a -> mod (f1 a) (f2 a)
    divMod f1 f2 = (div f1 f2, mod f1 f2)

    -- FIXME
    toInteger = error "toInteger shouldn't be in the integral class b/c of bad function instance"

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

-- | Fields are Rings with a multiplicative inverse.
--
-- See <https://en.wikipedia.org/wiki/Field_%28mathematics%29 wikipedia>
-- and <http://ncatlab.org/nlab/show/field ncatlab>
-- for more details.
class Ring r => Field r where
    {-# INLINE reciprocal #-}
    reciprocal :: r -> r
    reciprocal r = one/r

    {-# INLINE (/) #-}
    infixl 7 /
    (/) :: r -> r -> r
    n/d = n * reciprocal d

--     infixr 5 /=
--     (/=) :: (PrimBase m) => Mutable m g -> g -> m ()
--     (/=) = immutable2mutable (/)

    {-# INLINE fromRational #-}
    fromRational :: Rational -> r
    fromRational r = fromInteger (numerator r) / fromInteger (denominator r)

#define mkField(x) \
instance Field x where \
    (/) = (P./) ;\
    fromRational=P.fromRational ;\
    {-# INLINE fromRational #-} ;\
    {-# INLINE (/) #-}

mkField(Float)
mkField(Double)
mkField(Rational)

instance Field b => Field (a -> b) where
    {-# INLINE fromRational #-}
    reciprocal f = reciprocal . f

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

-- | Ordered fields are generalizations of the rational numbers that maintain most of the nice properties.
-- In particular, all finite fields and the complex numbers are NOT ordered fields.
--
-- See <http://en.wikipedia.org/wiki/Ordered_field wikipedia> for more details.
class (Field r, Ord r, Normed r, IsScalar r) => OrdField r

instance OrdField Float
instance OrdField Double
instance OrdField Rational

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

-- | The prototypical example of a bounded field is the extended real numbers.
-- Other examples are the extended hyperreal numbers and the extended rationals.
-- Each of these fields has been extensively studied, but I don't know of any studies of this particular abstraction of these fields.
--
-- See <https://en.wikipedia.org/wiki/Extended_real_number_line wikipedia> for more details.
class (OrdField r, Bounded r) => BoundedField r where
    {-# INLINE nan #-}
    nan :: r
    nan = 0/0

    isNaN :: r -> Bool

{-# INLINE infinity #-}
infinity :: BoundedField r => r
infinity = maxBound

{-# INLINE negInfinity #-}
negInfinity :: BoundedField r => r
negInfinity = minBound

instance BoundedField Float  where isNaN = P.isNaN ; {-# INLINE isNaN #-}
instance BoundedField Double where isNaN = P.isNaN ; {-# INLINE isNaN #-}

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

-- | A Rational field is a field with only a single dimension.
--
-- FIXME: this isn't part of standard math; why is it here?
class Field r => RationalField r where
    toRational :: r -> Rational

instance RationalField Float    where  toRational=P.toRational ; {-# INLINE toRational #-}
instance RationalField Double   where  toRational=P.toRational ; {-# INLINE toRational #-}
instance RationalField Rational where  toRational=P.toRational ; {-# INLINE toRational #-}

{-# INLINE convertRationalField #-}
convertRationalField :: (RationalField a, RationalField b) => a -> b
convertRationalField = fromRational . toRational

-- |
--
-- FIXME:
-- These functions don't work for Int's, but they should
toFloat :: RationalField a => a -> Float
toFloat = convertRationalField

toDouble :: RationalField a => a -> Double
toDouble = convertRationalField

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

-- | A 'QuotientField' is a field with an 'IntegralDomain' as a subring.
-- There may be many such subrings (for example, every field has itself as an integral domain subring).
-- This is especially true in Haskell because we have different data types that represent essentially the same ring (e.g. "Int" and "Integer").
-- Therefore this is a multiparameter type class.
-- The 'r' parameter represents the quotient field, and the 's' parameter represents the subring.
-- The main purpose of this class is to provide functions that map elements in 'r' to elements in 's' in various ways.
--
-- FIXME: Need examples.  Is there a better representation?
--
-- See <http://en.wikipedia.org/wiki/Field_of_fractions wikipedia> for more details.
--
class (Ring r, Integral s) => QuotientField r s where
    truncate    :: r -> s
    round       :: r -> s
    ceiling     :: r -> s
    floor       :: r -> s

    (^^)        :: r -> s -> r

#define mkQuotientField(r,s) \
instance QuotientField r s where \
    truncate = P.truncate; \
    round    = P.round; \
    ceiling  = P.ceiling; \
    floor    = P.floor; \
    (^^)     = (P.^^); \
    {-# INLINE truncate #-} ;\
    {-# INLINE round #-} ;\
    {-# INLINE ceiling #-} ;\
    {-# INLINE floor #-} ;\
    {-# INLINE (^^) #-} ;\

mkQuotientField(Float,Int)
mkQuotientField(Float,Integer)
mkQuotientField(Double,Int)
mkQuotientField(Double,Integer)
mkQuotientField(Rational,Int)
mkQuotientField(Rational,Integer)

-- mkQuotientField(Integer,Integer)
-- mkQuotientField(Int,Int)

instance QuotientField b1 b2 => QuotientField (a -> b1) (a -> b2) where
    truncate f = \a -> truncate $ f a
    round f = \a -> round $ f a
    ceiling f = \a -> ceiling $ f a
    floor f = \a -> floor $ f a
    (^^) f1 f2 = \a -> (^^) (f1 a) (f2 a)

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

-- | Rings augmented with the ability to take exponents.
--
-- Not all rings have this ability.
-- Consider the ring of rational numbers (represented by "Rational" in Haskell).
-- Raising any rational to an integral power results in another rational.
-- But raising to a fractional power results in an irrational number.
-- For example, the square root of 2.
--
-- See <http://en.wikipedia.org/wiki/Exponential_field#Exponential_rings wikipedia> for more detail.
--
-- FIXME:
-- This class hierarchy doesn't give a nice way exponentiate the integers.
-- We need to add instances for all the quotient groups.
class Ring r => ExpRing r where
    (**) :: r -> r -> r
    infixl 8 **

    logBase :: r -> r -> r

-- | An alternate form of "(**)" that some people find more convenient.
(^) :: ExpRing r => r -> r -> r
(^) = (**)

instance ExpRing Float where
    {-# INLINE (**) #-}
    (**) = (P.**)

    {-# INLINE logBase #-}
    logBase = P.logBase

instance ExpRing Double where
    {-# INLINE (**) #-}
    (**) = (P.**)

    {-# INLINE logBase #-}
    logBase = P.logBase

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

-- | Fields augmented with exponents and logarithms.
--
-- Technically, there are fields for which only a subset of the functions below are meaningful.
-- But these fields don't have any practical computational uses that I'm aware of.
-- So I've combined them all into a single class for simplicity.
--
-- See <http://en.wikipedia.org/wiki/Exponential_field wikipedia> for more detail.
class (ExpRing r, Field r) => ExpField r where
    sqrt :: r -> r
    sqrt r = r**(1/2)

    exp :: r -> r
    log :: r -> r

instance ExpField Float where
    sqrt = P.sqrt
    log = P.log
    exp = P.exp

instance ExpField Double where
    sqrt = P.sqrt
    log = P.log
    exp = P.exp

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

-- | This is a catch-all class for things the real numbers can do but don't exist in other classes.
--
-- FIXME:
-- Factor this out into a more appropriate class hierarchy.
-- For example, some (all?) trig functions need to move to a separate class in order to support trig in finite fields (see <https://en.wikipedia.org/wiki/Trigonometry_in_Galois_fields wikipedia>).
--
-- FIXME:
-- This class is misleading/incorrect for complex numbers.
--
-- FIXME:
-- There's a lot more functions that need adding.
class ExpField r => Real r where
    gamma :: r -> r
    lnGamma :: r -> r
    erf :: r -> r
    pi :: r
    sin :: r -> r
    cos :: r -> r
    tan :: r -> r
    asin :: r -> r
    acos :: r -> r
    atan :: r -> r
    sinh :: r -> r
    cosh :: r -> r
    tanh :: r -> r
    asinh :: r -> r
    acosh :: r -> r
    atanh :: r -> r

instance Real Float where
    gamma = P.gamma
    lnGamma = P.lnGamma
    erf = P.erf

    pi = P.pi

    sin = P.sin
    cos = P.cos
    tan = P.tan
    asin = P.asin
    acos = P.acos
    atan = P.atan
    sinh = P.sinh
    cosh = P.cosh
    tanh = P.tanh
    asinh = P.asinh
    acosh = P.acosh
    atanh = P.atanh

instance Real Double where
    gamma = P.gamma
    lnGamma = P.lnGamma
    erf = P.erf

    pi = P.pi

    sin = P.sin
    cos = P.cos
    tan = P.tan
    asin = P.asin
    acos = P.acos
    atan = P.atan
    sinh = P.sinh
    cosh = P.cosh
    tanh = P.tanh
    asinh = P.asinh
    acosh = P.acosh
    atanh = P.atanh

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

type family Scalar m

infixr 8 ><
type family (><) (a::k1) (b::k2) :: *
type instance Int       >< Int        = Int
type instance Integer   >< Integer    = Integer
type instance Float     >< Float      = Float
type instance Double    >< Double     = Double
type instance Rational  >< Rational   = Rational

-- type instance (a,b)     >< Scalar b   = (a,b)
-- type instance (a,b,c)   >< Scalar b   = (a,b,c)

type instance (a -> b)  >< c          = a -> (b><c)
-- type instance c         >< (a -> b)   = a -> (c><b)

-- | A synonym that covers everything we intuitively thing scalar variables should have.
type IsScalar r = (Ring r, Ord_ r, Scalar r~r, Normed r, ClassicalLogic r, r~(r><r))

-- | A (sometimes) more convenient version of "IsScalar".
type HasScalar a = IsScalar (Scalar a)

type instance Scalar Int      = Int
type instance Scalar Integer  = Integer
type instance Scalar Float    = Float
type instance Scalar Double   = Double
type instance Scalar Rational = Rational

type instance Scalar (a,b) = Scalar a
type instance Scalar (a,b,c) = Scalar a
type instance Scalar (a,b,c,d) = Scalar a

type instance Scalar (a -> b) = Scalar b

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

-- | FIXME: What constraint should be here? Semigroup?
--
-- See <http://ncatlab.org/nlab/show/normed%20group ncatlab>
class
    ( Ord_ (Scalar g)
    , Scalar (Scalar g) ~ Scalar g
    , Ring (Scalar g)
    ) => Normed g where
    size :: g -> Scalar g

    sizeSquared :: g -> Scalar g
    sizeSquared g = s*s
        where
            s = size g

abs :: IsScalar g => g -> g
abs = size

instance Normed Int       where size = P.abs
instance Normed Integer   where size = P.abs
instance Normed Float     where size = P.abs
instance Normed Double    where size = P.abs
instance Normed Rational  where size = P.abs

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

-- | A Cone is an \"almost linear\" subspace of a module.
-- Examples include the cone of positive real numbers and the cone of positive semidefinite matrices.
--
-- See <http://en.wikipedia.org/wiki/Cone_%28linear_algebra%29 wikipedia> for more details.
--
-- FIXME:
-- There are many possible laws for cones (as seen in the wikipedia article).
-- I need to explicitly formulate them here.
-- Intuitively, the laws should apply the module operations and then project back into the "closest point" in the cone.
--
-- FIXME:
-- We're using the definition of a cone from linear algebra.
-- This definition is closely related to the definition from topology.
-- What is needed to ensure our definition generalizes to topological cones?
-- See <http://en.wikipedia.org/wiki/Cone_(topology) wikipedia>
-- and <http://ncatlab.org/nlab/show/cone ncatlab> for more details.
class (Cancellative m, HasScalar m, Rig (Scalar m)) => Cone m where
    infixl 7 *..
    (*..) :: Scalar m -> m -> m

    infixl 7 ..*..
    (..*..) :: m -> m -> m

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

class
    ( Abelian v
    , Group v
    , HasScalar v
    , v ~ (v><Scalar v)
--     , v ~ (Scalar v><v)
    ) => Module v
        where

    {-# MINIMAL (.*) | (.*=) #-}

    -- | Scalar multiplication.
    {-# INLINE (.*) #-}
    infixl 7 .*
    (.*) :: v -> Scalar v -> v
    (.*) = mutable2immutable (.*=)

    {-# INLINE (.*=) #-}
    infixr 5 .*=
    (.*=) :: (PrimBase m) => Mutable m v -> Scalar v -> m ()
    (.*=) = immutable2mutable (.*)

law_Module_multiplication :: (Eq_ m, Module m) => m -> m -> Scalar m -> Logic m
law_Module_multiplication m1 m2 s = s *. (m1 + m2) == s*.m1 + s*.m2

law_Module_addition :: (Eq_ m, Module m) => m -> Scalar m -> Scalar m -> Logic m
law_Module_addition  m s1 s2 = (s1+s2)*.m == s1*.m + s2*.m

law_Module_action :: (Eq_ m, Module m) => m -> Scalar m -> Scalar m -> Logic m
law_Module_action m s1 s2 = s1*.(s2*.m) == (s1*s2)*.m

law_Module_unital :: (Eq_ m, Module m) => m -> Logic m
law_Module_unital m = 1 *. m == m

defn_Module_dotstarequal :: (Eq_ m, Module m) => m -> Scalar m -> Logic m
defn_Module_dotstarequal = simpleMutableDefn (.*=) (.*)


{-# INLINE (*.) #-}
infixl 7 *.
(*.) :: Module v => Scalar v -> v -> v
r *. v  = v .* r

instance Module Int       where (.*) = (*)
instance Module Integer   where (.*) = (*)
instance Module Float     where (.*) = (*)
instance Module Double    where (.*) = (*)
instance Module Rational  where (.*) = (*)

instance
    ( Module b
    ) => Module (a -> b)
        where
    f .*  b = \a -> f a .*  b

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

-- | Free modules have a basis.
-- This means it makes sense to perform operations elementwise on the basis coefficients.
--
-- See <https://en.wikipedia.org/wiki/Free_module wikipedia> for more detail.
class Module v => FreeModule v where

    {-# MINIMAL ones, ((.*.) | (.*.=)) #-}

    -- | Multiplication of the components pointwise.
    -- For matrices, this is commonly called Hadamard multiplication.
    --
    -- See <http://en.wikipedia.org/wiki/Hadamard_product_%28matrices%29 wikipedia> for more detail.
    --
    -- FIXME: This is only valid for modules with a basis.
    {-# INLINE (.*.) #-}
    infixl 7 .*.
    (.*.) :: v -> v -> v
    (.*.) = mutable2immutable (.*.=)

    {-# INLINE (.*.=) #-}
    infixr 5 .*.=
    (.*.=) :: (PrimBase m) => Mutable m v -> v -> m ()
    (.*.=) = immutable2mutable (.*.)

    -- | The identity for Hadamard multiplication.
    -- Intuitively, this object has the value "one" in every column.
    ones :: v

law_FreeModule_commutative :: (Eq_ m, FreeModule m) => m -> m -> Logic m
law_FreeModule_commutative m1 m2 = m1.*.m2 == m2.*.m1

law_FreeModule_associative :: (Eq_ m, FreeModule m) => m -> m -> m -> Logic m
law_FreeModule_associative m1 m2 m3 = m1.*.(m2.*.m3) == (m1.*.m2).*.m3

law_FreeModule_id :: (Eq_ m, FreeModule m) => m -> Logic m
law_FreeModule_id m = m == m.*.ones

defn_FreeModule_dotstardotequal :: (Eq_ m, FreeModule m) => m -> m -> Logic m
defn_FreeModule_dotstardotequal = simpleMutableDefn (.*.=) (.*.)

instance FreeModule Int       where (.*.) = (*); ones = one
instance FreeModule Integer   where (.*.) = (*); ones = one
instance FreeModule Float     where (.*.) = (*); ones = one
instance FreeModule Double    where (.*.) = (*); ones = one
instance FreeModule Rational  where (.*.) = (*); ones = one

instance
    ( FreeModule b
    ) => FreeModule (a -> b)
        where
    g .*. f = \a -> g a .*. f a
    ones = \_ -> ones

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

-- | If our "FreeModule" has a finite basis, then we can:
--
-- * index into the modules basis coefficients
--
-- * provide a dense construction method that's a bit more convenient than "fromIxList".
class
    ( FreeModule v
    , IxContainer v
    , Elem v~Scalar v
    , Index v~Int
    , v ~ SetElem v (Elem v)
    ) => FiniteModule v
        where
    -- | Returns the dimension of the object.
    -- For some objects, this may be known statically, and so the parameter will not be "seq"ed.
    -- But for others, this may not be known statically, and so the parameter will be "seq"ed.
    dim :: v -> Int

    unsafeToModule :: [Scalar v] -> v

type instance Elem Int      = Int
type instance Elem Integer  = Integer
type instance Elem Float    = Float
type instance Elem Double   = Double
type instance Elem Rational = Rational

type instance SetElem Int      a = Int
type instance SetElem Integer  a = Integer
type instance SetElem Float    a = Float
type instance SetElem Double   a = Double
type instance SetElem Rational a = Rational

type instance Index Int      = Int
type instance Index Integer  = Int
type instance Index Float    = Int
type instance Index Double   = Int
type instance Index Rational = Int

type instance SetIndex Int      a = Int
type instance SetIndex Integer  a = Int
type instance SetIndex Float    a = Int
type instance SetIndex Double   a = Int
type instance SetIndex Rational a = Int

instance FiniteModule Int       where dim _ = 1; unsafeToModule [x] = x
instance FiniteModule Integer   where dim _ = 1; unsafeToModule [x] = x
instance FiniteModule Float     where dim _ = 1; unsafeToModule [x] = x
instance FiniteModule Double    where dim _ = 1; unsafeToModule [x] = x
instance FiniteModule Rational  where dim _ = 1; unsafeToModule [x] = x

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

class (FreeModule v, Field (Scalar v)) => VectorSpace v where

    {-# MINIMAL (./.) | (./.=) #-}

    {-# INLINE (./) #-}
    infixl 7 ./
    (./) :: v -> Scalar v -> v
    v ./ r = v .* reciprocal r

    {-# INLINE (./.) #-}
    infixl 7 ./.
    (./.) :: v -> v -> v
    (./.) = mutable2immutable (./.=)

    {-# INLINE (./=) #-}
    infixr 5 ./=
    (./=) :: (PrimBase m) => Mutable m v -> Scalar v -> m ()
    (./=) = immutable2mutable (./)

    {-# INLINE (./.=) #-}
    infixr 5 ./.=
    (./.=) :: (PrimBase m) => Mutable m v -> v -> m ()
    (./.=) = immutable2mutable (./.)


instance VectorSpace Float     where (./) = (/); (./.) = (/)
instance VectorSpace Double    where (./) = (/); (./.) = (/)
instance VectorSpace Rational  where (./) = (/); (./.) = (/)

instance VectorSpace b => VectorSpace (a -> b) where g ./. f = \a -> g a ./. f a

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

-- | A Reisz space is a vector space obeying nice partial ordering laws.
--
-- See <http://en.wikipedia.org/wiki/Riesz_space wikipedia> for more details.
class (VectorSpace v, Lattice_ v) => Reisz v where
    --
    -- | An element of a Reisz space can always be split into positive and negative components.
    reiszSplit :: v -> (v,v)

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

-- | A Banach space is a Vector Space equipped with a compatible Norm and Metric.
--
-- See <http://en.wikipedia.org/wiki/Banach_space wikipedia> for more details.
class (VectorSpace v, Normed v, Metric v) => Banach v where
    {-# INLINE normalize #-}
    normalize :: v -> v
    normalize v = v ./ size v

-- | These laws correspond to the actual math class, but they don't
-- actually hold for 'Float' and 'Double'.
--
-- FIXME:
-- Find a way to actually test these laws and add them to
-- "SubHask.TemplateHaskell.Test".
law_Banach_distance :: Banach v => v -> v -> Logic (Scalar v)
law_Banach_distance v1 v2 = size (v1 - v2) == distance v1 v2

law_Banach_size :: Banach v => v -> Logic (Scalar v)
law_Banach_size v
    = isZero v
   || size (normalize v) == 1

instance Banach Float
instance Banach Double
instance Banach Rational

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

-- | Hilbert spaces are a natural generalization of Euclidean space that allows for infinite dimension.
--
-- See <http://en.wikipedia.org/wiki/Hilbert_space wikipedia> for more details.
--
-- FIXME:
-- The result of a dot product must always be an ordered field.
-- This is true even when the Hilbert space is over a non-ordered field like the complex numbers.
-- But the "OrdField" constraint currently prevents us from doing scalar multiplication on Complex Hilbert spaces.
-- See <http://math.stackexchange.com/questions/49348/inner-product-spaces-over-finite-fields> and <http://math.stackexchange.com/questions/47916/banach-spaces-over-fields-other-than-mathbbc> for some technical details.
class ( Banach v , TensorAlgebra v , Real (Scalar v), OrdField (Scalar v) ) => Hilbert v where
    infix 8 <>
    (<>) :: v -> v -> Scalar v

instance Hilbert Float    where (<>) = (*)
instance Hilbert Double   where (<>) = (*)

{-# INLINE squaredInnerProductNorm #-}
squaredInnerProductNorm :: Hilbert v => v -> Scalar v
squaredInnerProductNorm v = v<>v

{-# INLINE innerProductNorm #-}
innerProductNorm :: Hilbert v => v -> Scalar v
innerProductNorm = undefined -- sqrt . squaredInnerProductNorm

{-# INLINE innerProductDistance #-}
innerProductDistance :: Hilbert v => v -> v -> Scalar v
innerProductDistance _ _ = undefined --innerProductNorm $ v1-v2

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

-- | Tensor algebras generalize the outer product of vectors to construct a matrix.
--
-- See <https://en.wikipedia.org/wiki/Tensor_algebra wikipedia> for details.
--
-- FIXME:
-- This needs to be replaced by the Tensor product in the Monoidal category Vect
class
    ( VectorSpace v
    , VectorSpace (v><v)
    , Scalar (v><v) ~ Scalar v
    , Normed (v><v)     -- the size represents the determinant
    , Field (v><v)
    ) => TensorAlgebra v
        where

    -- | Take the tensor product of two vectors
    (><) :: v -> v -> (v><v)

    -- | "left multiplication" of a square matrix
    vXm :: v -> (v><v) -> v

    -- | "right multiplication" of a square matrix
    mXv :: (v><v) -> v -> v

instance TensorAlgebra Float    where  (><) = (*); vXm = (*);  mXv = (*)
instance TensorAlgebra Double   where  (><) = (*); vXm = (*);  mXv = (*)
instance TensorAlgebra Rational where  (><) = (*); vXm = (*);  mXv = (*)

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

{-
-- | Bregman divergences generalize the squared Euclidean distance and the KL-divergence.
-- They are closely related to exponential family distributions.
--
-- Mark Reid has a <http://mark.reid.name/blog/meet-the-bregman-divergences.html good tutorial>.
--
-- FIXME:
-- The definition of divergence requires taking the derivative.
-- How should this relate to categories?
class
    ( Hilbert v
    ) => Bregman v
        where

    divergence :: v -> v -> Scalar v
    divergence v1 v2 = f v1 - f v2 - (derivative f v2 <> v1 - v2)
        where
            f = bregmanFunction

    bregmanFunction :: v -> Scalar v

law_Bregman_nonnegativity :: v -> v -> Logic v
law_Bregman_nonnegativity v1 v2 = divergence v1 v2 > 0

law_Bregman_triangle ::
-}

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

-- | Metric spaces give us the most intuitive notion of distance between objects.
--
-- FIXME: There are many other notions of distance and we should make a whole hierarchy.
class
    ( HasScalar v
    , Eq_ v
    , Boolean (Logic v)
    , Logic (Scalar v) ~ Logic v
    ) => Metric v
        where

    distance :: v -> v -> Scalar v

    -- | If the distance between two datapoints is less than or equal to the upper bound,
    -- then this function will return the distance.
    -- Otherwise, it will return some number greater than the upper bound.
    {-# INLINE distanceUB #-}
    distanceUB :: v -> v -> Scalar v -> Scalar v
    distanceUB v1 v2 _ = distance v1 v2

-- | Calling this function will be faster on some 'Metric's than manually checking if distance is greater than the bound.
{-# INLINE isFartherThan #-}
isFartherThan :: Metric v => v -> v -> Scalar v -> Logic v
isFartherThan s1 s2 b = distanceUB s1 s2 b > b

-- | This function constructs an efficient default implementation for 'distanceUB' given a function that lower bounds the distance metric.
{-# INLINE lb2distanceUB #-}
lb2distanceUB ::
    ( Metric a
    , ClassicalLogic a
    ) => (a -> a -> Scalar a)
      -> (a -> a -> Scalar a -> Scalar a)
lb2distanceUB lb p q b = if lbpq > b
    then lbpq
    else distance p q
    where
        lbpq = lb p q
law_Metric_nonnegativity :: Metric v => v -> v -> Logic v
law_Metric_nonnegativity v1 v2 = distance v1 v2 >= 0

law_Metric_indiscernables :: (Eq v, Metric v) => v -> v -> Logic v
law_Metric_indiscernables v1 v2 = if v1 == v2
    then distance v1 v2 == 0
    else distance v1 v2 > 0

law_Metric_symmetry :: Metric v => v -> v -> Logic v
law_Metric_symmetry v1 v2 = distance v1 v2 == distance v2 v1

law_Metric_triangle :: Metric v => v -> v -> v -> Logic v
law_Metric_triangle m1 m2 m3
    = distance m1 m2 <= distance m1 m3 + distance m2 m3
   && distance m1 m3 <= distance m1 m2 + distance m2 m3
   && distance m2 m3 <= distance m1 m3 + distance m2 m1

instance Metric Int      where distance x1 x2 = abs $ x1 - x2
instance Metric Integer  where distance x1 x2 = abs $ x1 - x2
instance Metric Float    where distance x1 x2 = abs $ x1 - x2
instance Metric Double   where distance x1 x2 = abs $ x1 - x2
instance Metric Rational where distance x1 x2 = abs $ x1 - x2

---------

class CanError a where
    errorVal :: a
    isError :: a -> Bool

    isJust :: a -> Bool
    isJust = not isError

instance CanError (Maybe a) where
    {-# INLINE isError #-}
    isError Nothing = True
    isError _ = False

    {-# INLINE errorVal #-}
    errorVal = Nothing

instance CanError (Maybe' a) where
    {-# INLINE isError #-}
    isError Nothing' = True
    isError _ = False

    {-# INLINE errorVal #-}
    errorVal = Nothing'

instance CanError [a] where
    {-# INLINE isError #-}
    isError [] = True
    isError _  = False

    {-# INLINE errorVal #-}
    errorVal = []

instance CanError Float where
    {-# INLINE isError #-}
    {-# INLINE errorVal #-}
    isError = isNaN
    errorVal = 0/0

instance CanError Double where
    {-# INLINE isError #-}
    {-# INLINE errorVal #-}
    isError = isNaN
    errorVal = 0/0

-------------------------------------------------------------------------------
-- set-like
type family Elem s
type family SetElem s t

type ValidSetElem s = SetElem s (Elem s) ~ s

-- | Two sets are disjoint if their infimum is the empty set.
-- This function generalizes the notion of disjointness for any lower bounded lattice.
-- FIXME: add other notions of disjoint
infDisjoint :: (Constructible s, MinBound s, Monoid s) => s -> s -> Logic s
infDisjoint s1 s2 = isEmpty $ inf s1 s2

sizeDisjoint :: (Normed s, Constructible s) => s -> s -> Logic (Scalar s)
sizeDisjoint s1 s2 = size s1 + size s2 == size (s1+s2)

type Constructible0 x = (Monoid x, Constructible x)

-- | This is the class for any type that gets "constructed" from smaller types.
-- It is a massive generalization of the notion of a constructible set in topology.
--
-- See <https://en.wikipedia.org/wiki/Constructible_set_%28topology%29 wikipedia> for more details.
class Semigroup s => Constructible s where

    {-# MINIMAL singleton | cons | fromList1 #-}

    -- | creates the smallest value containing the given element
    singleton :: Elem s -> s
    singleton x = fromList1N 1 x []

    -- | inserts an element on the left
    cons :: Elem s -> s -> s
    cons x xs = singleton x + xs

    -- | inserts an element on the right;
    -- in a non-abelian 'Constructible', this may not insert the element;
    -- this occurs, for example, in the Map type.
    snoc :: s -> Elem s -> s
    snoc xs x = xs + singleton x

    -- | Construct the type from a list.
    -- Since lists may be empty (but not all 'Constructible's can be empty) we explicitly pass in an Elem s.
    fromList1 :: Elem s -> [Elem s] -> s
    fromList1 x xs = foldl' snoc (singleton x) xs

    -- | Like "fromList1" but passes in the size of the list for more efficient construction.
    fromList1N :: Int -> Elem s -> [Elem s] -> s
    fromList1N _ = fromList1

defn_Constructible_fromList :: (Eq_ s, Constructible s) => s -> Elem s -> [Elem s] -> Logic s
defn_Constructible_fromList s e es = fromList1 e es `asTypeOf` s == foldl' snoc (singleton e) es

defn_Constructible_fromListN :: (Eq_ s, Constructible s) => s -> Elem s -> [Elem s] -> Logic s
defn_Constructible_fromListN s e es = (fromList1 e es `asTypeOf` s)==fromList1N (size es+1) e es

defn_Constructible_cons :: (Eq_ s, Constructible s) => s -> Elem s -> Logic s
defn_Constructible_cons s e = cons e s == singleton e + s

defn_Constructible_snoc :: (Eq_ s, Constructible s) => s -> Elem s -> Logic s
defn_Constructible_snoc s e = snoc s e == s + singleton e

-- | A more suggestive name for inserting an element into a container that does not remember location
insert :: Constructible s => Elem s -> s -> s
insert = cons

-- | A slightly more suggestive name for a container's monoid identity
empty :: (Monoid s, Constructible s) => s
empty = zero

-- | A slightly more suggestive name for checking if a container is empty
isEmpty :: (ValidEq s, Monoid s, Constructible s) => s -> Logic s
isEmpty = isZero

-- | This function needed for the OverloadedStrings language extension
fromString :: (Monoid s, Constructible s, Elem s ~ Char) => String -> s
fromString = fromList

-- | FIXME: if -XOverloadedLists is enabled, this causes an infinite loop for some reason
{-# INLINABLE fromList #-}
fromList :: (Monoid s, Constructible s) => [Elem s] -> s
fromList [] = zero
fromList (x:xs) = fromList1 x xs

{-# INLINABLE fromListN #-}
fromListN :: (Monoid s, Constructible s) => Int -> [Elem s] -> s
fromListN 0 [] = zero
fromListN i (x:xs) = fromList1N i x xs

{-# INLINABLE generate #-}
generate :: (Monoid v, Constructible v) => Int -> (Int -> Elem v) -> v
generate n f = if n <= 0
    then zero
    else fromList1N n (f 0) (map f [1..n-1])

-- | This is a generalization of a "set".
-- We do not require a container to be a boolean algebra, just a semigroup.
class (ValidLogic s, Constructible s, ValidSetElem s) => Container s where
    elem :: Elem s -> s -> Logic s

    notElem :: Elem s -> s -> Logic s
    notElem = not elem

law_Container_preservation :: (Heyting (Logic s), Container s) => s -> s -> Elem s -> Logic s
law_Container_preservation s1 s2 e = (e `elem` s1 || e `elem` s2) ==> (e `elem` (s1+s2))

law_Constructible_singleton :: Container s => s -> Elem s -> Logic s
law_Constructible_singleton s e = elem e $ singleton e `asTypeOf` s

theorem_Constructible_cons :: Container s => s -> Elem s -> Logic s
theorem_Constructible_cons s e = elem e (cons e s)


-- | The dual of a monoid, obtained by swapping the arguments of 'mappend'.
newtype DualSG a = DualSG { getDualSG :: a }
        deriving (Read,Show)

instance Semigroup a => Semigroup (DualSG a) where
    (DualSG x)+(DualSG y) = DualSG (x+y)

instance Monoid a => Monoid (DualSG a) where
    zero = DualSG zero

-- | The monoid of endomorphisms under composition.
newtype Endo a = Endo { appEndo :: a -> a }

instance Semigroup (Endo a) where
    (Endo f)+(Endo g) = Endo (f.g)

instance Monoid (Endo a) where
    zero = Endo id

-- | Provides inverse operations for "Constructible".
--
-- FIXME:
-- should this class be broken up into smaller pieces?
class (Constructible s, Monoid s, Normed s, Scalar s~Int) => Foldable s where

    {-# MINIMAL foldMap | foldr #-}

    -- | Convert the container into a list.
    toList :: Foldable s => s -> [Elem s]
    toList s = foldr (:) [] s

    -- | Remove an element from the left of the container.
    uncons :: s -> Maybe (Elem s,s)
    uncons s = case toList s of
        []     -> Nothing
        (x:xs) -> Just (x,fromList xs)

    -- | Remove an element from the right of the container.
    unsnoc :: s -> Maybe (s,Elem s)
    unsnoc s = case unsnoc (toList s) of
        Nothing -> Nothing
        Just (xs,x) -> Just (fromList xs,x)

    -- | Add all the elements of the container together.
    {-# INLINABLE sum #-}
    sum :: Monoid (Elem s) => s -> Elem s
    sum xs = foldl' (+) zero $ toList xs

    -- the definitions below are copied from Data.Foldable
    foldMap :: Monoid a => (Elem s -> a) -> s -> a
    foldMap f = foldr ((+) . f) zero

    foldr :: (Elem s -> a -> a) -> a -> s -> a
    foldr f z t = appEndo (foldMap (Endo . f) t) z

    foldr' :: (Elem s -> a -> a) -> a -> s -> a
    foldr' f z0 xs = foldl f' id xs z0
        where f' k x z = k $! f x z

    foldl   :: (a -> Elem s -> a) -> a -> s -> a
    foldl f z t = appEndo (getDualSG (foldMap (DualSG . Endo . flip f) t)) z

    foldl'  :: (a -> Elem s -> a) -> a -> s -> a
    foldl' f z0 xs = foldr f' id xs z0
         where f' x k z = k $! f z x

    -- the following definitions are simpler (IMO) than those in Data.Foldable

    foldr1  :: (Elem s -> Elem s -> Elem s) -> s -> Elem s
    foldr1  f s = foldr1  f (toList s)

    foldr1' :: (Elem s -> Elem s -> Elem s) -> s -> Elem s
    foldr1' f s = foldr1' f (toList s)

    foldl1  :: (Elem s -> Elem s -> Elem s) -> s -> Elem s
    foldl1  f s = foldl1  f (toList s)

    foldl1' :: (Elem s -> Elem s -> Elem s) -> s -> Elem s
    foldl1' f s = foldl1' f (toList s)

defn_Foldable_foldr ::
    ( Eq_ a
    , a~Elem s
    , Logic a ~ Logic (Elem s)
    , Logic (Scalar s) ~ Logic (Elem s)
    , Boolean (Logic (Elem s))
    , Foldable s
    ) => (Elem s -> Elem s -> Elem s) -> Elem s -> s -> Logic (Elem s)
defn_Foldable_foldr f a s = foldr f a s == foldr f a (toList s)

defn_Foldable_foldr' ::
    ( Eq_ a
    , a~Elem s
    , Logic a ~ Logic (Elem s)
    , Logic (Scalar s) ~ Logic (Elem s)
    , Boolean (Logic (Elem s))
    , Foldable s
    ) => (Elem s -> Elem s -> Elem s) -> Elem s -> s -> Logic (Elem s)
defn_Foldable_foldr' f a s = foldr' f a s == foldr' f a (toList s)

defn_Foldable_foldl ::
    ( Eq_ a
    , a~Elem s
    , Logic a ~ Logic (Elem s)
    , Logic (Scalar s) ~ Logic (Elem s)
    , Boolean (Logic (Elem s))
    , Foldable s
    ) => (Elem s -> Elem s -> Elem s) -> Elem s -> s -> Logic (Elem s)
defn_Foldable_foldl f a s = foldl f a s == foldl f a (toList s)

defn_Foldable_foldl' ::
    ( Eq_ a
    , a~Elem s
    , Logic a ~ Logic (Elem s)
    , Logic (Scalar s) ~ Logic (Elem s)
    , Boolean (Logic (Elem s))
    , Foldable s
    ) => (Elem s -> Elem s -> Elem s) -> Elem s -> s -> Logic (Elem s)
defn_Foldable_foldl' f a s = foldl' f a s == foldl' f a (toList s)

defn_Foldable_foldr1 ::
    ( Eq_ (Elem s)
    , Logic (Scalar s) ~ Logic (Elem s)
    , Boolean (Logic (Elem s))
    , Foldable s
    ) => (Elem s -> Elem s -> Elem s) -> s -> Logic (Elem s)
defn_Foldable_foldr1 f s = (length s > 0) ==> (foldr1 f s == foldr1 f (toList s))

defn_Foldable_foldr1' ::
    ( Eq_ (Elem s)
    , Logic (Scalar s) ~ Logic (Elem s)
    , Boolean (Logic (Elem s))
    , Foldable s
    ) => (Elem s -> Elem s -> Elem s) -> s -> Logic (Elem s)
defn_Foldable_foldr1' f s = (length s > 0) ==> (foldr1' f s == foldr1' f (toList s))

defn_Foldable_foldl1 ::
    ( Eq_ (Elem s)
    , Logic (Scalar s) ~ Logic (Elem s)
    , Boolean (Logic (Elem s))
    , Foldable s
    ) => (Elem s -> Elem s -> Elem s) -> s -> Logic (Elem s)
defn_Foldable_foldl1 f s = (length s > 0) ==> (foldl1 f s == foldl1 f (toList s))

defn_Foldable_foldl1' ::
    ( Eq_ (Elem s)
    , Logic (Scalar s) ~ Logic (Elem s)
    , Boolean (Logic (Elem s))
    , Foldable s
    ) => (Elem s -> Elem s -> Elem s) -> s -> Logic (Elem s)
defn_Foldable_foldl1' f s = (length s > 0) ==> (foldl1' f s == foldl1' f (toList s))

-- |
--
-- Note:
-- The inverse \"theorem\" of @(toList . fromList) xs == xs@ is actually not true.
-- See the "Set" type for a counter example.
theorem_Foldable_tofrom :: (Eq_ s, Foldable s) => s -> Logic s
theorem_Foldable_tofrom s = fromList (toList s) == s

-- |
-- FIXME:
-- This law can't be automatically included in the current test system because it breaks parametricity by requiring @Monoid (Elem s)@
law_Foldable_sum ::
    ( Logic (Scalar s)~Logic s
    , Logic (Elem s)~Logic s
    , Heyting (Logic s)
    , Monoid (Elem s)
    , Eq_ (Elem s)
    , Foldable s
    ) => s -> s -> Logic s
law_Foldable_sum s1 s2 = sizeDisjoint s1 s2 ==> (sum (s1+s2) == sum s1 + sum s2)

-- | This fold is not in any of the standard libraries.
foldtree1 :: Monoid a => [a] -> a
foldtree1 as = case go as of
    []  -> zero
    [a] -> a
    as'  -> foldtree1 as'
    where
        go []  = []
        go [a] = [a]
        go (a1:a2:as'') = (a1+a2):go as''

{-# INLINE[1] convertUnfoldable #-}
convertUnfoldable :: (Monoid t, Foldable s, Constructible t, Elem s ~ Elem t) => s -> t
convertUnfoldable = fromList . toList

{-# INLINE reduce #-}
reduce :: (Monoid (Elem s), Foldable s) => s -> Elem s
reduce s = foldl' (+) zero s

-- | For anything foldable, the norm must be compatible with the folding structure.
{-# INLINE length #-}
length :: Normed s => s -> Scalar s
length = size

{-# INLINE and #-}
and :: (Foldable bs, Elem bs~b, Boolean b) => bs -> b
and = foldl' inf true

{-# INLINE or #-}
or :: (Foldable bs, Elem bs~b, Boolean b) => bs -> b
or = foldl' sup false

{-# INLINE argmin #-}
argmin :: Ord b => a -> a -> (a -> b) -> a
argmin a1 a2 f = if f a1 < f a2 then a1 else a2

{-# INLINE argmax #-}
argmax :: Ord b => a -> a -> (a -> b) -> a
argmax a1 a2 f = if f a1 > f a2 then a1 else a2

{-# INLINE maximum #-}
maximum :: (ValidLogic b, Bounded b) => [b] -> b
maximum = supremum

{-# INLINE maximum_ #-}
maximum_ :: (ValidLogic b, Ord_ b) => b -> [b] -> b
maximum_ = supremum_

{-# INLINE minimum #-}
minimum :: (ValidLogic b, Bounded b) => [b] -> b
minimum = infimum

{-# INLINE minimum_ #-}
minimum_ :: (ValidLogic b, Ord_ b) => b -> [b] -> b
minimum_ = infimum_

{-# INLINE supremum #-}
supremum :: (Foldable bs, Elem bs~b, Bounded b) => bs -> b
supremum = supremum_ minBound

{-# INLINE supremum_ #-}
supremum_ :: (Foldable bs, Elem bs~b, Lattice_ b) => b -> bs -> b
supremum_ = foldl' sup

{-# INLINE infimum #-}
infimum :: (Foldable bs, Elem bs~b, Bounded b) => bs -> b
infimum = infimum_ maxBound

{-# INLINE infimum_ #-}
infimum_ :: (Foldable bs, Elem bs~b, POrd_ b) => b -> bs -> b
infimum_ = foldl' inf

{-# INLINE concat #-}
concat :: (Monoid (Elem s), Foldable s) => s -> Elem s
concat = foldl' (+) zero

{-# INLINE headMaybe #-}
headMaybe :: Foldable s => s -> Maybe (Elem s)
headMaybe = P.fmap fst . uncons

{-# INLINE tailMaybe #-}
tailMaybe :: Foldable s => s -> Maybe s
tailMaybe = P.fmap snd . uncons

{-# INLINE lastMaybe #-}
lastMaybe :: Foldable s => s -> Maybe (Elem s)
lastMaybe = P.fmap snd . unsnoc

{-# INLINE initMaybe #-}
initMaybe :: Foldable s => s -> Maybe s
initMaybe = P.fmap fst . unsnoc

-- |
--
-- FIXME:
-- This is a correct definition of topologies, but is it useful?
-- How can this relate to continuous functions?
class (Boolean (Logic s), Boolean s, Container s) => Topology s where
    open :: s -> Logic s

    closed :: s -> Logic s
    closed s = open $ not s

    clopen :: s -> Logic s
    clopen = open && closed

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

type family Index s
type family SetIndex s a

-- | An indexed constructible container associates an 'Index' with each 'Elem'.
-- This class generalizes the map abstract data type.
--
-- There are two differences in the indexed hierarchy of containers from the standard hierarchy.
--   1. 'IxConstructible' requires a 'Monoid' constraint whereas 'Constructible' requires a 'Semigroup' constraint because there are no valid 'IxConstructible's (that I know of at least) that are not also 'Monoid's.
--   2. Many regular containers are indexed containers, but not the other way around.
--      So the class hierarchy is in a different order.
--
class (ValidLogic s, Monoid s, ValidSetElem s{-, ValidSetIndex s-}) => IxContainer s where
    lookup :: Index s -> s -> Maybe (Elem s)

    {-# INLINABLE (!) #-}
    (!) :: s -> Index s -> Elem s
    (!) s i = case lookup i s of
        Just x -> x
        Nothing -> error "used (!) on an invalid index"

    {-# INLINABLE findWithDefault #-}
    findWithDefault :: Elem s -> Index s -> s -> Elem s
    findWithDefault def i s = case s !? i of
        Nothing -> def
        Just e -> e

    {-# INLINABLE hasIndex #-}
    hasIndex :: s -> Index s -> Logic s
    hasIndex s i = case s !? i of
        Nothing -> false
        Just _ -> true

    -- | FIXME: should the functions below be moved to other classes?
    type ValidElem s e :: Constraint
    type ValidElem s e = ()

    imap :: (ValidElem s (Elem s), ValidElem s b) => (Index s -> Elem s -> b) -> s -> SetElem s b

    toIxList :: s -> [(Index s, Elem s)]

    indices :: s -> [Index s]
    indices = map fst . toIxList

    values :: s -> [Elem s]
    values = map snd . toIxList

law_IxContainer_preservation ::
    ( Logic (Elem s)~Logic s
    , ValidLogic s
    , Eq_ (Elem s)
    , IxContainer s
    ) => s -> s -> Index s -> Logic s
law_IxContainer_preservation s1 s2 i = case s1 !? i of
    Just e -> (s1+s2) !? i == Just e
    Nothing -> true

defn_IxContainer_bang ::
    ( Eq_ (Elem s)
    , ValidLogic (Elem s)
    , IxContainer s
    ) => s -> Index s -> Logic (Elem s)
defn_IxContainer_bang s i = case s !? i of
    Nothing -> true
    Just e -> s!i == e

defn_IxContainer_findWithDefault ::
    ( Eq_ (Elem s)
    , IxContainer s
    ) => s -> Index s -> Elem s -> Logic (Elem s)
defn_IxContainer_findWithDefault s i e = case s !? i of
    Nothing -> findWithDefault e i s == e
    Just e' -> findWithDefault e i s == e'

defn_IxContainer_hasIndex ::
    ( Eq_ (Elem s)
    , IxContainer s
    ) => s -> Index s -> Logic s
defn_IxContainer_hasIndex s i = case s !? i of
    Nothing -> not $ hasIndex s i
    Just _  -> hasIndex s i

-- FIXME:
-- It would be interesting to make the "Index" of scalars be ().
-- Is it worth it?
#define mkIxContainer(t) \
type instance Index t = Int; \
type instance Elem t = t; \
instance IxContainer t where \
    lookup 0 x = Just x; \
    lookup _ _ = Nothing

mkIxContainer(Int)
mkIxContainer(Integer)
mkIxContainer(Float)
mkIxContainer(Double)
mkIxContainer(Rational)

-- | Sliceable containers generalize the notion of a substring to any IxContainer.
-- Sliceables place a stronger guarantee on the way the Semigroup and IxContainer class interact to make the containers more array-like.
--
-- FIXME:
-- Slice should probably be redefined in terms of "drop" and "take" (which also need to be included into the class hierarchy properly).
class (IxContainer s, Scalar s~Index s, HasScalar s, Normed s) => Sliceable s where
    -- | Extract a subcontainer
    slice
        :: Index s -- ^ starting index
        -> Index s -- ^ number of elements
        -> s       -- ^ container
        -> s

law_Sliceable_restorable ::
    ( Sliceable s
    , Eq s
    ) => s -> Index s -> Logic s
law_Sliceable_restorable s i
    | i >= 0 && i < length s = slice 0 i s + slice i (length s-i) s == s
    | otherwise = True

law_Sliceable_preservation ::
    ( ValidLogic s
    , Logic (Elem s) ~ Logic s
    , Eq_ (Elem s)
    , Eq_ s
    , Sliceable s
    ) => s -> s -> Index s -> Logic s
law_Sliceable_preservation s1 s2 i = case s1 !? i of
    Just e -> (s1+s2) !? i == Just e
    Nothing -> case s2 !? (i - length s1) of
        Just e  -> (s1+s2) !? i == Just e
        Nothing -> true

-- | This is the class for Map-like containers.
-- Every element in these containers must contain both an index and an element.
--
-- Some containers that use indices are not typically constructed with those indices (e.g. Arrays).
-- They belong to the "Sliceable" and "Constructable" classes, but not to this class.
class IxContainer s => IxConstructible s where
    {-# MINIMAL singletonAt | consAt #-}

    -- | Construct a container with only the single (index,element) pair.
    -- This function is equivalent to 'singleton' in the 'Constructible' class.
    singletonAt :: Index s -> Elem s -> s
    singletonAt i e = consAt i e zero

    -- | Insert an element, overwriting the previous value if the index already exists.
    -- This function is equivalent to 'cons' in the 'Constructible' class.
    {-# INLINABLE consAt #-}
    consAt :: Index s -> Elem s -> s -> s
    consAt i e s = singletonAt i e + s

    -- | Insert an element only if the index does not already exist.
    -- If the index already exists, the container is unmodified.
    -- This function is equivalent to 'snoc' in the 'Constructible' class.
    {-# INLINABLE snocAt #-}
    snocAt :: s -> Index s -> Elem s -> s
    snocAt s i e = s + singletonAt i e

    -- | This function is the equivalent of 'fromList' in the 'Constructible' class.
    -- We do not require all the variants of 'fromList' because of our 'Monoid' constraint.
    {-# INLINABLE fromIxList #-}
    fromIxList :: [(Index s, Elem s)] -> s
    fromIxList xs = foldl' (\s (i,e) -> snocAt s i e) zero xs

law_IxConstructible_lookup ::
    ( ValidLogic (Elem s)
    , Eq_ (Elem s)
    , IxConstructible s
    ) => s -> Index s -> Elem s -> Logic (Elem s)
law_IxConstructible_lookup s i e = case lookup i (consAt i e s) of
    Just e' -> e'==e
    Nothing -> false

defn_IxConstructible_consAt :: (Eq_ s, IxConstructible s) => s -> Index s -> Elem s -> Logic s
defn_IxConstructible_consAt s i e = consAt i e s == singletonAt i e + s

defn_IxConstructible_snocAt :: (Eq_ s, IxConstructible s) => s -> Index s -> Elem s -> Logic s
defn_IxConstructible_snocAt s i e = snocAt s i e == s + singletonAt i e

defn_IxConstructible_fromIxList :: (Eq_ s, IxConstructible s) => s -> [(Index s, Elem s)] -> Logic s
defn_IxConstructible_fromIxList t es
    = fromIxList es `asTypeOf` t == foldl' (\s (i,e) -> snocAt s i e) zero es

-- | Follows from "law_IxConstructible_lookup" but is closely related to "law_IxContainer_preservation" and "law_Sliceable_preservation"
theorem_IxConstructible_preservation ::
    ( ValidLogic s
    , Logic (Elem s) ~ Logic s
    , Eq_ (Elem s)
    , IxContainer s
    , Scalar s ~ Int
    ) => s -> s -> Index s -> Logic s
theorem_IxConstructible_preservation s1 s2 i = case s1 !? i of
    Just e -> (s1+s2) !? i == Just e
    Nothing -> case s2 !? i of
        Just e  -> (s1+s2) !? i == Just e
        Nothing -> true

insertAt :: IxConstructible s => Index s -> Elem s -> s -> s
insertAt = consAt

-- | An infix operator equivalent to 'lookup'
-- FIXME: what should the precedence be?
{-# INLINABLE (!?) #-}
(!?) :: IxContainer s => s -> Index s -> Maybe (Elem s)
(!?) s i = lookup i s

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

type instance Scalar [a] = Int
type instance Logic [a] = Logic a
type instance Elem [a] = a
type instance SetElem [a] b = [b]
type instance Index [a] = Int

instance ValidEq a => Eq_ [a] where
    (x:xs)==(y:ys) = x==y && xs==ys
    (_:_)==[]     = false
    []    ==(_:_) = false
    []    ==[]     = true

instance Eq a => POrd_ [a] where
    inf [] _  = []
    inf _  [] = []
    inf (x:xs) (y:ys) = if x==y
        then x:inf xs ys
        else []

instance Eq a => MinBound_ [a] where
    minBound = []

instance Normed [a] where
    size = P.length

instance Semigroup [a] where
    (+) = (P.++)

instance Monoid [a] where
    zero = []

instance ValidEq a => Container [a] where
    elem _ []       = false
    elem x (y:ys)   = x==y || elem x ys

    notElem = not elem

instance Constructible [a] where
    singleton a = [a]
    cons x xs = x:xs
    fromList1 x xs = x:xs
    fromList1N _ x xs = x:xs

instance Foldable [a] where
    toList = id

    uncons [] = Nothing
    uncons (x:xs) = Just (x,xs)

    unsnoc [] = Nothing
    unsnoc xs = Just (P.init xs,P.last xs)

    foldMap f s = concat $ map f s

    foldr = L.foldr
    foldr' = L.foldr
    foldr1 = L.foldr1
    foldr1' = L.foldr1

    foldl = L.foldl
    foldl' = L.foldl'
    foldl1 = L.foldl1
    foldl1' = L.foldl1'

instance ValidLogic a => IxContainer [a] where
    lookup 0 (x:_) = Just x
    lookup i (_:xs) = lookup (i-1) xs
    lookup _ [] = Nothing

    imap f xs = map (uncurry f) $ P.zip [0..] xs

    toIxList xs = P.zip [0..] xs

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

type instance Scalar (Maybe a) = Scalar a
type instance Logic (Maybe a) = Logic a

instance ValidEq a => Eq_ (Maybe a) where
    Nothing   == Nothing   = true
    Nothing   == _         = false
    _         == Nothing   = false
    (Just a1) == (Just a2) = a1==a2

instance Semigroup a => Semigroup (Maybe a) where
    (Just a1) + (Just a2) = Just $ a1+a2
    Nothing   + a2        = a2
    a1        + Nothing   = a1

instance Semigroup a => Monoid (Maybe a) where
    zero = Nothing

----------

data Maybe' a = Nothing' | Just' { fromJust' :: !a }

justs' :: [Maybe' a] -> [a]
justs' [] = []
justs' (Nothing':xs) = justs' xs
justs' (Just' x:xs) = x:justs' xs

type instance Scalar (Maybe' a) = Scalar a
type instance Logic (Maybe' a) = Logic a

instance NFData a => NFData (Maybe' a) where
    rnf Nothing' = ()
    rnf (Just' a) = rnf a

instance ValidEq a => Eq_ (Maybe' a) where
    (Just' a1) == (Just' a2) = a1==a2
    Nothing'   == Nothing'   = true
    _          == _          = false

instance Semigroup a => Semigroup (Maybe' a) where
    (Just' a1) + (Just' a2) = Just' $ a1+a2
    Nothing'   + a2         = a2
    a1         + Nothing'   = a1

instance Semigroup a => Monoid (Maybe' a) where
    zero = Nothing'

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

type instance Logic (a,b) = Logic a
type instance Logic (a,b,c) = Logic a

instance (ValidEq a, ValidEq b, Logic a ~ Logic b) => Eq_ (a,b) where
    (a1,b1)==(a2,b2) = a1==a2 && b1==b2

instance (ValidEq a, ValidEq b, ValidEq c, Logic a ~ Logic b, Logic b~Logic c) => Eq_ (a,b,c) where
    (a1,b1,c1)==(a2,b2,c2) = a1==a2 && b1==b2 && c1==c2

instance (Semigroup a, Semigroup b) => Semigroup (a,b) where
    (a1,b1)+(a2,b2) = (a1+a2,b1+b2)

instance (Semigroup a, Semigroup b, Semigroup c) => Semigroup (a,b,c) where
    (a1,b1,c1)+(a2,b2,c2) = (a1+a2,b1+b2,c1+c2)

instance (Monoid a, Monoid b) => Monoid (a,b) where
    zero = (zero,zero)

instance (Monoid a, Monoid b, Monoid c) => Monoid (a,b,c) where
    zero = (zero,zero,zero)

instance (Cancellative a, Cancellative b) => Cancellative (a,b) where
    (a1,b1)-(a2,b2) = (a1-a2,b1-b2)

instance (Cancellative a, Cancellative b, Cancellative c) => Cancellative (a,b,c) where
    (a1,b1,c1)-(a2,b2,c2) = (a1-a2,b1-b2,c1-c2)

instance (Group a, Group b) => Group (a,b) where
    negate (a,b) = (negate a,negate b)

instance (Group a, Group b, Group c) => Group (a,b,c) where
    negate (a,b,c) = (negate a,negate b,negate c)

instance (Abelian a, Abelian b) => Abelian (a,b)

instance (Abelian a, Abelian b, Abelian c) => Abelian (a,b,c)

data Labeled' x y = Labeled' { xLabeled' :: !x, yLabeled' :: !y }
    deriving (Read,Show,Typeable)

instance (NFData x, NFData y) => NFData (Labeled' x y) where
    rnf (Labeled' x y) = deepseq x $ rnf y

instance (Arbitrary x, Arbitrary y) => Arbitrary (Labeled' x y) where
    arbitrary = do
        x <- arbitrary
        y <- arbitrary
        return $ Labeled' x y

instance (CoArbitrary x, CoArbitrary y) => CoArbitrary (Labeled' x y) where
    coarbitrary (Labeled' x  y) = coarbitrary (x,y)

type instance Scalar (Labeled' x y) = Scalar x
type instance Actor (Labeled' x y) = x
type instance Logic (Labeled' x y) = Logic x
type instance Elem (Labeled' x y) = Elem x

-----

instance Eq_ x => Eq_ (Labeled' x y) where
    (Labeled' x1 _) == (Labeled' x2 _) = x1==x2

instance (ClassicalLogic x, Ord_ x) => POrd_ (Labeled' x y) where
    inf (Labeled' x1 y1) (Labeled' x2 y2) = if x1 < x2
        then Labeled' x1 y1
        else Labeled' x2 y2
    (Labeled' x1 _)< (Labeled' x2 _) = x1< x2
    (Labeled' x1 _)<=(Labeled' x2 _) = x1<=x2

instance (ClassicalLogic x, Ord_ x) => Lattice_ (Labeled' x y) where
    sup (Labeled' x1 y1) (Labeled' x2 y2) = if x1 >= x2
        then Labeled' x1 y1
        else Labeled' x2 y2
    (Labeled' x1 _)> (Labeled' x2 _) = x1> x2
    (Labeled' x1 _)>=(Labeled' x2 _) = x1>=x2

instance (ClassicalLogic x, Ord_ x) => Ord_ (Labeled' x y) where

instance Semigroup x => Action (Labeled' x y) where
    (Labeled' x y) .+ x' = Labeled' (x'+x) y

instance Metric x => Metric (Labeled' x y) where
    distance (Labeled' x1 _) (Labeled' x2 _) = distance x1 x2
    distanceUB (Labeled' x1 _) (Labeled' x2 _) = distanceUB x1 x2

instance Normed x => Normed (Labeled' x y) where
    size (Labeled' x _) = size x


--------------------------------------------------------------------------------
-- spatial programming
--
-- FIXME:
-- This is broken, partly due to type system limits.
-- It's being exported just for basic testing.

-- | The type of all containers satisfying the @cxt@ constraint with elements of type @x@.
type All cxt x = forall xs. (cxt xs, Elem xs~x) => xs

data Any cxt x where
    Any :: forall cxt x xs. (cxt xs, Elem xs~x) => xs -> Any cxt x
--     Any :: All cxt x -> Any cxt x

instance Show x => Show (Any Foldable x) where
    show (Any xs) = show $ toList xs

type instance Elem (Any cxt x) = x
type instance Scalar (Any cxt x) = Int

instance Semigroup (Any Foldable x) where
    (Any x1)+(Any x2)=Any (x1+(fromList.toList)x2)

instance Constructible (Any Foldable x) where

instance Normed (Any Foldable x) where
    size (Any xs) = size xs

instance Monoid (Any Foldable x) where
    zero = Any []

instance Foldable (Any Foldable x) where
    toList (Any xs) = toList xs

mkMutable [t| forall cxt x. Any cxt x |]

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

mkMutable [t| POrdering |]
mkMutable [t| Ordering |]
mkMutable [t| forall a. Endo a |]
mkMutable [t| forall a. DualSG a |]
mkMutable [t| forall a. Maybe a |]
mkMutable [t| forall a. Maybe' a |]
mkMutable [t| forall a b. Labeled' a b |]