Numeric.Dimensions.List

Provides type-level operations on lists.

• Note for GHC 8.0 Due to GHC issue #13538 some complex type families could not be truly kind-polymorphic before GHC 8.2, thus I specialized them to work only on `[Nat]` and `[XNat]`.

Basic operations

type family (as :: [k]) ++ (bs :: [k]) :: [k] where ... infixr 5

List concatenation

Equations

'[] ++ bs = bs

as ++ '[] = as

(a :+ as) ++ bs = a :+ (as ++ bs)

type (:+) a as = a ': as infixr 5

Synonym for a type-level cons (injective, since this is just a synonym for the list constructor)

type (+:) ns n = Snoc ns n infixl 5

Synonym for a type-level snoc (injective!)

type Empty = '[]

Synonym for an empty type-level list

type Cons n ns = n :+ ns

Prefix-style synonym for cons

type Snoc ns n = GetSnoc (DoSnoc ns n)

Prefix-style synonym for snoc

type family Head (xs :: [k]) :: k where ...

Equations

Head (x :+ xs) = x

Head '[] = TypeError (Text "Head -- empty type-level list.")

type family Tail (xs :: [k]) :: [k] where ...

Equations

Tail (x :+ xs) = xs

Tail '[] = TypeError (Text "Tail -- empty type-level list.")

type family Init (xs :: [k]) :: [k] where ...

Equations

Init '[x] = '[]

Init (x :+ xs) = x :+ Init xs

Init '[] = TypeError (Text "Init -- empty type-level list.")

type family Last (xs :: [k]) :: k where ...

Equations

Last '[x] = x

Last (x :+ xs) = Last xs

Last '[] = TypeError (Text "Last -- empty type-level list.")

type Concat as bs = as ++ bs

Prefix-style synonym for concatenation

type Reverse xs = Reversed (DoReverse xs)

Reverse a type-level list (injective!)

type family Take (n :: Nat) (xs :: [k]) :: [k] where ...

Equations

Take _ '[] = '[]

Take 0 xs = '[]

Take n (x :+ xs) = x :+ Take (n - 1) xs

type family Drop (n :: Nat) (xs :: [k]) :: [k] where ...

Equations

Drop _ '[] = '[]

Drop 0 xs = xs

Drop n (x :+ xs) = Drop (n - 1) xs

Working with concatenations

type family Suffix (as :: [k]) (asbs :: [k]) :: [k] where ...

Equations

Suffix '[] bs = bs

Suffix as as = '[]

Suffix (_ :+ as) (_ :+ asbs) = Suffix as asbs

type family Prefix (bs :: [k]) (asbs :: [k]) :: [k] where ...

Equations

Prefix '[] as = as

Prefix bs bs = '[]

Prefix bs asbs = Take (Length asbs - Length bs) asbs

type family IsPrefix (as :: [k]) (asbs :: [k]) :: Bool where ...

Equations

IsPrefix '[] _ = True

IsPrefix (a :+ as) (a :+ asbs) = IsPrefix as asbs

IsPrefix as as = True

IsPrefix _ _ = False

type family IsSuffix (as :: [k]) (asbs :: [k]) :: Bool where ...

Equations

IsSuffix '[] _ = True

IsSuffix bs bs = True

IsSuffix bs (_ :+ sbs) = IsSuffix bs sbs

IsSuffix _ _ = False

Term level functions

class (asbs ~ Concat as bs, as ~ Prefix bs asbs, bs ~ Suffix as asbs, IsSuffix bs asbs ~ True, IsPrefix as asbs ~ True) => ConcatList as bs asbs | as bs -> asbs, as asbs -> bs, bs asbs -> as where

Represent a triple of lists forming a relation `as ++ bs ~ asbs`

Minimal complete definition

tlPrefix, tlSuffix, tlConcat

Methods

tlPrefix :: ConcatEvidence as bs asbs -> Proxy as

tlSuffix :: ConcatEvidence as bs asbs -> Proxy bs

tlConcat :: ConcatEvidence as bs asbs -> Proxy asbs

Instances

((~) [k] asbs (Concat k as bs), (~) [k] as (Prefix k bs asbs), (~) [k] bs (Suffix k as asbs), (~) Bool (IsSuffix k bs asbs) True, (~) Bool (IsPrefix k as asbs) True) => ConcatList k as bs asbs

Methods

