```module StarSemiring where

import Data.Maybe (listToMaybe)

infixl 6 <+>
infixl 7 <.>

{- Laws:
- a <+> b = b <+> a
- (a <+> b) <+> c = a <+> (b <+> c)
- a <+> zero = zero <+> a = a
- (a <.> b) <.> c = a <.> (b <.> c)
- a <.> one = one <.> a = a
- a <.> zero = zero <.> a = zero
- a <.> (b <+> c) = a <.> b <+> a <.> c
- (a <+> b) <.> c = a <.> c <+> b <.> c
-}
class Semiring a where
zero  :: a
(<+>) :: a -> a -> a
one   :: a
(<.>) :: a -> a -> a
srsum :: [a] -> a
srsum = foldr (<+>) zero
srprod :: [a] -> a
srprod = foldr (<.>) one

{- Laws:
- star a = one <+> a <.> star a = one <+> star a <.> a
-}
class Semiring a => StarSemiring a where
star :: a -> a
star a = one <+> plus a
plus :: a -> a
plus a = a <.> star a

{- Laws:
- a <+> a = a
- a <.> x <+> x = x ==> star a <.> x <+> x = x
- x <.> a <+> x = x ==> x <.> star a <+> x = x
-}

class StarSemiring a => KleeneAlgebra a where

data StarSemiringExpr a = Var a
| Or (StarSemiringExpr a) (StarSemiringExpr a)
| Seq (StarSemiringExpr a) (StarSemiringExpr a)
| Star (StarSemiringExpr a)
| None
| Empty

newtype RE a = RE (StarSemiringExpr a)

re :: a -> RE a
re = RE . Var

instance Eq a => Eq (RE a) where
(RE x) == (RE y) = todo

-- While we could simply implement *-semiring operations directly as the constructors of StarSemiringExpr, instead we will take advantage of this opportunity to implement a few local simplifications: identities of ε and 0, absorption of 0, idempotency of asteration, and the following theorems of regular expressions:
-- ε + ε = ε
-- ε + x∗ = x∗
-- x∗ + ε = x∗

instance Semiring (RE a) where
zero = RE None
RE None <+> y = y
x <+> RE None = x
RE Empty <+> RE Empty = RE Empty
RE Empty <+> RE (Star y) = RE (Star y)
RE (Star x) <+> RE Empty = RE (Star x)
RE x <+> RE y = RE (x `Or` y)
one = RE Empty
RE Empty <.> y = y
x <.> RE Empty = x
RE None <.> _  = RE None
_ <.> RE None  = RE None
RE x <.> RE y  = RE (x `Seq` y)

instance StarSemiring (RE a) where
star (RE None) = RE Empty
star (RE Empty) = RE Empty
star (RE (Star x)) = star (RE x)
star (RE x) = RE (Star x)

data Tropical a = Tropical a
| Infinity deriving (Eq, Ord)

instance (Ord a, Num a) => Semiring (Tropical a) where
zero = Infinity
Infinity <+> y = y
x <+> Infinity = x
(Tropical a) <+> (Tropical b) = Tropical (min a b)
one = Tropical 0
Infinity <.> _ = Infinity
_ <.> Infinity = Infinity
(Tropical x) <.> (Tropical y) = Tropical (x + y)

instance (Ord a, Num a) => StarSemiring (Tropical a) where
star _ = one

instance (Ord a, Num a) => KleeneAlgebra (Tropical a) where

data ShortestPath a b = ShortestPath (Tropical a) b

instance Functor (ShortestPath a) where
fmap f (ShortestPath a x) = ShortestPath a (f x)

extract :: ShortestPath a b -> b
extract (ShortestPath _ x) = x

instance (Ord a, Num a, Semiring b) => Semiring (ShortestPath a b) where
zero = ShortestPath zero zero
ShortestPath a x <+> ShortestPath b y | c < b = ShortestPath a x
| c < a = ShortestPath b y
| otherwise = ShortestPath c (x <+> y)
where
c = a <+> b
one = ShortestPath one one
ShortestPath a x <.> ShortestPath b y = ShortestPath (a <.> b) (x <.> y)

instance (Ord a, Num a, StarSemiring b) => StarSemiring (ShortestPath a b) where
star (ShortestPath x b) | x == one  = ShortestPath one (star b)
| otherwise = ShortestPath one one

instance (Ord a, Num a, KleeneAlgebra b) => KleeneAlgebra (ShortestPath a b) where

newtype Language a = Language [[a]]

letter x = Language [[x]]

instance Semiring (Language a) where
zero = Language []
(Language x) <+> (Language y) = Language (x `interleave` y)
where
[]     `interleave` ys = ys
(x:xs) `interleave` ys = x:(ys `interleave` xs)
one = Language (pure [])
(Language x) <.> (Language y) = Language (dovetail (++) x y)
where
dovetail f l1 l2 = concat \$ go l1 (scanl (flip (:)) [] l2)
where
go [] _           = []
go l1 l2@(x:y:ys) = (zipWith f l1 x):(go l1 (y:ys))
go l1@(a:as) [x]  = (zipWith f l1 x):(go as [x])

instance StarSemiring (Language a) where
star (Language l) = one <+> plusList (filter (not . null) l)
where
plusList [] = zero
plusList l  = star (Language l) <.> (Language l)

someWord :: Language a -> Maybe [a]
someWord (Language l) = listToMaybe l

evalRE :: (KleeneAlgebra a) => (l -> a) -> RE l -> a
evalRE f (RE None) = zero
evalRE f (RE Empty) = one
evalRE f (RE (Var a)) = f a
evalRE f (RE (Star x)) = star (evalRE f (RE x))
evalRE f (RE (x `Or` y)) = (evalRE f (RE x)) <+> (evalRE f (RE y))
evalRE f (RE (x `Seq` y)) = (evalRE f (RE x)) <.> (evalRE f (RE y))

data Compact a = Real a
| Inf

instance (Eq a, Num a) => Semiring (Compact a) where
zero = Real 0
Inf <+> _ = Inf
_ <+> Inf = Inf
Real x <+> Real y = Real (x + y)
one = Real 1
Real 0 <.> _ = Real 0
_ <.> Real 0 = Real 0
Inf <.> _ = Inf
_ <.> Inf = Inf
Real x <.> Real y = Real (x * y)

instance (Eq a, Fractional a) => StarSemiring (Compact a) where
star (Real 1) = Inf
star (Real x) = Real (recip (1 - x))
star Inf      = Inf

instance Semiring (StarSemiringExpr a) where
zero = None
None <+> y = y
x <+> None = x
x <+> y = x `Or` y
one = Empty
Empty <.> y = y
x <.> Empty = x
None <.> _ = None
_ <.> None = None
x <.> y = x `Seq` y

instance StarSemiring (StarSemiringExpr a) where
star None = Empty
star x    = Star x

evalSSE :: (StarSemiring a) => (l -> a) -> StarSemiringExpr l -> a
evalSSE f None        = zero
evalSSE f Empty       = one
evalSSE f (Var a)     = f a
evalSSE f (Star x)    = star (evalSSE f x)
evalSSE f (x `Or` y)  = (evalSSE f x) <+> (evalSSE f y)
evalSSE f (x `Seq` y) = (evalSSE f x) <.> (evalSSE f y)
-- | Below you will find an appendix of functions that completes this module.
--

instance Show a => Show (StarSemiringExpr a) where
showsPrec d (Var a) = showParen (d > 10) (shows a)
showsPrec d Empty = showParen (d > 10) (showString "ε")
showsPrec d None = showParen (d > 10) (showString "0")
showsPrec d (Star x) = showParen (d > 9) (showsPrec 9 x . showString "*")
showsPrec d (x `Or` y) = showParen (d > 6) showStr
where
showStr = showsPrec 6 x . showString "|" . showsPrec 6 y
showsPrec d (x `Seq` y) = showParen (d > 7) showStr
where
showStr = showsPrec 7 x . showsPrec 7 y

instance Show a => Show (RE a) where
showsPrec d (RE x) = showsPrec d x

instance Show a => Show (Tropical a) where
show (Tropical a) = show a
show Infinity = "∞"

instance (Show a, Show b) => Show (ShortestPath a b) where
show (ShortestPath a x) = show x ++ "[" ++ show a ++ "]"

instance (Show a) => Show (Compact a) where
show (Real a) = show a
show Inf = "∞"

todo = error "TODO"
```