Sorta representing laws in the Haskell type system

Monoid.hs

{-
Uses the She (Stathclyde Haskell Enhancement), which you
can get from http://bit.ly/gaVM8X.
-}

{-# OPTIONS_GHC -Wall -F -pgmF she #-}
{-# LANGUAGE GADTs, KindSignatures #-}
{-# LANGUAGE TypeFamilies, TypeOperators #-}
{-# LANGUAGE RankNTypes, FlexibleContexts #-}
{-# LANGUAGE MultiParamTypeClasses, NoImplicitPrelude #-}
module Monoid where
import ShePrelude

-- | Theory of equivalence
data (:=:) a :: * -> * where
  -- | Proof of equivalence
  Refl :: a :=: a

-- | Congruence proof
cong :: a :=: b -> f a :=: f b
cong Refl = Refl

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

-- | Monoid ops, include laws on type-level equivalents
class Monoid s where
  mempty  :: s
  mappend :: s -> s -> s
  
  midentl :: pi (ys :: s). MAppend s (MEmpty s) {ys} :=: {ys}
  midentr :: pi (xs :: s). MAppend s {xs} (MEmpty s) :=: {xs}
  massoc  :: pi (xs :: s). pi (ys :: s). pi (zs :: s).
             MAppend s (MAppend s {xs} {ys}) {zs} :=: MAppend s {xs} (MAppend s {ys} {zs})

-- | Sigs for type-level equivalents
type family MEmpty s :: {s}
type family MAppend s (xs :: {s}) (ys :: {s}) :: {s}
  
-------------

data List a where
  Nil  :: List a
  Cons :: a -> List a -> List a

instance Monoid (List a) where
  mempty  = Nil
  
  mappend Nil         ys = ys
  mappend (Cons x xs) ys = Cons x (mappend xs ys)
  
  midentl _ = Refl
  
  midentr {Nil}       = Refl
  midentr {Cons _ xs} = cong (midentr xs)
  
  massoc {Nil}        _    _   = Refl
  massoc {Cons _ xs} {ys} {zs} = cong (massoc xs ys zs)
  
type instance MEmpty (List a) = {Nil}
type instance MAppend (List a) {Nil}       ys = ys
type instance MAppend (List a) {Cons x xs} ys = {Cons} x (MAppend (List a) xs ys)

{- All this will be derived automatically one day. -}
data instance SheSingleton (List a) dummy where
    SheWitNil :: (SheSingleton (List a)) (SheTyNil)
    SheWitCons :: forall a sha0 sha1. (SheChecks (a ) sha0, SheChecks ( List a ) sha1) => SheSingleton (a ) sha0 -> SheSingleton ( List a ) sha1 -> (SheSingleton (List a)) (SheTyCons sha0 sha1)
    
instance SheChecks (List  a) (SheTyNil) where sheTypes _ = SheWitNil
                                              
instance (SheChecks (a ) sha0, SheChecks ( List a ) sha1) => SheChecks (List  a) (SheTyCons sha0 sha1) where sheTypes _ = SheWitCons (sheTypes (SheProxy :: SheProxy (a ) (sha0))) (sheTypes (SheProxy :: SheProxy ( List a ) (sha1)))

Monoid.hspp.hs

{-
Uses the She (Stathclyde Haskell Enhancement), which you
can get from http://bit.ly/gaVM8X.
-}{-# LINE 5 "Monoid.hs" #-}
{-# OPTIONS_GHC -Wall -F -pgmF she #-}{-# LINE 6 "Monoid.hs" #-}
{-# LANGUAGE GADTs, KindSignatures #-}{-# LINE 7 "Monoid.hs" #-}
{-# LANGUAGE TypeFamilies, TypeOperators #-}{-# LINE 8 "Monoid.hs" #-}
{-# LANGUAGE RankNTypes, FlexibleContexts #-}{-# LINE 9 "Monoid.hs" #-}
{-# LANGUAGE MultiParamTypeClasses, NoImplicitPrelude #-}{-# LINE 10 "Monoid.hs" #-}
module Monoid where{-# LINE 11 "Monoid.hs" #-}
import ShePrelude{-# LINE 13 "Monoid.hs" #-}
-- | Theory of equivalence{-# LINE 14 "Monoid.hs" #-}
data (:=:) a :: * -> * where{-# LINE 15 "Monoid.hs" #-}
  -- | Proof of equivalence{-# LINE 16 "Monoid.hs" #-}
  Refl :: a :=: a{-# LINE 18 "Monoid.hs" #-}
-- | Congruence proof{-# LINE 19 "Monoid.hs" #-}
cong :: a :=: b -> f a :=: f b{-# LINE 20 "Monoid.hs" #-}
cong Refl = Refl{-# LINE 22 "Monoid.hs" #-}
-------------{-# LINE 24 "Monoid.hs" #-}
-- | Monoid ops, include laws on type-level equivalents{-# LINE 25 "Monoid.hs" #-}
class Monoid s where{-# LINE 26 "Monoid.hs" #-}
  mempty  :: s{-# LINE 27 "Monoid.hs" #-}
  mappend :: s -> s -> s{-# LINE 28 "Monoid.hs" #-}
  {-# LINE 29 "Monoid.hs" #-}
  midentl :: forall ys . SheSingleton ( s) ys ->  MAppend s (MEmpty s) (ys) :=: (ys){-# LINE 30 "Monoid.hs" #-}
  midentr :: forall xs . SheSingleton ( s) xs ->  MAppend s (xs) (MEmpty s) :=: (xs){-# LINE 31 "Monoid.hs" #-}
  massoc  :: forall xs . SheSingleton ( s) xs ->  forall ys . SheSingleton ( s) ys ->  forall zs . SheSingleton ( s) zs -> {-# LINE 32 "Monoid.hs" #-}
             MAppend s (MAppend s (xs) (ys)) (zs) :=: MAppend s (xs) (MAppend s (ys) (zs)){-# LINE 34 "Monoid.hs" #-}
-- | Sigs for type-level equivalents{-# LINE 35 "Monoid.hs" #-}
type family MEmpty s :: *{-# LINE 36 "Monoid.hs" #-}
type family MAppend s (xs :: *) (ys :: *) :: *{-# LINE 37 "Monoid.hs" #-}
  {-# LINE 38 "Monoid.hs" #-}
-------------{-# LINE 40 "Monoid.hs" #-}
data List a where{-# LINE 41 "Monoid.hs" #-}
  Nil  :: List a{-# LINE 42 "Monoid.hs" #-}
  Cons :: a -> List a -> List a{-# LINE 44 "Monoid.hs" #-}
instance Monoid (List a) where{-# LINE 45 "Monoid.hs" #-}
  mempty  = Nil{-# LINE 46 "Monoid.hs" #-}
  {-# LINE 47 "Monoid.hs" #-}
  mappend Nil         ys = ys{-# LINE 48 "Monoid.hs" #-}
  mappend (Cons x xs) ys = Cons x (mappend xs ys){-# LINE 49 "Monoid.hs" #-}
  {-# LINE 50 "Monoid.hs" #-}
  midentl _ = Refl{-# LINE 51 "Monoid.hs" #-}
  {-# LINE 52 "Monoid.hs" #-}
  midentr (SheWitNil)       = Refl{-# LINE 53 "Monoid.hs" #-}
  midentr (SheWitCons _ xs) = cong (midentr xs){-# LINE 54 "Monoid.hs" #-}
  {-# LINE 55 "Monoid.hs" #-}
  massoc (SheWitNil)        _    _   = Refl{-# LINE 56 "Monoid.hs" #-}
  massoc (SheWitCons _ xs) (ys) (zs) = cong (massoc xs ys zs){-# LINE 57 "Monoid.hs" #-}
  {-# LINE 58 "Monoid.hs" #-}
type instance MEmpty (List a) = (SheTyNil){-# LINE 59 "Monoid.hs" #-}
type instance MAppend (List a) (SheTyNil)       ys = ys{-# LINE 60 "Monoid.hs" #-}
type instance MAppend (List a) (SheTyCons x xs) ys = (SheTyCons) x (MAppend (List a) xs ys){-# LINE 62 "Monoid.hs" #-}
{- All this will be derived automatically one day. -}{-# LINE 63 "Monoid.hs" #-}
data instance SheSingleton (List a) dummy where{-# LINE 64 "Monoid.hs" #-}
    SheWitNil :: (SheSingleton (List a)) (SheTyNil){-# LINE 65 "Monoid.hs" #-}
    SheWitCons :: forall a sha0 sha1. (SheChecks (a ) sha0, SheChecks ( List a ) sha1) => SheSingleton (a ) sha0 -> SheSingleton ( List a ) sha1 -> (SheSingleton (List a)) (SheTyCons sha0 sha1){-# LINE 66 "Monoid.hs" #-}
    {-# LINE 67 "Monoid.hs" #-}
instance SheChecks (List  a) (SheTyNil) where sheTypes _ = SheWitNil{-# LINE 68 "Monoid.hs" #-}
                                              {-# LINE 69 "Monoid.hs" #-}
instance (SheChecks (a ) sha0, SheChecks ( List a ) sha1) => SheChecks (List  a) (SheTyCons sha0 sha1) where sheTypes _ = SheWitCons (sheTypes (SheProxy :: SheProxy (a ) (sha0))) (sheTypes (SheProxy :: SheProxy ( List a ) (sha1))){-# LINE 10 "Monoid.hs" #-}
data SheTyRefl = SheTyRefl{-# LINE 10 "Monoid.hs" #-}
data SheTyNil = SheTyNil{-# LINE 10 "Monoid.hs" #-}
data SheTyCons x1 x2 = SheTyCons x1 x2{-# LINE 10 "Monoid.hs" #-}
data SheTySheWitNil = SheTySheWitNil{-# LINE 10 "Monoid.hs" #-}
data SheTySheWitCons x1 x2 = SheTySheWitCons x1 x2