rev.hs

{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE DataKinds, GADTs, TypeFamilies, PolyKinds, TypeOperators #-}
{-# LANGUAGE RankNTypes, TypeApplications #-}
import Prelude(($), putStrLn)

-- equality

infix 2 ==
data (==) :: k -> k -> * where
  Refl :: a == a

cong :: a == b -> f a == f b
cong Refl = Refl

congApp :: f == g -> x -> f x == g x
congApp Refl x = Refl

refl :: a == a
refl = Refl

sym :: a == b -> b == a
sym Refl = Refl

trans :: a == b -> b == c -> a == c
trans Refl Refl = Refl

data family Sing (typ :: k)

-- equational reasoning of `==`
data Tuple a b where
  Mk2 :: a -> b -> Tuple a b

data instance Sing (typ :: Tuple a b) where
  STuple :: Sing a -> Sing b -> Sing (Mk2 a b)

(===) :: Sing a -> Sing b -> Sing (Mk2 a b)
(===) a b = STuple a b

infixl 3 `by`
by :: Sing (Mk2 a b) -> a == b -> b == c -> a == c
by _ = trans

qed :: forall a. a == a
qed = refl

ex :: Sing a -> Sing b -> Sing c -> Sing d -> a == b -> b == c -> c == d -> a == d
ex a b c d ab bc cd =
  a === b `by` ab $
  b === c `by` bc $
  c === d `by` cd $ qed

-- list

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

type family (++) (x :: List a) (y :: List a) :: List a where
  Nil ++ l = l
  (Cons x xs) ++ l = Cons x (xs ++ l)

data instance Sing (typ :: List a) where
  SNil :: Sing Nil
  SCons :: Sing x -> Sing xs -> Sing (Cons x xs)

(++:) :: Sing xs -> Sing ys -> Sing (xs ++ ys)
SNil ++: l = l
SCons x xs ++: l = SCons x (xs ++: l)

-- proof

appendNilRight :: Sing xs -> (xs ++ Nil) == xs
appendNilRight SNil = Refl
appendNilRight (SCons x xs) =
  SCons x xs ++: SNil === SCons x (xs ++: SNil) `by` Refl $
  SCons x (xs ++: SNil) === SCons x xs `by` cong (appendNilRight xs) $ qed

appendAssoc :: Sing xs -> Sing ys -> Sing zs -> xs ++ (ys ++ zs) == (xs ++ ys) ++ zs
appendAssoc SNil _ _ = Refl
appendAssoc (SCons x xs) ys zs =
  SCons x xs ++: (ys ++: zs) === SCons x (xs ++: (ys ++: zs)) `by` Refl $
  SCons x (xs ++: (ys ++: zs)) === SCons x ((xs ++: ys) ++: zs) `by` cong (appendAssoc xs ys zs) $ qed

type family Reverse (xs :: List a) :: List a where
  Reverse Nil = Nil
  Reverse (Cons x xs) = Reverse xs ++ Cons x Nil

reverse :: Sing xs -> Sing (Reverse xs)
reverse SNil = SNil
reverse (SCons x xs) = reverse xs ++: SCons x SNil

revAppend :: Sing xs -> Sing ys -> Reverse (xs ++ ys) == Reverse ys ++ Reverse xs
revAppend xs SNil =
  reverse (xs ++: SNil) === reverse xs `by` congReverse (appendNilRight xs) $
  reverse xs === (SNil ++: reverse xs) `by` Refl $ qed
  where
    congReverse :: a == b -> Reverse a == Reverse b
    congReverse Refl = Refl
revAppend SNil ys =
  reverse (SNil ++: ys) === reverse ys `by` Refl $
  reverse ys === (reverse ys ++: reverse SNil) `by` (sym $ appendNilRight (reverse ys)) $ qed
revAppend (SCons x xs) ys =
  reverse (SCons x xs ++: ys) === reverse (SCons x (xs ++: ys)) `by` Refl $
  reverse (SCons x (xs ++: ys)) === (reverse (xs ++: ys) ++: SCons x SNil) `by` Refl $
  (reverse (xs ++: ys) ++: SCons x SNil) === ((reverse ys ++: reverse xs) ++: SCons x SNil) `by` congAppend x (revAppend xs ys) $
  ((reverse ys ++: reverse xs) ++: SCons x SNil) === (reverse ys ++: (reverse xs ++: SCons x SNil)) `by` sym (appendAssoc (reverse ys) (reverse xs) (SCons x SNil)) $
  (reverse ys ++: (reverse xs ++: SCons x SNil)) === (reverse ys ++: reverse (SCons x xs)) `by` Refl $ qed
  where
    congAppend :: Sing x -> a == b -> a ++ Cons x Nil == b ++ Cons x Nil
    congAppend _ Refl = Refl

revRevId :: Sing xs -> Reverse (Reverse xs) == xs
revRevId SNil = Refl
revRevId (SCons x xs) =
  reverse (reverse (SCons x xs)) === reverse (reverse xs ++: SCons x SNil) `by` Refl $
  reverse (reverse xs ++: SCons x SNil) === (reverse (SCons x SNil) ++: reverse (reverse xs)) `by` revAppend (reverse xs) (SCons x SNil) $
  (reverse (SCons x SNil) ++: reverse (reverse xs)) === (SCons x SNil ++: reverse (reverse xs)) `by` Refl $
  (SCons x SNil ++: reverse (reverse xs)) === (SCons x SNil ++: xs) `by` cong (revRevId xs) $
  (SCons x SNil ++: xs) === SCons x xs `by` Refl $ qed

main = do
  putStrLn "Proved: rev . rev = id"