Data.Apiary.SList

Documentation

data SList as where

Constructors

SNil :: SList []

(:::) :: a -> SList xs -> SList (a : xs) infixr 9

Instances

All Show as => Show (SList as)

type family Fn as r

Instances

type Fn ([] *) r = r

type Fn ((:) * x xs) r = x -> Fn xs r

type family Snoc as a :: [*]

Instances

type Snoc ([] *) a = (:) * a ([] *)

type Snoc ((:) * x xs) a = (:) * x (Snoc xs a)

type family All c as :: Constraint

Instances

type All c ([] *) = ()

type All c ((:) * a as) = (c a, All c as)

apply :: Fn xs r -> SList xs -> r

sSnoc :: SList as -> a -> SList (Snoc as a)

type family Rev l a :: [*]

Instances

type Rev ([] *) a = a

type Rev ((:) * x xs) a = Rev xs ((:) * x a)

type Reverse a = Rev a []

sReverse :: SList as -> SList (Reverse as)