AppendProof.hs

{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeOperators #-}

module Main where

import GHC.Types
import GHC.TypeLits
import Data.Type.Equality
import Data.Singletons
import Data.Type.Natural.Builtin
import GHC.TypeLits.Witnesses

main :: IO ()
main = pure ()

data Vec :: Type -> Nat -> Type where
  Nil :: Vec a 0
  (:>) :: KnownNat n => a -> Vec a n -> Vec a (n + 1)

deriving instance  Show a => Show (Vec a n)
infixr 5 :>

vec1 = 'h' :> Nil
vec2 = 'e' :> Nil
vec3 = 'l' :> Nil
vec4 = 'l' :> Nil

{-> :t vec1 `append` vec2 `append` vec3 `append` vec4

vec1 `append` vec2 `append` vec3 `append` vec4 :: Vec Char 4
-}

{-> vec1 `append` vec2 `append` vec3 `append` vec4

'h' :> ('e' :> ('l' :> ('l' :> Nil)))
-}

append :: forall a n m. Vec a n -> Vec a m -> Vec a (n + m)
append Nil w = w
append (a :> (v :: Vec a n1)) w = withLength w $
  let m = sing :: Sing m
      n' = sing :: Sing n1
  in
  case (support n' m Refl) of
      (Refl :: (n1 + m) + 1 :~: (n + m)) ->
        withNatOp (%+) (Proxy @n1) (Proxy @m) $
         a :> (append v w)

withLength :: Vec a n -> (KnownNat n => r) -> r
withLength Nil x = x
withLength (_ :> (_ :: Vec a n1)) x =
  withNatOp (%+) (Proxy @n1) (Proxy @1) x

support :: forall n n' m. Sing n' -> Sing m -> (n :~: n' + 1) -> (((n' + m) + 1) :~: (n + m))
support n' m Refl =
  let r = plusAssocSwap n' _1 m
   in gcastWith r Refl
  where _1 = sing :: Sing 1

plusAssocSwap :: forall p q r. Sing p -> Sing q -> Sing r -> (((p + q) + r) :~: ((p + r) + q))
plusAssocSwap p q r =
  let p0 = plusAssoc p q r
      p1 = plusComm q r
      p2 = sym (plusAssoc p r q)
   in trans p0 (trans (gcastWith p1 Refl) p2)