Maintainer	gatlin@niltag.net
Safe Haskell	Safe-Inferred
Language	Haskell2010

Lists

Contents

Counted Lists
- Counted utilities
Conic Lists
- Type-level conic manipulation
Conversion

Description

Counted lists have a length represented by a Peano number encoded in their types which permit compile-time bounds checking.

The members of Conic lists, meanwhile, do not need to be all of the same type. The type of each list member is encoded in the list's type signature.

Synopsis

data Counted (n :: Type) (a :: Type)
- = forall t.n ~ S t => a ::: (Counted t a)
- | n ~ Z => CountedNil
count :: Counted n a -> Natural n
unCount :: Counted n a -> [a]
replicate :: Natural n -> x -> Counted n x
append :: Counted n a -> Counted m a -> Counted (m + n) a
nth :: n < m => Natural n -> Counted m a -> a
padTo :: m <= n => Natural n -> x -> Counted m x -> Counted ((n - m) + m) x
zip :: Counted n a -> Counted n b -> Counted n (a, b)
data Conic f ts
- = forall rest a.ts ~ (a :-: rest) => (f a) :-: (Conic f rest)
- | ts ~ Nil => ConicNil
data (x :: k1) :-: (y :: k2)
data Nil
class ReifyNatural n => Replicable n (x :: k) where
- type Replicate n x :: Type
class Tackable (x :: k) (xs :: Type) where
- type Tack x xs :: Type
- tack :: f x -> Conic f xs -> Conic f (Tack x xs)
class HasLength (ts :: k) where
- type Length ts :: Type
heterogenize :: (a -> f t) -> Counted n a -> Conic f (Replicate n t)
homogenize :: (forall t. f t -> a) -> Conic f ts -> Counted (Length ts) a

Counted Lists

data Counted (n :: Type) (a :: Type) Source #

A Counted list encodes its length as a type parameter.

Constructors

forall t.n ~ S t => a ::: (Counted t a) infixr 5	Prepend an item.
n ~ Z => CountedNil	Construct an empty list.

Instances

Instances details

ReifyNatural n => Applicative (Counted n) Source #
Instance details Defined in Lists Methods pure :: a -> Counted n a Source # (<>) :: Counted n (a -> b) -> Counted n a -> Counted n b Source # liftA2 :: (a -> b -> c) -> Counted n a -> Counted n b -> Counted n c Source # (>) :: Counted n a -> Counted n b -> Counted n b Source # (<*) :: Counted n a -> Counted n b -> Counted n a Source #
Functor (Counted n) Source #
Instance details Defined in Lists Methods fmap :: (a -> b) -> Counted n a -> Counted n b Source # (<$) :: a -> Counted n b -> Counted n a Source #
Show x => Show (Counted n x) Source #
Instance details Defined in Lists Methods showsPrec :: Int -> Counted n x -> ShowS Source # show :: Counted n x -> String Source # showList :: [Counted n x] -> ShowS Source #
Eq a => Eq (Counted n a) Source #
Instance details Defined in Lists Methods (==) :: Counted n a -> Counted n a -> Bool Source # (/=) :: Counted n a -> Counted n a -> Bool Source #

count :: Counted n a -> Natural n Source #

Compute the length of a Counted in terms of a Natural.

unCount :: Counted n a -> [a] Source #

Counted utilities

replicate :: Natural n -> x -> Counted n x Source #

append :: Counted n a -> Counted m a -> Counted (m + n) a Source #

nth :: n < m => Natural n -> Counted m a -> a Source #

padTo :: m <= n => Natural n -> x -> Counted m x -> Counted ((n - m) + m) x Source #

Pad the length of a list to a given length. If the number specified is less than the length of the list given, it won't pass the type checker. [^1]

zip :: Counted n a -> Counted n b -> Counted n (a, b) Source #

Conic Lists

data Conic f ts Source #

Conic lists are lists where each element is an f a for some a, but the a may be different for each element. Types of elements are kept track of in the type list.

Constructors

forall rest a.ts ~ (a :-: rest) => (f a) :-: (Conic f rest) infixr 5
ts ~ Nil => ConicNil

data (x :: k1) :-: (y :: k2) infixr 5 Source #

Instances

Instances details

