List append associativity proof in Haskell's type system... perhaps

List.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 #-}
module List where
import Prelude ()
import ShePrelude

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

-- | Value-level append
append :: List a -> List a -> List a
append Nil         ys = ys
append (Cons x xs) ys = Cons x (append xs ys)

-- | Type-level append
type family Append (xs :: {List a}) (ys :: {List a})
type instance Append {Nil}       ys = ys
type instance Append {Cons x xs} ys = {Cons} x (Append xs ys)

-- | Value-level map
map :: (a -> b) -> List a -> List b
map _ Nil         = Nil
map f (Cons x xs) = Cons (f x) (map f xs)

-- | Type-level map     \/ Why can't I write `{a -> b}`?
type family Map (f :: * -> *) (xs :: {List a})
type instance Map f {Nil}       = {Nil}
type instance Map f {Cons x xs} = {Cons} (f x) (Map f xs)

-- | Equivalence
data (:=:) a :: * -> * where
  Refl :: a :=: a

-- | Congruence proof
cong :: x :=: y -> f x :=: f y
cong Refl = Refl

-- | Proof of append associativity
class ListClass (xs :: {List a}) where 
  appendAssoc :: xs -> ys -> zs -> Append xs (Append ys zs) :=: Append (Append xs ys) zs
  mapDistribApp :: (forall a. f a) -> xs -> ys -> Map f (Append xs ys) :=: Append (Map f xs) (Map f ys)  

instance ListClass {Nil} where
  appendAssoc _ _ _ = Refl
  mapDistribApp _ _ _ = Refl
  
instance (ListClass xs) => ListClass {Cons x xs} where
  appendAssoc (SheTyCons _ xs) ys zs = cong (appendAssoc xs ys zs)
      -- A hack /\ and \/ as She insisted on naming the constructor differently
  mapDistribApp f (SheTyCons _ xs) ys = cong (mapDistribApp f xs ys)

{-
Updated following http://bit.ly/gSX36R with
Conor.

Above proofs again using the pi types approach.
Had to hack my own SheSingleton instance
as it didn't like polymorphic types. 
While missing cases do trigger GHC's -Wall,
I prefer the error messages I got using
the above approach.
-}

appendAssoc' :: forall a ys zs. pi (xs :: List a). ys -> zs -> Append {xs} (Append ys zs) :=: Append (Append {xs} ys) zs
appendAssoc' {Nil}       _  _  = Refl
appendAssoc' {Cons _ xs} ys zs = cong (appendAssoc' xs ys zs)

mapDistribApp' :: forall a f ys. (forall d. f d) -> pi (xs :: List a). ys -> Map f (Append {xs} ys) :=: Append (Map f {xs}) (Map f ys)
mapDistribApp' _ {Nil}       _  = Refl
mapDistribApp' f {Cons _ xs} ys = cong (mapDistribApp' f xs ys)

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)))