garden
Maintainergatlin@niltag.net
Safe HaskellSafe
LanguageHaskell2010

Lists

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

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
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 #

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 #

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 #

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 #

CombineRefLists Nil (b :-: bs) Source # 
Instance details

Defined in Sheet

Methods

(&) :: RefList Nil -> RefList (b :-: bs) -> RefList (Nil & (b :-: bs)) 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 #

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 #

HasLength xs => HasLength (x :-: xs :: Type) Source # 
Instance details

Defined in Lists

Associated Types

type Length (x :-: xs) Source #

CombineRefLists (a :-: as) Nil Source # 
Instance details

Defined in Sheet

Methods

(&) :: RefList (a :-: as) -> RefList Nil -> RefList ((a :-: as) & Nil) 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 #

View ('Relative :-: Nil) (Nested (F Tape)) Source # 
Instance details

Defined in Sheet

Associated Types

type StreamFrom (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 #

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 #

(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
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 #

(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 #

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 #

(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 #

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 #

HasLength Nil Source # 
Instance details

Defined in Lists

Associated Types

type Length Nil Source #

CombineRefLists (a :-: as) Nil Source # 
Instance details

Defined in Sheet

Methods

(&) :: RefList (a :-: as) -> RefList Nil -> RefList ((a :-: as) & Nil) Source #

View ('Relative :-: Nil) (Nested (F Tape)) Source # 
Instance details

Defined in Sheet

Associated Types

type StreamFrom (Nested (F Tape)) a 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 #

type Tack (a :: k) Nil Source # 
Instance details

Defined in Lists

type Tack (a :: k) Nil = a :-: Nil
type Length Nil Source # 
Instance details

Defined in Lists

type Length Nil = Z

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 xs => 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.