module SubHask.Algebra
(
Logic
, ValidLogic
, ClassicalLogic
, Eq_ (..)
, Eq
, ValidEq
, law_Eq_reflexive
, law_Eq_symmetric
, law_Eq_transitive
, 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
, Graded (..)
, law_Graded_pred
, law_Graded_fromEnum
, Ord_ (..)
, law_Ord_totality
, law_Ord_min
, law_Ord_max
, Ord
, Ordering (..)
, min
, max
, maximum
, maximum_
, minimum
, minimum_
, argmin
, argmax
, Enum (..)
, law_Enum_succ
, law_Enum_toEnum
, (||)
, (&&)
, true
, false
, and
, or
, Elem
, 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
, length
, reduce
, concat
, headMaybe
, tailMaybe
, lastMaybe
, initMaybe
, Index
, SetIndex
, IxContainer (..)
, law_IxContainer_preservation
, defn_IxContainer_bang
, defn_IxContainer_findWithDefault
, defn_IxContainer_hasIndex
, (!?)
, Sliceable (..)
, IxConstructible (..)
, law_IxConstructible_lookup
, defn_IxConstructible_consAt
, defn_IxConstructible_snocAt
, defn_IxConstructible_fromIxList
, insertAt
, CanError (..)
, Maybe' (..)
, justs'
, Labeled' (..)
, Semigroup (..)
, law_Semigroup_associativity
, defn_Semigroup_plusequal
, 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
, 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
, fromIntegral
, Field(..)
, OrdField(..)
, RationalField(..)
, convertRationalField
, toFloat
, toDouble
, BoundedField(..)
, infinity
, negInfinity
, ExpRing (..)
, (^)
, ExpField (..)
, Real (..)
, QuotientField(..)
, Normed (..)
, abs
, Metric (..)
, isFartherThan
, lb2distanceUB
, law_Metric_nonnegativity
, law_Metric_indiscernables
, law_Metric_symmetry
, law_Metric_triangle
, 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 (..)
, Banach (..)
, Hilbert (..)
, innerProductDistance
, innerProductNorm
, TensorAlgebra (..)
, Any (..)
, All
, 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 Prelude (Ordering (..))
import Control.Monad hiding (liftM)
import Control.Monad.ST
import Data.Ratio
import Data.Typeable
import Test.QuickCheck (Arbitrary (..), frequency)
import Control.Concurrent
import Control.Parallel
import Control.Parallel.Strategies
import System.IO.Unsafe
import GHC.Prim hiding (Any)
import GHC.Types
import GHC.Magic
import SubHask.Internal.Prelude
import SubHask.Category
import SubHask.Mutable
import SubHask.SubType
simpleMutableDefn :: (Eq_ a, IsMutable a)
=> (Mutable (ST s) a -> b -> ST s ())
-> (a -> b -> a)
-> (a -> b -> Logic a)
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
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 () = ()
type ValidLogic a = Complemented (Logic a)
type ClassicalLogic a = Logic a ~ Bool
class Eq_ a where
infix 4 ==
(==) :: a -> a -> Logic a
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
() == () = ()
() /= () = ()
instance Eq_ Bool where (==) = (P.==); (/=) = (P./=); ;
instance Eq_ Char where (==) = (P.==); (/=) = (P./=); ;
instance Eq_ Int where (==) = (P.==); (/=) = (P./=); ;
instance Eq_ Integer where (==) = (P.==); (/=) = (P./=); ;
instance Eq_ Rational where (==) = (P.==); (/=) = (P./=); ;
instance Eq_ Float where (==) = (P.==); (/=) = (P./=); ;
instance Eq_ Double where (==) = (P.==); (/=) = (P./=); ;
instance Eq_ b => Eq_ (a -> b) where
(f==g) a = f a == g a
type Eq a = (Eq_ a, Logic a~Bool)
type ValidEq a = (Eq_ a, ValidLogic a)
class Eq_ b => POrd_ b where
inf :: b -> b -> b
infix 4 <=
(<=) :: b -> b -> Logic b
b1 <= b2 = inf b1 b2 == b1
infix 4 <
(<) :: Complemented (Logic b) => b -> b -> Logic b
b1 < b2 = inf b1 b2 == b1 && b1 /= b2
type POrd a = (Eq a, POrd_ a)
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.<) ;\
;\
;\
mkPOrd_(Bool)
mkPOrd_(Char)
mkPOrd_(Int)
mkPOrd_(Integer)
mkPOrd_(Float)
mkPOrd_(Double)
mkPOrd_(Rational)
instance POrd_ () where
inf () () = ()
instance POrd_ b => POrd_ (a -> b) where
inf f g = \x -> inf (f x) (g x)
(f<=g) a = f a <= g a
class POrd_ b => MinBound_ b where
minBound :: b
type MinBound a = (Eq a, MinBound_ a)
law_MinBound_inf :: (Eq b, MinBound_ b) => b -> Bool
law_MinBound_inf b = inf b minBound == minBound
false :: MinBound_ b => b
false = minBound
instance MinBound_ () where minBound = () ;
instance MinBound_ Bool where minBound = False ;
instance MinBound_ Char where minBound = P.minBound ;
instance MinBound_ Int where minBound = P.minBound ;
instance MinBound_ Float where minBound = 1/0 ;
instance MinBound_ Double where minBound = 1/0 ;
instance MinBound_ b => MinBound_ (a -> b) where minBound = \x -> minBound ;
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
PLT == PLT = True
PGT == PGT = True
PEQ == PEQ = True
PNA == PNA = True
_ == _ = False
instance Semigroup POrdering where
PEQ + x = x
PLT + _ = PLT
PGT + _ = PGT
PNA + _ = PNA
type instance Logic Ordering = Bool
instance Eq_ Ordering where
EQ == EQ = True
LT == LT = True
GT == GT = True
_ == _ = False
instance Semigroup Ordering where
EQ + x = x
LT + _ = LT
GT + _ = GT
instance Monoid POrdering where
zero = PEQ
instance Monoid Ordering where
zero = EQ
class POrd_ b => Lattice_ b where
sup :: b -> b -> b
infix 4 >=
(>=) :: b -> b -> Logic b
b1 >= b2 = sup b1 b2 == b1
infix 4 >
(>) :: Boolean (Logic b) => b -> b -> Logic b
b1 > b2 = sup b1 b2 == b1 && b1 /= b2
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)
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.>) ;\
;\
;\
mkLattice_(Bool)
mkLattice_(Char)
mkLattice_(Int)
mkLattice_(Integer)
mkLattice_(Float)
mkLattice_(Double)
mkLattice_(Rational)
instance Lattice_ () where
sup () () = ()
instance Lattice_ b => Lattice_ (a -> b) where
sup f g = \x -> sup (f x) (g x)
(f>=g) a = f a >= g a
infixr 3 &&
(&&) :: Lattice_ b => b -> b -> b
(&&) = inf
infixr 2 ||
(||) :: Lattice_ b => b -> b -> b
(||) = sup
isChain :: Lattice a => [a] -> Logic a
isChain [] = true
isChain (x:xs) = all (/=PNA) (map (pcompare x) xs) && isChain xs
isAntichain :: Lattice a => [a] -> Logic a
isAntichain [] = true
isAntichain (x:xs) = all (==PNA) (map (pcompare x) xs) && isAntichain xs
class (Graded b, Ord_ b) => Enum b where
succ :: b -> b
toEnum :: Int -> b
law_Enum_succ :: Enum b => b -> b -> Bool
law_Enum_succ b1 b2 = fromEnum (succ b1) == fromEnum b1+1
|| fromEnum (succ b1) == fromEnum b1
law_Enum_toEnum :: (Lattice b, Enum b) => b -> Bool
law_Enum_toEnum b = toEnum (fromEnum b) == b
instance Enum Bool where
succ True = True
succ False = True
toEnum 1 = True
toEnum 0 = False
instance Enum Int where
succ i = if i == maxBound
then i
else i+1
toEnum = id
instance Enum Char where
succ = P.succ
toEnum i = if i < 0
then P.toEnum 0
else P.toEnum i
instance Enum Integer where
succ = P.succ
toEnum = P.toEnum
class Lattice b => Graded b where
pred :: b -> b
fromEnum :: b -> Int
law_Graded_pred :: Graded b => b -> b -> Bool
law_Graded_pred b1 b2 = fromEnum (pred b1) == fromEnum b11
|| fromEnum (pred b1) == fromEnum b1
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
instance Graded Bool where
pred True = False
pred False = False
fromEnum True = 1
fromEnum False = 0
instance Graded Int where
pred i = if i == minBound
then i
else i1
fromEnum = id
instance Graded Char where
pred c = if c=='\NUL'
then '\NUL'
else P.pred c
fromEnum = P.fromEnum
instance Graded Integer where
pred = P.pred
fromEnum = P.fromEnum
(<.) :: (Lattice b, Graded b) => b -> b -> Bool
b1 <. b2 = b1 == pred b2
(>.) :: (Lattice b, Enum b) => b -> b -> Bool
b1 >. b2 = b1 == succ b2
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
min :: Ord_ a => a -> a -> a
min = inf
max :: Ord_ a => a -> a -> a
max = sup
type Ord a = (Eq a, Ord_ a)
instance Ord_ ()
instance Ord_ Char where compare = P.compare ;
instance Ord_ Int where compare = P.compare ;
instance Ord_ Integer where compare = P.compare ;
instance Ord_ Float where compare = P.compare ;
instance Ord_ Double where compare = P.compare ;
instance Ord_ Rational where compare = P.compare ;
instance Ord_ Bool where compare = P.compare ;
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 :: Bounded b => b
true = maxBound
instance Bounded () where maxBound = () ;
instance Bounded Bool where maxBound = True ;
instance Bounded Char where maxBound = P.maxBound ;
instance Bounded Int where maxBound = P.maxBound ;
instance Bounded Float where maxBound = 1/0 ;
instance Bounded Double where maxBound = 1/0 ;
instance Bounded b => Bounded (a -> b) where
maxBound = \x -> 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
not () = ()
instance Complemented Bool where
not = P.not
instance Complemented b => Complemented (a -> b) where
not f = \x -> not $ f x
class Bounded b => Heyting b where
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))
modusPonens :: Boolean b => b -> b -> b
modusPonens b1 b2 = not b1 || b2
instance Heyting () where
() ==> () = ()
instance Heyting Bool where
(==>) = modusPonens
instance Heyting b => Heyting (a -> b) where
(f==>g) a = f a ==> g a
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)
class IsMutable g => Semigroup g where
infixl 6 +
(+) :: g -> g -> g
(+) = mutable2immutable (+=)
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 (+=) (+)
associator :: (Semigroup g, Metric g) => g -> g -> g -> Scalar g
associator g1 g2 g3 = distance ((g1+g2)+g3) (g1+(g2+g3))
cycle :: Semigroup m => m -> m
cycle xs = xs' where xs' = xs + xs'
instance Semigroup Int where (+) = (P.+) ;
instance Semigroup Integer where (+) = (P.+) ;
instance Semigroup Float where (+) = (P.+) ;
instance Semigroup Double where (+) = (P.+) ;
instance Semigroup Rational where (+) = (P.+) ;
instance Semigroup () where
()+() = ()
instance Semigroup b => Semigroup (a -> b) where
f+g = \a -> f a + g a
type family Actor s
class (IsMutable s, Semigroup (Actor s)) => Action s where
infixl 6 .+
(.+) :: s -> Actor s -> s
(.+) = mutable2immutable (.+=)
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 (.+=) (.+)
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 (.+) = (+) ;
instance Action Integer where (.+) = (+) ;
instance Action Float where (.+) = (+) ;
instance Action Double where (.+) = (+) ;
instance Action Rational where (.+) = (+) ;
instance Action () where (.+) = (+) ;
instance Action b => Action (a->b) where
f.+g = \x -> f x.+g x
class Semigroup g => Monoid g where
zero :: g
isZero :: (Monoid g, ValidEq g) => g -> Logic g
isZero = (==zero)
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 ;
instance Monoid Integer where zero = 0 ;
instance Monoid Float where zero = 0 ;
instance Monoid Double where zero = 0 ;
instance Monoid Rational where zero = 0 ;
instance Monoid () where
zero = ()
instance Monoid b => Monoid (a -> b) where
zero = \a -> zero
class Semigroup g => Cancellative g where
infixl 6
() :: g -> g -> g
() = mutable2immutable (-=)
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.-) ;
instance Cancellative Integer where () = (P.-) ;
instance Cancellative Float where () = (P.-) ;
instance Cancellative Double where () = (P.-) ;
instance Cancellative Rational where () = (P.-) ;
instance Cancellative () where
()() = ()
instance Cancellative b => Cancellative (a -> b) where
fg = \a -> f a g a
class (Cancellative g, Monoid g) => Group g where
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 ;
instance Group Integer where negate = P.negate ;
instance Group Float where negate = P.negate ;
instance Group Double where negate = P.negate ;
instance Group Rational where negate = P.negate ;
instance Group () where
negate () = ()
instance Group b => Group (a -> b) where
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)
class (Abelian r, Monoid r) => Rg r where
infixl 7 *
(*) :: r -> r -> r
(*) = mutable2immutable (*=)
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.*) ;
instance Rg Integer where (*) = (P.*) ;
instance Rg Float where (*) = (P.*) ;
instance Rg Double where (*) = (P.*) ;
instance Rg Rational where (*) = (P.*) ;
instance Rg b => Rg (a -> b) where
f*g = \a -> f a * g a
class (Monoid r, Rg r) => Rig r where
one :: r
isOne :: (Rig g, ValidEq g) => g -> Logic g
isOne = (==one)
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 ;
instance Rig Integer where one = 1 ;
instance Rig Float where one = 1 ;
instance Rig Double where one = 1 ;
instance Rig Rational where one = 1 ;
instance Rig b => Rig (a -> b) where
one = \a -> one
type Rng r = (Rg r, Group r)
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
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 ;
instance Ring Integer where fromInteger = P.fromInteger ;
instance Ring Float where fromInteger = P.fromInteger ;
instance Ring Double where fromInteger = P.fromInteger ;
instance Ring Rational where fromInteger = P.fromInteger ;
instance Ring b => Ring (a -> b) where
fromInteger i = \a -> fromInteger i
indicator :: Ring r => Bool -> r
indicator True = 1
indicator False = 0
class Ring a => Integral a where
toInteger :: a -> Integer
infixl 7 `quot`, `rem`
quot :: a -> a -> a
quot a1 a2 = fst (quotRem a1 a2)
rem :: a -> a -> a
rem a1 a2 = snd (quotRem a1 a2)
quotRem :: a -> a -> (a,a)
infixl 7 `div`, `mod`
div :: a -> a -> a
div a1 a2 = fst (divMod a1 a2)
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
fromIntegral :: (Integral a, Ring b) => a -> b
fromIntegral = fromInteger . toInteger
roundUpToNearest :: Int -> Int -> Int
roundUpToNearest m x = x + m 1 (x1)`rem`m
instance Integral Int where
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
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
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)
toInteger = error "toInteger shouldn't be in the integral class b/c of bad function instance"
class Ring r => Field r where
reciprocal :: r -> r
reciprocal r = one/r
infixl 7 /
(/) :: r -> r -> r
n/d = n * reciprocal d
fromRational :: Rational -> r
fromRational r = fromInteger (numerator r) / fromInteger (denominator r)
#define mkField(x) \
instance Field x where \
(/) = (P./) ;\
fromRational=P.fromRational ;\
;\
mkField(Float)
mkField(Double)
mkField(Rational)
instance Field b => Field (a -> b) where
reciprocal f = reciprocal . f
class (Field r, Ord r, Normed r, IsScalar r) => OrdField r
instance OrdField Float
instance OrdField Double
instance OrdField Rational
class (OrdField r, Bounded r) => BoundedField r where
nan :: r
nan = 0/0
isNaN :: r -> Bool
infinity :: BoundedField r => r
infinity = maxBound
negInfinity :: BoundedField r => r
negInfinity = minBound
instance BoundedField Float where isNaN = P.isNaN ;
instance BoundedField Double where isNaN = P.isNaN ;
class Field r => RationalField r where
toRational :: r -> Rational
instance RationalField Float where toRational=P.toRational ;
instance RationalField Double where toRational=P.toRational ;
instance RationalField Rational where toRational=P.toRational ;
convertRationalField :: (RationalField a, RationalField b) => a -> b
convertRationalField = fromRational . toRational
toFloat :: RationalField a => a -> Float
toFloat = convertRationalField
toDouble :: RationalField a => a -> Double
toDouble = convertRationalField
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.^^); \
;\
;\
;\
;\
;\
mkQuotientField(Float,Int)
mkQuotientField(Float,Integer)
mkQuotientField(Double,Int)
mkQuotientField(Double,Integer)
mkQuotientField(Rational,Int)
mkQuotientField(Rational,Integer)
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)
class Ring r => ExpRing r where
(**) :: r -> r -> r
infixl 8 **
logBase :: r -> r -> r
(^) :: ExpRing r => r -> r -> r
(^) = (**)
instance ExpRing Float where
(**) = (P.**)
logBase = P.logBase
instance ExpRing Double where
(**) = (P.**)
logBase = P.logBase
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
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) >< c = a -> (b><c)
type IsScalar r = (Ring r, Ord_ r, Scalar r~r, Normed r, ClassicalLogic r, r~(r><r))
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
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
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)
) => Module v
where
infixl 7 .*
(.*) :: v -> Scalar v -> v
(.*) = mutable2immutable (.*=)
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 (.*=) (.*)
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
class Module v => FreeModule v where
infixl 7 .*.
(.*.) :: v -> v -> v
(.*.) = mutable2immutable (.*.=)
infixr 5 .*.=
(.*.=) :: (PrimBase m) => Mutable m v -> v -> m ()
(.*.=) = immutable2mutable (.*.)
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 = \a -> ones
class
( FreeModule v
, IxContainer v
, Elem v~Scalar v
, Index v~Int
, v ~ SetElem v (Elem v)
) => FiniteModule v
where
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
infixl 7 ./
(./) :: v -> Scalar v -> v
v ./ r = v .* reciprocal r
infixl 7 ./.
(./.) :: v -> v -> v
(./.) = mutable2immutable (./.=)
infixr 5 ./=
(./=) :: (PrimBase m) => Mutable m v -> Scalar v -> m ()
(./=) = immutable2mutable (./)
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
class (VectorSpace v, Lattice_ v) => Reisz v where
reiszSplit :: v -> (v,v)
class (VectorSpace v, Normed v, Metric v) => Banach v where
normalize :: v -> v
normalize v = v ./ size v
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
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 (<>) = (*)
squaredInnerProductNorm :: Hilbert v => v -> Scalar v
squaredInnerProductNorm v = v<>v
innerProductNorm :: Hilbert v => v -> Scalar v
innerProductNorm = undefined
innerProductDistance :: Hilbert v => v -> v -> Scalar v
innerProductDistance v1 v2 = undefined
class
( VectorSpace v
, VectorSpace (v><v)
, Scalar (v><v) ~ Scalar v
, Normed (v><v)
, Field (v><v)
) => TensorAlgebra v
where
(><) :: v -> v -> (v><v)
vXm :: v -> (v><v) -> v
mXv :: (v><v) -> v -> v
instance TensorAlgebra Float where (><) = (*); vXm = (*); mXv = (*)
instance TensorAlgebra Double where (><) = (*); vXm = (*); mXv = (*)
instance TensorAlgebra Rational where (><) = (*); vXm = (*); mXv = (*)
class
( HasScalar v
, Eq_ v
, Boolean (Logic v)
, Logic (Scalar v) ~ Logic v
) => Metric v
where
distance :: v -> v -> Scalar v
distanceUB :: v -> v -> Scalar v -> Scalar v
distanceUB v1 v2 _ = distance v1 v2
isFartherThan :: Metric v => v -> v -> Scalar v -> Logic v
isFartherThan s1 s2 b = distanceUB s1 s2 b > b
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
isError Nothing = True
isError _ = False
errorVal = Nothing
instance CanError (Maybe' a) where
isError Nothing' = True
isError _ = False
errorVal = Nothing'
instance CanError [a] where
isError [] = True
isError _ = False
errorVal = []
instance CanError Float where
isError = isNaN
errorVal = 0/0
instance CanError Double where
isError = isNaN
errorVal = 0/0
type Item s = Elem s
type family Elem s
type family SetElem s t
type ValidSetElem s = SetElem s (Elem s) ~ s
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)
class Semigroup s => Constructible s where
singleton :: Elem s -> s
singleton x = fromList1N 1 x []
cons :: Elem s -> s -> s
cons x xs = singleton x + xs
snoc :: s -> Elem s -> s
snoc xs x = xs + singleton x
fromList1 :: Elem s -> [Elem s] -> s
fromList1 x xs = foldl' snoc (singleton x) xs
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
insert :: Constructible s => Elem s -> s -> s
insert = cons
empty :: (Monoid s, Constructible s) => s
empty = zero
isEmpty :: (ValidEq s, Monoid s, Constructible s) => s -> Logic s
isEmpty = isZero
fromString :: (Monoid s, Constructible s, Elem s ~ Char) => String -> s
fromString = fromList
fromList :: (Monoid s, Constructible s) => [Elem s] -> s
fromList [] = zero
fromList (x:xs) = fromList1 x xs
fromListN :: (Monoid s, Constructible s) => Int -> [Elem s] -> s
fromListN 0 [] = zero
fromListN i (x:xs) = fromList1N i x xs
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..n1])
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)
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
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
class (Constructible s, Monoid s, Normed s, Scalar s~Int) => Foldable s where
toList :: Foldable s => s -> [Elem s]
toList s = foldr (:) [] s
uncons :: s -> Maybe (Elem s,s)
uncons s = case toList s of
[] -> Nothing
(x:xs) -> Just (x,fromList xs)
unsnoc :: s -> Maybe (s,Elem s)
unsnoc s = case unsnoc (toList s) of
Nothing -> Nothing
Just (xs,x) -> Just (fromList xs,x)
sum :: Monoid (Elem s) => s -> Elem s
sum xs = foldl' (+) zero $ toList xs
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
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))
theorem_Foldable_tofrom :: (Eq_ s, Foldable s) => s -> Logic s
theorem_Foldable_tofrom s = fromList (toList s) == 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)
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
convertUnfoldable :: (Monoid t, Foldable s, Constructible t, Elem s ~ Elem t) => s -> t
convertUnfoldable = fromList . toList
reduce :: (Monoid (Elem s), Foldable s) => s -> Elem s
reduce s = foldl' (+) zero s
length :: Normed s => s -> Scalar s
length = size
and :: (Foldable bs, Elem bs~b, Boolean b) => bs -> b
and = foldl' inf true
or :: (Foldable bs, Elem bs~b, Boolean b) => bs -> b
or = foldl' sup false
argmin :: Ord b => a -> a -> (a -> b) -> a
argmin a1 a2 f = if f a1 < f a2 then a1 else a2
argmax :: Ord b => a -> a -> (a -> b) -> a
argmax a1 a2 f = if f a1 > f a2 then a1 else a2
maximum :: (ValidLogic b, Bounded b) => [b] -> b
maximum = supremum
maximum_ :: (ValidLogic b, Ord_ b) => b -> [b] -> b
maximum_ = supremum_
minimum :: (ValidLogic b, Bounded b) => [b] -> b
minimum = infimum
minimum_ :: (ValidLogic b, Ord_ b) => b -> [b] -> b
minimum_ = infimum_
supremum :: (Foldable bs, Elem bs~b, Bounded b) => bs -> b
supremum = supremum_ minBound
supremum_ :: (Foldable bs, Elem bs~b, Lattice_ b) => b -> bs -> b
supremum_ = foldl' sup
infimum :: (Foldable bs, Elem bs~b, Bounded b) => bs -> b
infimum = infimum_ maxBound
infimum_ :: (Foldable bs, Elem bs~b, POrd_ b) => b -> bs -> b
infimum_ = foldl' inf
concat :: (Monoid (Elem s), Foldable s) => s -> Elem s
concat = foldl' (+) zero
headMaybe :: Foldable s => s -> Maybe (Elem s)
headMaybe = P.fmap fst . uncons
tailMaybe :: Foldable s => s -> Maybe s
tailMaybe = P.fmap snd . uncons
lastMaybe :: Foldable s => s -> Maybe (Elem s)
lastMaybe = P.fmap snd . unsnoc
initMaybe :: Foldable s => s -> Maybe s
initMaybe = P.fmap fst . unsnoc
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
type ValidSetIndex s = SetIndex s (Index s) ~ s
class (ValidLogic s, Monoid s, ValidSetElem s) => IxContainer s where
lookup :: Index s -> s -> Maybe (Elem s)
(!) :: s -> Index s -> Elem s
(!) s i = case lookup i s of
Just x -> x
Nothing -> error "used (!) on an invalid index"
findWithDefault :: Elem s -> Index s -> s -> Elem s
findWithDefault def i s = case s !? i of
Nothing -> def
Just e -> e
hasIndex :: s -> Index s -> Logic s
hasIndex s i = case s !? i of
Nothing -> false
Just _ -> true
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
Nothing -> case s2 !? i of
Nothing -> true
Just e -> (s1+s2) !? i == Just e
Just e -> (s1+s2) !? i == Just e
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
#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)
class (IxContainer s, Enum (Index s)) => Sliceable s where
slice :: Index s -> Int -> s -> s
class IxContainer s => IxConstructible s where
singletonAt :: Index s -> Elem s -> s
singletonAt i e = consAt i e zero
consAt :: Index s -> Elem s -> s -> s
consAt i e s = singletonAt i e + s
snocAt :: s -> Index s -> Elem s -> s
snocAt s i e = s + singletonAt i e
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
insertAt :: IxConstructible s => Index s -> Elem s -> s -> s
insertAt = consAt
(!?) :: 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
(x:xs)==[] = false
[] ==(y:ts) = 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:xs) = Just x
lookup i (x:xs) = lookup (i1) 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) = (a1a2,b1b2)
instance (Cancellative a, Cancellative b, Cancellative c) => Cancellative (a,b,c) where
(a1,b1,c1)(a2,b2,c2) = (a1a2,b1b2,c1c2)
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 y1) == (Labeled' x2 y2) = 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 y1) (Labeled' x2 y2) = distance x1 x2
distanceUB (Labeled' x1 y1) (Labeled' x2 y2) = distanceUB x1 x2
instance Normed x => Normed (Labeled' x y) where
size (Labeled' x _) = size 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
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 |]