Data.Type.Length

A singleton-esque type for representing lengths of type-level lists, irrespective of the actual types in that list.

Documentation

data Length :: [k] -> * where

Constructors

LZ :: Length Ø

LS :: !(Length as) -> Length (a :< as)

Instances

(~) N n (Len k as) => Witness ØC (Known N Nat n, Known [k] (Length k) as) (Length k as)

Associated Types

type WitnessC (ØC :: Constraint) ((Known N Nat n, Known [k] (Length k) as) :: Constraint) (Length k as) :: Constraint

Methods

(\\) :: ØC => ((Known N Nat n, Known [k] (Length k) as) -> r) -> Length k as -> r

Read1 [k] (Length k)

Methods

readsPrec1 :: Int -> ReadS (Some (Length k) f)

Show1 [k] (Length k)

Methods

showsPrec1 :: Int -> f a -> ShowS

show1 :: f a -> String

Ord1 [k] (Length k)

Methods

compare1 :: f a -> f a -> Ordering

(<#) :: f a -> f a -> Bool

(>#) :: f a -> f a -> Bool

(<=#) :: f a -> f a -> Bool

(>=#) :: f a -> f a -> Bool

Eq1 [k] (Length k)

Methods

eq1 :: f a -> f a -> Bool

neq1 :: f a -> f a -> Bool

Known [k] (Length k) (Ø k)

Associated Types

type KnownC (Length k) (Ø k :: Length k -> *) (a :: Length k) :: Constraint

Methods

known :: Ø k a

Known [k] (Length k) as => Known [k] (Length k) ((:<) k a as)

Associated Types

type KnownC (Length k) ((:<) k a as :: Length k -> *) (a :: Length k) :: Constraint

Methods

known :: (k :< a) as a

Eq (Length k as)

Methods

(==) :: Length k as -> Length k as -> Bool

(/=) :: Length k as -> Length k as -> Bool

Ord (Length k as)

Methods

compare :: Length k as -> Length k as -> Ordering

(<) :: Length k as -> Length k as -> Bool

(<=) :: Length k as -> Length k as -> Bool

(>) :: Length k as -> Length k as -> Bool

(>=) :: Length k as -> Length k as -> Bool

max :: Length k as -> Length k as -> Length k as

min :: Length k as -> Length k as -> Length k as

Show (Length k as)

Methods

showsPrec :: Int -> Length k as -> ShowS

show :: Length k as -> String

showList :: [Length k as] -> ShowS

type WitnessC ØC (Known N Nat n, Known [k] (Length k) as) (Length k as)

type WitnessC ØC (Known N Nat n, Known [k] (Length k) as) (Length k as) = (~) N n (Len k as)

type KnownC [k] (Length k) (Ø k)

type KnownC [k] (Length k) (Ø k) = ØC

type KnownC [k] (Length k) ((:<) k a as)

type KnownC [k] (Length k) ((:<) k a as) = Known [k] (Length k) as

elimLength :: p Ø -> (forall x xs. Length xs -> p xs -> p (x :< xs)) -> Length as -> p as

lOdd :: Length as -> Bool

lEven :: Length as -> Bool