instance pi n. Show (Fin n)

showelem.hs

data SVec :: forall n a. Vec n a -> Type where
 SVecO :: SVec VecO
 SVecS :: Sing a -> SVec as -> SVec (a :> as)

type instance Sing @(Vec n a) = SVec @n @a

instance SingI VecO where
 sing :: Sing VecO
 sing = SVecO

instance (SingI a, SingI as) => SingI (a :> as) where
 sing :: Sing (a :> as)
 sing = SVecS sing sing

----

type Elem :: forall a n. Vec n a -> a -> Type
data Elem as a where
  Here  :: Elem (a:>as) a
  There :: Elem bs      b
        -> Elem (a:>bs) b

pattern Here0 :: forall {sn}      {k} {vec :: Vec sn      k} {a}. () => forall n           (as :: Vec n k). (sn      ~ S n,                     vec ~~ (a:>as))                => Elem vec a
pattern Here1 :: forall {ssn}     {k} {vec :: Vec ssn     k} {b}. () => forall n a         (as :: Vec n k). (ssn     ~ S (S n),                 vec ~~ (a:>b:>as))             => Elem vec b
pattern Here2 :: forall {sssn}    {k} {vec :: Vec sssn    k} {c}. () => forall n a b       (as :: Vec n k). (sssn    ~ S (S (S n)),             vec ~~ (a:>b:>c:>as))          => Elem vec c
pattern Here3 :: forall {ssssn}   {k} {vec :: Vec ssssn   k} {d}. () => forall n a b c     (as :: Vec n k). (ssssn   ~ S (S (S (S n))),         vec ~~ (a:>b:>c:>d:>as))       => Elem vec d
pattern Here4 :: forall {sssssn}  {k} {vec :: Vec sssssn  k} {e}. () => forall n a b c d   (as :: Vec n k). (sssssn  ~ S (S (S (S (S n)))),     vec ~~ (a:>b:>c:>d:>e:>as))    => Elem vec e
pattern Here5 :: forall {ssssssn} {k} {vec :: Vec ssssssn k} {f}. () => forall n a b c d e (as :: Vec n k). (ssssssn ~ S (S (S (S (S (S n))))), vec ~~ (a:>b:>c:>d:>e:>f:>as)) => Elem vec f
pattern Here0 = Here
pattern Here1 = There Here0
pattern Here2 = There Here1
pattern Here3 = There Here2
pattern Here4 = There Here3
pattern Here5 = There Here4

-- >> Here0 @Five @(Int:>Int:>Int:>Int:>Int:>VecO)
-- [x,_,_,_,_,_]
-- >> Here1 @Four @(Int:>Int:>Int:>Int:>VecO)
-- [_,x,_,_,_,_]
-- >> Here2 @Three @(Int:>Int:>Int:>VecO)
-- [_,_,x,_,_,_]
-- >> Here3 @Two @(Int:>Int:>VecO)
-- [_,_,_,x,_,_]
-- >> Here4 @One @(Int:>VecO)
-- [_,_,_,_,x,_]
-- >> Here5 @O @VecO
-- [_,_,_,_,_,x]

instance SingI vec => Show (Elem vec a) where
 show :: Elem vec a -> String
 show elem = "[" ++ intercalate "," (sh sing elem) ++ "]" where

  sh :: Sing m -> Elem m a -> [String]
  sh (SVecS a as) Here         = "x" : replicate as
  sh (SVecS a as) (There elem) = "_" : sh as elem

  replicate :: forall n a (vec :: Vec n a). Sing vec -> [String]
  replicate SVecO        = []
  replicate (SVecS a as) = "_" : replicate as

showfin.hs

{-# Language DataKinds                #-}
{-# Language GADTs                    #-}
{-# Language KindSignatures           #-}
{-# Language ScopedTypeVariables      #-}
{-# Language StandaloneKindSignatures #-}
{-# Language TemplateHaskell          #-}
{-# Language TypeApplications         #-}
{-# Language TypeFamilies             #-}

import Data.Singletons
import Data.Singletons.TH
import Data.Kind
import Data.List

singletons [d| data N = O | S N |]

type One   :: N
type Two   :: N
type Three :: N
type Four  :: N
type Five  :: N
type Six   :: N
type One   = S O
type Two   = S One
type Three = S Two
type Four  = S Three
type Five  = S Four
type Six   = S Five

type Fin :: N -> Type
data Fin n where
 FinO :: Fin (S n)
 FinS :: Fin n -> Fin (S n)

-- >> Fin0 @Five
-- [x,_,_,_,_,_]
-- >> Fin1 @Four
-- [_,x,_,_,_,_]
-- >> Fin2 @Three
-- [_,_,x,_,_,_]
-- >> Fin3 @Two
-- [_,_,_,x,_,_]
-- >> Fin4 @One
-- [_,_,_,_,x,_]
-- >> Fin5 @O
-- [_,_,_,_,_,x]
instance SingI n => Show (Fin n) where
 show :: Fin n -> String
 show fin = "[" ++ intercalate "," (sh sing fin) ++ "]" where

  sh :: Sing m -> Fin m -> [String]
  sh (SS n) FinO       = "x" : replicate n
  sh (SS n) (FinS fin) = "_" : sh n fin

  replicate :: Sing @N j -> [String]
  replicate SO     = []
  replicate (SS n) = "_" : replicate n

pattern Fin0 :: forall {sn}.       () => forall n. sn      ~ S n                      => Fin sn
pattern Fin1 :: forall {ssn}.      () => forall n. ssn     ~ S (S n)                  => Fin ssn
pattern Fin2 :: forall {sssn}.     () => forall n. sssn    ~ S (S (S n))              => Fin sssn
pattern Fin3 :: forall {ssssn}.    () => forall n. ssssn   ~ S (S (S (S n)))          => Fin ssssn
pattern Fin4 :: forall {sssssn}.   () => forall n. sssssn  ~ S (S (S (S (S n))))      => Fin sssssn
pattern Fin5 :: forall {ssssssn}.  () => forall n. ssssssn ~ S (S (S (S (S (S n)))))  => Fin ssssssn
pattern Fin0 = FinO
pattern Fin1 = FinS Fin0
pattern Fin2 = FinS Fin1
pattern Fin3 = FinS Fin2
pattern Fin4 = FinS Fin3
pattern Fin5 = FinS Fin4