Coming to a Haskell and a Scalaz near you!

Lift.hs

----
-- Lift (reusable instance)
----

-- | Lift an instance through an applicative functor.
-- |
-- | Applicative functors preserve identities and associativity, though
-- | perhaps not commutativity. The most well-known example is perhaps
-- | that functions into a monoid themselves form a monoid.
-- |
-- | Under the lifting, 'pure' becomes a lawful homomorphism.
newtype Lift f a = Lift { getLift :: f a }

instance (Applicative f, PreSemigroup a) => PreSemigroup (Lift f a) where
    (<>) = coerce $ liftA2 @f @a (<>)

instance (Applicative f, Semigroup a) => Semigroup (Lift f a)

instance (Applicative f, PreMonoid a) => PreMonoid (Lift f a) where
    identity = coerce $ pure @f @a identity

instance (Applicative f, Monoid a) => Monoid (Lift f a)

instance (Applicative f, PreGroup a) => PreGroup (Lift f a) where
    inverse = coerce $ fmap @f @a inverse
    (//) = coerce $ liftA2 @f @a (//)

instance (Applicative f, PreNearsemiring a) => PreNearsemiring (Lift f a) where
    zero = coerce $ pure @f @a zero
    unit = coerce $ pure @f @a unit
    (+) = coerce $ liftA2 @f @a (+)
    (*) = coerce $ liftA2 @f @a (*)

instance (Applicative f, Nearsemiring a) => Nearsemiring (Lift f a)

instance (Applicative f, PreNearring a) => PreNearring (Lift f a) where
    negate = coerce $ fmap @f @a negate
    (-) = coerce $ liftA2 @f @a (-)
    fromInteger = coerce $ pure @f @a . fromInteger

instance (Applicative f, PreHeyting a) => PreHeyting (Lift f a) where
    top = coerce $ pure @f @a top
    bottom = coerce $ pure @f @a bottom
    (\/) = coerce $ liftA2 @f @a (\/)
    (/\) = coerce $ liftA2 @f @a (/\)
    (~>) = coerce $ liftA2 @f @a (~>)

instance (Applicative f, PreBoolean a) => PreBoolean (Lift f a) where
    not = coerce $ fmap @f @a not

Ring.hs

-- abstract syntax
class PreNearsemiring a where
    zero :: a
    unit :: a
    (+) :: a -> a -> a
    infixl 6 +
    (*) :: a -> a -> a
    infixl 7 *

-- addition is associative and has an identity
-- multiplication is associative and has an identity
-- multiplication distributes over addition
class PreNearsemiring a => Nearsemiring a where
    associativeAddition_Nearsemiring :: (a -> a -> t) -> a -> a -> a -> t
    associativeAddition_Nearsemiring = associative (+)

    leftIdentityAddition_Nearsemiring :: (a -> a -> t) -> a -> t
    leftIdentityAddition_Nearsemiring = leftIdentity (+) zero

    rightIdentityAddition_Nearsemiring :: (a -> a -> t) -> a -> t
    rightIdentityAddition_Nearsemiring = rightIdentity (+) zero

    associativeMultiplication_Nearsemiring :: (a -> a -> t) -> a -> a -> a -> t
    associativeMultiplication_Nearsemiring = associative (*)

    leftIdentityMultiplication_Nearsemiring :: (a -> a -> t) -> a -> t
    leftIdentityMultiplication_Nearsemiring = leftIdentity (*) unit

    rightIdentityMultiplication_Nearsemiring :: (a -> a -> t) -> a -> t
    rightIdentityMultiplication_Nearsemiring = rightIdentity (*) unit

    leftDistributive_Nearsemiring :: (a -> a -> t) -> a -> a -> a -> t
    leftDistributive_Nearsemiring = leftDistributive (*) (+)

    rightDistributive_Nearsemiring :: (a -> a -> t) -> a -> a -> a -> t
    rightDistributive_Nearsemiring = rightDistributive (*) (+)

-- addition is commutative
class Nearsemiring a => Semiring a where
    commutativeAddition_Semiring :: (a -> a -> t) -> a -> a -> t
    commutativeAddition_Semiring = commutative (+)

-- abstract syntax
class PreNearsemiring a => PreNearring a where
    negate :: a -> a
    (-) :: a -> a -> a
    x - y = x + negate y
    infixl 6 -

    -- default is lawful but may be overriden for efficiency
    fromInteger :: Integer -> a
    fromInteger = defaultFromInteger

defaultFromInteger :: (PreNearring a) => Integer -> a
defaultFromInteger n | n < 0     = negate . fromInteger . negate $ n
                     | otherwise = helper n zero where
                        helper 0 x = x
                        helper i x =
                            let i' = i - 1
                                x' = x + unit
                             in seq i' $ seq x' $ helper i' x'

-- addition is invertible
-- every nearring has an embedded copy of the integers (possibly modulo n)
-- fromInteger 0 is zero
-- fromInteger 1 is unit
-- fromInteger n (positive) is unit + ... + unit (n terms)
-- fromInteger n (negative) is negate (unit + ... + unit (n terms))
class (PreNearring a, Nearsemiring a) => Nearring a where
    leftInverse_Nearring :: (a -> a -> t) -> a -> t
    leftInverse_Nearring = leftInverse (+) zero negate id

    rightInverse_Nearring :: (a -> a -> t) -> a -> t
    rightInverse_Nearring = rightInverse (+) zero negate id

    integerEmbedding_Nearring :: (a -> a -> t) -> Integer -> t
    integerEmbedding_Nearring eq n = fromInteger n `eq` defaultFromInteger n

-- class alias
class (Nearring a, Semiring a) => Ring a
instance (Nearring a, Semiring a) => Ring a

-- multiplication is commutative
class Ring a => CommutativeRing a where
    commutative_CommutativeRing :: (a -> a -> t) -> a -> a -> t
    commutative_CommutativeRing = commutative (*)

-- TODO: we can do better
newtype Nonzero a = Nonzero { getNonzero :: a }

-- abstract syntax
class PreNearring a => PreDivisionRing a where
    recip :: Nonzero a -> Nonzero a
    (/) :: a -> Nonzero a -> a
    x / y = x *  getNonzero (recip y)
    infixl 7 /

    -- default is lawful but may be overriden for efficiency
    fromRational :: Rational -> a
    fromRational = defaultFromRational

defaultFromRational :: (PreDivisionRing a) => Rational -> a
defaultFromRational q = num q / den q where
    num = fromInteger . numerator
    den = Nonzero . fromInteger . denominator

-- multiplication is invertible
class (PreDivisionRing a, Ring a) => DivisionRing a where
    leftInverse_DivisionRing :: (a -> a -> t) -> Nonzero a -> t
    leftInverse_DivisionRing = leftInverse (*) unit recip getNonzero

    rightInverse_DivisionRing :: (a -> a -> t) -> Nonzero a -> t
    rightInverse_DivisionRing = rightInverse (*) unit recip getNonzero

    -- TODO: check if this is necessarily true
    rationalEmbedding_DivisionRing :: (a -> a -> t) -> Rational -> t
    rationalEmbedding_DivisionRing eq q =
        fromRational q `eq` defaultFromRational q

-- class alias
class (CommutativeRing a, DivisionRing a) => Field a
instance (CommutativeRing a, DivisionRing a) => Field a

instance PreNearsemiring Integer where
    zero = Num.fromInteger 0
    unit = Num.fromInteger 1
    (+) = (Num.+)
    (*) = (Num.*)

instance PreNearring Integer where
    negate = Num.negate
    (-) = (Num.-)
    fromInteger = Num.fromInteger

instance Nearsemiring Integer
instance Semiring Integer
instance Nearring Integer
instance CommutativeRing Integer

instance PreNearsemiring Rational where
    zero = Num.fromInteger 0
    unit = Num.fromInteger 1
    (+) = (Num.+)
    (*) = (Num.*)

instance PreNearring Rational where
    negate = Num.negate
    (-) = (Num.-)
    fromInteger = Num.fromInteger

instance PreDivisionRing Rational where
    recip = Nonzero . Fractional.recip . getNonzero
    x / Nonzero y = x Fractional./ y
    fromRational = Fractional.fromRational

instance Nearsemiring Rational
instance Semiring Rational
instance Nearring Rational
instance CommutativeRing Rational
instance DivisionRing Rational