tlPrefix :: ConcatEvidence as bs asbs asbs -> Proxy [as] bs

tlSuffix :: ConcatEvidence as bs asbs asbs -> Proxy [as] asbs

tlConcat :: ConcatEvidence as bs asbs asbs -> Proxy [as] asbs

class FiniteList xs where

Type-level list that is known to be finite. Basically, provides means to get its length and term-level rep (via TypeList)

Minimal complete definition

order, tList

Associated Types

type Length xs :: Nat

Length of a type-level list at type level

Methods

order :: Int

Length of a type-level list at term level

tList :: TypeList xs

Get type-level constructed list

Instances

FiniteList k ([] k)

Associated Types

type Length ([] k) (xs :: [[] k]) :: Nat

Methods

order :: Int

tList :: TypeList [k] xs

FiniteList k xs => FiniteList k ((:+) k x xs)

Associated Types

type Length ((:+) k x xs) (xs :: [(:+) k x xs]) :: Nat

Methods

order :: Int

tList :: TypeList ((k :+ x) xs) xs

data TypeList xs where

Type level list, used together with FiniteList typeclass

Constructors

TLEmpty :: TypeList '[]

TLCons :: FiniteList xs => !(Proxy# x) -> !(TypeList xs) -> TypeList (x :+ xs)

Instances

Show (TypeList k xs)

Methods

showsPrec :: Int -> TypeList k xs -> ShowS

show :: TypeList k xs -> String

showList :: [TypeList k xs] -> ShowS

Term level inference of type-level functions

inferConcat :: forall as bs. ConcatEvidence as bs (as ++ bs)

Any two type-level lists can be concatenated, so we just fool the compiler by unsafeCoercing proxy-like data type.

inferSuffix :: forall as asbs. IsPrefix as asbs ~ True => ConcatEvidence as (Suffix as asbs) asbs

as being prefix of asbs is enough to infer some concatenation relations so we just fool the compiler by unsafeCoercing proxy-like data type.

inferPrefix :: forall bs asbs. IsSuffix bs asbs ~ True => ConcatEvidence (Prefix bs asbs) bs asbs

bs being suffix of asbs is enough to infer some concatenation relations so we just fool the compiler by unsafeCoercing proxy-like data type.

type ConcatEvidence as bs asbs = Evidence (asbs ~ Concat as bs, as ~ Prefix bs asbs, bs ~ Suffix as asbs, IsSuffix bs asbs ~ True, IsPrefix as asbs ~ True)

Pattern-matching on the constructor of this type brings an evidence that `as ++ bs ~ asbs`

type FiniteListEvidence xs = Evidence (FiniteList xs)

Pattern-matching on the constructor of this type brings an evidence that the type-level parameter list is finite

inferKnownLength :: forall xs. FiniteList xs => Evidence (KnownDim (Length xs))

Length of a finite list is known and equal to order of the list

inferTailFiniteList :: forall xs. FiniteList xs => Maybe (Evidence (FiniteList (Tail xs)))

Tail of the list is also known list

inferConcatFiniteList :: forall as bs. (FiniteList as, FiniteList bs) => Evidence (FiniteList (as ++ bs))

Infer that concatenation is also finite

inferPrefixFiniteList :: forall bs asbs. (IsSuffix bs asbs ~ True, FiniteList bs, FiniteList asbs) => Evidence (FiniteList (Prefix bs asbs))

Infer that prefix is also finite

inferSuffixFiniteList :: forall as asbs. (IsPrefix as asbs ~ True, FiniteList as, FiniteList asbs) => Evidence (FiniteList (Suffix as asbs))

Infer that suffix is also finite

inferSnocFiniteList :: forall xs z. FiniteList xs => Evidence (FiniteList (xs +: z))

Make snoc almost as good as cons

inferInitFiniteList :: forall xs. FiniteList xs => Maybe (Evidence (FiniteList (Init xs)))

Init of the list is also known list

inferTakeNFiniteList :: forall n xs. (KnownDim n, FiniteList xs) => Evidence (FiniteList (Take n xs))

Take KnownDim of the list is also known list

inferDropNFiniteList :: forall n xs. (KnownDim n, FiniteList xs) => Evidence (FiniteList (Drop n xs))

Drop KnownDim of the list is also known list

inferReverseFiniteList :: forall xs. FiniteList xs => Evidence (FiniteList (Reverse xs))

Reverse of the list is also known list