Maintainer | gatlin@niltag.net |
---|---|

Safe Haskell | Safe-Inferred |

Language | Haskell2010 |

## 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
- data (x :: k1) :-: (y :: k2)
- data Nil
- class ReifyNatural n => Replicable n (x :: k) where
- class Tackable (x :: k) (xs :: Type) where
- class HasLength (ts :: k) where
- 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.

forall t.n ~ S t => a ::: (Counted t a) infixr 5 | Prepend an item. |

n ~ Z => CountedNil | Construct an empty list. |

## Counted utilities

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]

# Conic Lists

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.

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

#### Instances

Tackable a xs => Tackable (a :: k) (x :-: xs) Source # | |

HasLength (x :-: xs :: Type) Source # | |

CombineRefLists Nil (b :-: bs) Source # | |

Go ('Relative :-: Nil) (Nested (F Tape)) Source # | |

(Go rs (Nested ts), Functor (Nested ts)) => Go ('Relative :-: rs) (Nested (N ts Tape) :: Type -> Type) Source # | |

CombineRefLists (a :-: as) Nil Source # | |

Take ('Relative :-: Nil) (Nested (F Tape)) Source # | |

(Functor (Nested ts), Take rs (Nested ts)) => Take ('Relative :-: rs) (Nested (N ts Tape)) Source # | |

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

(Functor (Nested ts), View rs (Nested ts)) => View ('Relative :-: rs) (Nested (N ts Tape)) Source # | |

(CombineRefTypes a b, CombineRefLists as bs) => CombineRefLists (a :-: as) (b :-: bs) Source # | |

type Tack (a :: k) (x :-: xs) Source # | |

type Length (x :-: xs :: Type) Source # | |

#### Instances

HasLength Nil Source # | |

CombineRefLists Nil Nil Source # | |

Tackable (a :: k) Nil Source # | |

Go Nil (Nested ts :: Type -> Type) Source # | |

(Take Nil (Nested ts), Functor (Nested ts)) => Take Nil (Nested (N ts Tape)) Source # | |

View Nil (Nested (F Tape)) Source # | |

(View Nil (Nested ts), Functor (Nested ts)) => View Nil (Nested (N ts Tape)) Source # | |

CombineRefLists Nil (b :-: bs) Source # | |

Go ('Relative :-: Nil) (Nested (F Tape)) Source # | |

CombineRefLists (a :-: as) Nil Source # | |

Take ('Relative :-: Nil) (Nested (F Tape)) Source # | |

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

type Length Nil Source # | |

type Tack (a :: k) Nil Source # | |

## Type-level conic manipulation

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

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

A `Conic`

supports "tacking" a value onto its head.