algebra.hs

{-# LANGUAGE AllowAmbiguousTypes   #-}
{-# LANGUAGE DataKinds             #-}
{-# LANGUAGE FlexibleContexts      #-}
{-# LANGUAGE FlexibleInstances     #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE ScopedTypeVariables   #-}
{-# LANGUAGE TypeApplications      #-}
{-# LANGUAGE TypeFamilies          #-}

module Algebra where

import           Prelude hiding (Monoid)

-- $setup
-- >>> :set -XAllowAmbiguousTypes
-- >>> :set -XDataKinds
-- >>> :set -XFlexibleContexts
-- >>> :set -XFlexibleInstances
-- >>> :set -XMultiParamTypeClasses
-- >>> :set -XScopedTypeVariables
-- >>> :set -XTypeApplications
-- >>> :set -XTypeFamilies

data NumPlus a
data NumMultiply a

-- | Kind-of a singleton class for binary operations, which
-- associates an arbitrary proxy with some value-level operation.
class Magma m where
  type Carrier m
  op :: Carrier m -> Carrier m -> Carrier m

instance Num a => Magma (NumPlus a) where
  type Carrier (NumPlus a) = a
  op = (+)

instance Num a => Magma (NumMultiply a) where
  type Carrier (NumMultiply a) = a
  op = (*)

-- |
-- >>> example1 @(NumPlus Int)
-- 9
-- >>> example1 @(NumMultiply Int)
-- 24
example1 :: forall m . (Magma m, Num (Carrier m)) => Carrier m
example1 = 2 <> 3 <> 4
  where
    -- Carrier isn't injective and infix notation doesn't allow type
    -- applications, so this is a little unfortunate.
    (<>) = op @m

-- | Blah laws
class Magma m => SemiGroup m

instance Num a => SemiGroup (NumPlus a)

instance Num a => SemiGroup (NumMultiply a)

class SemiGroup m => Monoid m where
  neutral :: Carrier m

instance Num a => Monoid (NumPlus a) where
  neutral = 0

instance Num a => Monoid (NumMultiply a) where
  neutral = 1

class Monoid m => Group m where
  inverse :: Carrier m -> Carrier m

instance Num a => Group (NumPlus a) where
  inverse = negate

-- | Blah laws
class (Group add, Monoid mult, Carrier add ~ Carrier mult) => SemiRing add mult

instance Num a => SemiRing (NumPlus a) (NumMultiply a)

zero :: forall a m. SemiRing a m => Carrier a
zero = neutral @a

one :: forall a m. SemiRing a m => Carrier m
one = neutral @m

plus :: forall a m. SemiRing a m => Carrier a -> Carrier a -> Carrier a
plus = op @a

minus :: forall a m. SemiRing a m => Carrier a -> Carrier a -> Carrier a
minus x y = op @a x (inverse @a y)

multiply :: forall a m. SemiRing a m => Carrier m -> Carrier m -> Carrier m
multiply = op @m

-- |
-- >>> example2 @(NumPlus Int) @(NumMultiply _)
-- 25
example2 :: forall a m. (SemiRing a m, Num (Carrier a)) => Carrier a
example2 = ((o + ((five * five) - o)) - (five * z)) + z
  where
    z = zero @a @m
    o = one @a @m
    five = o + o + o + o + o
    (+) = plus @a @m
    (-) = minus @a @m
    (*) = multiply @a @m