module Data.Apiary.SList where
import GHC.Exts(Constraint)
data SList (as :: [*]) where
SNil :: SList '[]
(:::) :: a -> SList xs -> SList (a ': xs)
infixr :::
deriving instance All Show as => Show (SList as)
type family Fn (as :: [*]) r
type instance Fn '[] r = r
type instance Fn (x ': xs) r = x -> Fn xs r
type family Snoc (as :: [*]) a :: [*]
type instance Snoc '[] a = '[a]
type instance Snoc (x ': xs) a = x ': Snoc xs a
type family All (c :: * -> Constraint) (as :: [*]) :: Constraint
type instance All c '[] = ()
type instance All c (a ': as) = (c a, All c as)
apply :: Fn xs r -> SList xs -> r
apply v SNil = v
apply f (a ::: as) = apply (f a) as
sSnoc :: SList as -> a -> SList (Snoc as a)
sSnoc SNil a = a ::: SNil
sSnoc (x ::: xs) a = x ::: sSnoc xs a
type family Rev (l :: [*]) (a :: [*]) :: [*]
type instance Rev '[] a = a
type instance Rev (x ': xs) a = Rev xs (x ': a)
type Reverse (a :: [*]) = Rev a '[]
sReverse :: SList as -> SList (Reverse as)
sReverse l = rev l SNil
where
rev :: SList as -> SList bs -> SList (Rev as bs)
rev SNil a = a
rev (x:::xs) a = rev xs (x:::a)