Copyright | (c) Artem Chirkin |
---|---|

License | BSD3 |

Maintainer | chirkin@arch.ethz.ch |

Safe Haskell | None |

Language | Haskell2010 |

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]`.

- type family (as :: [k]) ++ (bs :: [k]) :: [k] where ...
- type (:+) a as = a ': as
- type (+:) ns n = Snoc ns n
- type Empty = '[]
- type Cons n ns = n :+ ns
- type Snoc ns n = GetSnoc (DoSnoc ns n)
- type family Head (xs :: [k]) :: k where ...
- type family Tail (xs :: [k]) :: [k] where ...
- type family Init (xs :: [k]) :: [k] where ...
- type family Last (xs :: [k]) :: k where ...
- type Concat as bs = as ++ bs
- type Reverse xs = Reversed (DoReverse xs)
- type family Take (n :: Nat) (xs :: [k]) :: [k] where ...
- type family Drop (n :: Nat) (xs :: [k]) :: [k] where ...
- type family Suffix (as :: [k]) (asbs :: [k]) :: [k] where ...
- type family Prefix (bs :: [k]) (asbs :: [k]) :: [k] where ...
- type family IsPrefix (as :: [k]) (asbs :: [k]) :: Bool where ...
- type family IsSuffix (as :: [k]) (asbs :: [k]) :: Bool where ...
- 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
- class FiniteList xs where
- data TypeList xs where
- inferConcat :: forall as bs. ConcatEvidence as bs (as ++ bs)
- inferSuffix :: forall as asbs. IsPrefix as asbs ~ True => ConcatEvidence as (Suffix as asbs) asbs
- inferPrefix :: forall bs asbs. IsSuffix bs asbs ~ True => ConcatEvidence (Prefix bs asbs) bs asbs
- 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)
- type FiniteListEvidence xs = Evidence (FiniteList xs)
- inferKnownLength :: forall xs. FiniteList xs => Evidence (KnownDim (Length xs))
- inferTailFiniteList :: forall xs. FiniteList xs => Maybe (Evidence (FiniteList (Tail xs)))
- inferConcatFiniteList :: forall as bs. (FiniteList as, FiniteList bs) => Evidence (FiniteList (as ++ bs))
- inferPrefixFiniteList :: forall bs asbs. (IsSuffix bs asbs ~ True, FiniteList bs, FiniteList asbs) => Evidence (FiniteList (Prefix bs asbs))
- inferSuffixFiniteList :: forall as asbs. (IsPrefix as asbs ~ True, FiniteList as, FiniteList asbs) => Evidence (FiniteList (Suffix as asbs))
- inferSnocFiniteList :: forall xs z. FiniteList xs => Evidence (FiniteList (xs +: z))
- inferInitFiniteList :: forall xs. FiniteList xs => Maybe (Evidence (FiniteList (Init xs)))
- inferTakeNFiniteList :: forall n xs. (KnownDim n, FiniteList xs) => Evidence (FiniteList (Take n xs))
- inferDropNFiniteList :: forall n xs. (KnownDim n, FiniteList xs) => Evidence (FiniteList (Drop n xs))
- inferReverseFiniteList :: forall xs. FiniteList xs => Evidence (FiniteList (Reverse xs))

# Basic operations

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

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

# Working with concatenations

# 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 Source #

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

tlPrefix :: ConcatEvidence as bs asbs -> Proxy as Source #

tlSuffix :: ConcatEvidence as bs asbs -> Proxy bs Source #

tlConcat :: ConcatEvidence as bs asbs -> Proxy asbs Source #

class FiniteList xs where Source #

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

Length of a type-level list at term level

Get type-level constructed list

FiniteList k ([] k) Source # | |

FiniteList k xs => FiniteList k ((:+) k x xs) Source # | |

data TypeList xs where Source #

Type level list, used together with FiniteList typeclass

# Term level inference of type-level functions

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

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 Source #

`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 Source #

`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) Source #

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

type FiniteListEvidence xs = Evidence (FiniteList xs) Source #

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)) Source #

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

of the list

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

Tail of the list is also known list

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

Infer that concatenation is also finite

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

Infer that prefix is also finite

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

Infer that suffix is also finite

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

Make snoc almost as good as cons

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

Init of the list is also known list

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

Take KnownDim of the list is also known list

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

Drop KnownDim of the list is also known list

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

Reverse of the list is also known list