Data.List.Indexed.Conic

This module implements conic lists, which are lists where every element is of type (f a) for some a, but the a index may vary. This sits between homogeneous and fully heterogeneous lists in terms of expressivity and also the ease to manipulate.

Documentation

data x :-: y infixr 5

data Nil

data ConicList f ts where

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 of the list.

Constructors

(:-:) :: f a -> ConicList f rest -> ConicList f (a :-: rest) infixr 5

ConicNil :: ConicList f Nil

type family Replicate n x

Equations

Replicate Zero x = Nil

Replicate (Succ n) x = x :-: Replicate n x

type family Length ts

Equations

Length Nil = Zero

Length (x :-: xs) = Succ (Length xs)

type family Tack x xs

Equations

Tack a Nil = a :-: Nil

Tack a (x :-: xs) = x :-: Tack a xs

tack :: f t -> ConicList f ts -> ConicList f (Tack t ts)