Tackable a xs => Tackable (a :: k) (x :-: xs) Source #
Instance details Defined in Lists Associated Types type Tack a (x :-: xs) Source # Methods tack :: f a -> Conic f (x :-: xs) -> Conic f (Tack a (x :-: xs)) Source #
HasLength (x :-: xs :: Type) Source #
Instance details Defined in Lists Associated Types type Length (x :-: xs) Source #
CombineRefLists Nil (b :-: bs) Source #
Instance details Defined in Sheet Methods (&) :: RefList Nil -> RefList (b :-: bs) -> RefList (Nil & (b :-: bs)) Source #
Go ('Relative :-: Nil) (Nested (F Tape)) Source #
Instance details Defined in Sheet Methods go :: forall (a :: k). RefList ('Relative :-: Nil) -> Nested (F Tape) a -> Nested (F Tape) a Source #
(Go rs (Nested ts), Functor (Nested ts)) => Go ('Relative :-: rs) (Nested (N ts Tape) :: Type -> Type) Source #
Instance details Defined in Sheet Methods go :: forall (a :: k). RefList ('Relative :-: rs) -> Nested (N ts Tape) a -> Nested (N ts Tape) a Source #
CombineRefLists (a :-: as) Nil Source #
Instance details Defined in Sheet Methods (&) :: RefList (a :-: as) -> RefList Nil -> RefList ((a :-: as) & Nil) Source #
Take ('Relative :-: Nil) (Nested (F Tape)) Source #
Instance details Defined in Sheet Associated Types type ListFrom (Nested (F Tape)) a Source # Methods take :: RefList ('Relative :-: Nil) -> Nested (F Tape) a -> ListFrom (Nested (F Tape)) a Source #
(Functor (Nested ts), Take rs (Nested ts)) => Take ('Relative :-: rs) (Nested (N ts Tape)) Source #
Instance details Defined in Sheet Associated Types type ListFrom (Nested (N ts Tape)) a Source # Methods take :: RefList ('Relative :-: rs) -> Nested (N ts Tape) a -> ListFrom (Nested (N ts Tape)) a Source #
View ('Relative :-: Nil) (Nested (F Tape)) Source #
Instance details Defined in Sheet Associated Types type StreamFrom (Nested (F Tape)) a Source # Methods view :: RefList ('Relative :-: Nil) -> Nested (F Tape) a -> StreamFrom (Nested (F Tape)) a Source #
(Functor (Nested ts), View rs (Nested ts)) => View ('Relative :-: rs) (Nested (N ts Tape)) Source #
Instance details Defined in Sheet Associated Types type StreamFrom (Nested (N ts Tape)) a Source # Methods view :: RefList ('Relative :-: rs) -> Nested (N ts Tape) a -> StreamFrom (Nested (N ts Tape)) a Source #
(CombineRefTypes a b, CombineRefLists as bs) => CombineRefLists (a :-: as) (b :-: bs) Source #
Instance details Defined in Sheet Methods (&) :: RefList (a :-: as) -> RefList (b :-: bs) -> RefList ((a :-: as) & (b :-: bs)) Source #
type Tack (a :: k) (x :-: xs) Source #
Instance details Defined in Lists type Tack (a :: k) (x :-: xs) = x :-: Tack a xs
type Length (x :-: xs :: Type) Source #
Instance details Defined in Lists type Length (x :-: xs :: Type) = S (Length xs)

data Nil Source #

Instances

Instances details

HasLength Nil Source #
Instance details Defined in Lists Associated Types type Length Nil Source #
CombineRefLists Nil Nil Source #
Instance details Defined in Sheet Methods (&) :: RefList Nil -> RefList Nil -> RefList (Nil & Nil) Source #
Tackable (a :: k) Nil Source #
Instance details Defined in Lists Associated Types type Tack a Nil Source # Methods tack :: f a -> Conic f Nil -> Conic f (Tack a Nil) Source #
Go Nil (Nested ts :: Type -> Type) Source #
Instance details Defined in Sheet Methods go :: forall (a :: k). RefList Nil -> Nested ts a -> Nested ts a Source #
(Take Nil (Nested ts), Functor (Nested ts)) => Take Nil (Nested (N ts Tape)) Source #
Instance details Defined in Sheet Associated Types type ListFrom (Nested (N ts Tape)) a Source # Methods take :: RefList Nil -> Nested (N ts Tape) a -> ListFrom (Nested (N ts Tape)) a Source #
View Nil (Nested (F Tape)) Source #
Instance details Defined in Sheet Associated Types type StreamFrom (Nested (F Tape)) a Source # Methods view :: RefList Nil -> Nested (F Tape) a -> StreamFrom (Nested (F Tape)) a Source #
(View Nil (Nested ts), Functor (Nested ts)) => View Nil (Nested (N ts Tape)) Source #
Instance details Defined in Sheet Associated Types type StreamFrom (Nested (N ts Tape)) a Source # Methods view :: RefList Nil -> Nested (N ts Tape) a -> StreamFrom (Nested (N ts Tape)) a Source #
CombineRefLists Nil (b :-: bs) Source #
Instance details Defined in Sheet Methods (&) :: RefList Nil -> RefList (b :-: bs) -> RefList (Nil & (b :-: bs)) Source #
Go ('Relative :-: Nil) (Nested (F Tape)) Source #
Instance details Defined in Sheet Methods go :: forall (a :: k). RefList ('Relative :-: Nil) -> Nested (F Tape) a -> Nested (F Tape) a Source #
CombineRefLists (a :-: as) Nil Source #
Instance details Defined in Sheet Methods (&) :: RefList (a :-: as) -> RefList Nil -> RefList ((a :-: as) & Nil) Source #
Take ('Relative :-: Nil) (Nested (F Tape)) Source #
Instance details Defined in Sheet Associated Types type ListFrom (Nested (F Tape)) a Source # Methods take :: RefList ('Relative :-: Nil) -> Nested (F Tape) a -> ListFrom (Nested (F Tape)) a Source #
View ('Relative :-: Nil) (Nested (F Tape)) Source #
Instance details Defined in Sheet Associated Types type StreamFrom (Nested (F Tape)) a Source # Methods view :: RefList ('Relative :-: Nil) -> Nested (F Tape) a -> StreamFrom (Nested (F Tape)) a Source #
type Length Nil Source #
Instance details Defined in Lists type Length Nil = Z
type Tack (a :: k) Nil Source #
Instance details Defined in Lists type Tack (a :: k) Nil = a :-: Nil

Type-level conic manipulation

class ReifyNatural n => Replicable n (x :: k) Source #

Associated Types

type Replicate n x :: Type Source #

Instances

Instances details

Replicable Z (x :: k) Source #
Instance details Defined in Lists Associated Types type Replicate Z x Source #
Replicable n x => Replicable (S n) (x :: k) Source #
Instance details Defined in Lists Associated Types type Replicate (S n) x Source #

class Tackable (x :: k) (xs :: Type) where Source #

A Conic supports "tacking" a value onto its head.

Associated Types

type Tack x xs :: Type Source #

Methods

tack :: f x -> Conic f xs -> Conic f (Tack x xs) Source #

Instances

Instances details

Tackable (a :: k) Nil Source #
Instance details Defined in Lists Associated Types type Tack a Nil Source # Methods tack :: f a -> Conic f Nil -> Conic f (Tack a Nil) Source #
Tackable a xs => Tackable (a :: k) (x :-: xs) Source #
Instance details Defined in Lists Associated Types type Tack a (x :-: xs) Source # Methods tack :: f a -> Conic f (x :-: xs) -> Conic f (Tack a (x :-: xs)) Source #

class HasLength (ts :: k) Source #

A Conic length may be computed at the type level.

Associated Types

type Length ts :: Type Source #

Instances

Instances details

HasLength Nil Source #
Instance details Defined in Lists Associated Types type Length Nil Source #
HasLength (x :-: xs :: Type) Source #
Instance details Defined in Lists Associated Types type Length (x :-: xs) Source #

Conversion

heterogenize :: (a -> f t) -> Counted n a -> Conic f (Replicate n t) Source #

Turned a Counted list into a Conic list by means of some function from a to (f t).

homogenize :: (forall t. f t -> a) -> Conic f ts -> Counted (Length ts) a Source #

Given a function to collapse any (f t), turn a Conic list into a Counted list.