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