Perm.hs

-- GHCi example:
--   ghci > mempty @(Permutation (Nx (Nx (Nx Zr))) Int)
--   Perm ((:++) 0 ((:++) 1 ((:++) 2 EmptyVec)))

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}

data Nat = Zr | Nx Nat


instance
  ( Integral i
  )
    => Semigroup (Permutation n i)
  where
    (<>) = undefined

instance
  ( Integral i
  )
    => Monoid (Permutation Zr i)
  where
    mempty = Perm EmptyVec

instance
  ( Integral i
  , Monoid (Permutation n i)
  )
    => Monoid (Permutation (Nx n) i)
  where
    mempty =
      case mempty @(Permutation n i) of
        Perm z -> Perm (0 :++ vecMap succ z)

newtype Permutation n a =
  Perm (Vector n a)
  deriving Show

data Vector n a where
  EmptyVec :: Vector Zr a
  (:++) :: a -> Vector n a -> Vector (Nx n) a

deriving instance Show a => Show (Vector n a)

vecMap :: (a -> b) -> Vector n a -> Vector n b
vecMap f EmptyVec = EmptyVec
vecMap f (x :++ xs) = f x :++ vecMap f xs