Skip to content

Instantly share code, notes, and snippets.

@Icelandjack
Last active Sep 17, 2020
Embed
What would you like to do?
instance pi n. Show (Fin n)
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
{-# 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
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment