Copyright	Copyright (C) 2015 Kyle Carter
License	BSD3
Maintainer	Kyle Carter <[email protected]>
Stability	experimental
Portability	RankNTypes
Safe Haskell	None
Language	Haskell2010

Data.Type.Length

Description

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

Documentation

data Length :: [k] -> * where Source #

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) Source #
Associated Types type WitnessC (ØC :: Constraint) ((Known N Nat n, Known [k] (Length k) as) :: Constraint) (Length k as) :: Constraint Source # Methods (\\) :: ØC => ((Known N Nat n, Known [k] (Length k) as) -> r) -> Length k as -> r Source #
Read1 [k] (Length k) Source #
Methods readsPrec1 :: Int -> ReadS (Some (Length k) f) Source #
Show1 [k] (Length k) Source #
Methods showsPrec1 :: Int -> f a -> ShowS Source # show1 :: f a -> String Source #
Ord1 [k] (Length k) Source #
Methods compare1 :: f a -> f a -> Ordering Source # (<#) :: f a -> f a -> Bool Source # (>#) :: f a -> f a -> Bool Source # (<=#) :: f a -> f a -> Bool Source # (>=#) :: f a -> f a -> Bool Source #
Eq1 [k] (Length k) Source #
Methods eq1 :: f a -> f a -> Bool Source # neq1 :: f a -> f a -> Bool Source #
Known [k] (Length k) (Ø k) Source #
Associated Types type KnownC (Length k) (Ø k :: Length k -> *) (a :: Length k) :: Constraint Source # Methods known :: Ø k a Source #
Known [k] (Length k) as => Known [k] (Length k) ((:<) k a as) Source #
Associated Types type KnownC (Length k) ((:<) k a as :: Length k -> *) (a :: Length k) :: Constraint Source # Methods known :: (k :< a) as a Source #
Eq (Length k as) Source #
Methods (==) :: Length k as -> Length k as -> Bool # (/=) :: Length k as -> Length k as -> Bool #
Ord (Length k as) Source #
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) Source #
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) Source #
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) Source #
type KnownC [k] (Length k) (Ø k) = ØC
type KnownC [k] (Length k) ((:<) k a as) Source #
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 Source #

lOdd :: Length as -> Bool Source #

lEven :: Length as -> Bool Source #