module Numeric.Dimensions.List
(
type (++), type (:+), type (+:)
, Empty, Cons, Snoc, Head
, Tail, Init, Last, Concat, Reverse, Take, Drop
, Suffix, Prefix, IsPrefix, IsSuffix
, ConcatList (..), FiniteList (..), TypeList (..)
, inferConcat, inferSuffix, inferPrefix, ConcatEvidence, FiniteListEvidence
, inferKnownLength
, inferTailFiniteList, inferConcatFiniteList
, inferPrefixFiniteList, inferSuffixFiniteList
, inferSnocFiniteList, inferInitFiniteList
, inferTakeNFiniteList, inferDropNFiniteList, inferReverseFiniteList
) where
import Data.Proxy (Proxy (..))
import Data.Type.Equality ((:~:)(..))
import Numeric.TypeLits
import Unsafe.Coerce (unsafeCoerce)
type (a :: k) :+ (as :: [k]) = a ': as
infixr 5 :+
type Cons (n :: k) (ns :: [k]) = n :+ ns
type (ns :: [k]) +: (n :: k) = Snoc ns n
infixl 5 +:
type Snoc (ns :: [k]) (n :: k) = GetSnoc (DoSnoc ns n)
type family (as :: [k]) ++ (bs :: [k]) :: [k] where
(++) '[] bs = bs
(++) as '[] = as
(++) (a :+ as) bs = a :+ (as ++ bs)
infixr 5 ++
type Concat (as :: [k]) (bs :: [k]) = as ++ bs
type Reverse (xs :: [k]) = Reversed (DoReverse xs)
type Empty = '[]
type family Take (n::Nat) (xs :: [k]) :: [k] where
Take _ '[] = '[]
Take 0 xs = '[]
Take n (x :+ xs) = x :+ Take (n1) xs
type family Drop (n::Nat) (xs :: [k]) :: [k] where
Drop _ '[] = '[]
Drop 0 xs = xs
Drop n (x :+ xs) = Drop (n1) xs
type family Suffix (as :: [k]) (asbs :: [k]) :: [k] where
Suffix '[] bs = bs
Suffix as as = '[]
Suffix (_ :+ as) (_ :+ asbs) = Suffix as asbs
type family Prefix (bs :: [k]) (asbs :: [k]) :: [k] where
Prefix '[] as = as
Prefix bs bs = '[]
Prefix bs asbs = Take (Length asbs Length bs) asbs
type family IsPrefix (as :: [k]) (asbs :: [k]) :: Bool where
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
IsSuffix '[] _ = 'True
IsSuffix bs bs = 'True
IsSuffix bs (_ :+ sbs) = IsSuffix bs sbs
IsSuffix _ _ = 'False
type family Head (xs :: [k]) :: k where
Head (x :+ xs) = x
Head '[] = TypeError ( 'Text
"Head -- empty type-level list."
)
type family Tail (xs :: [k]) :: [k] where
Tail (x :+ xs) = xs
Tail '[] = TypeError ( 'Text
"Tail -- empty type-level list."
)
type family Init (xs :: [k]) :: [k] where
Init '[x] = '[]
Init (x :+ xs) = x :+ Init xs
Init '[] = TypeError ( 'Text
"Init -- empty type-level list."
)
type family Last (xs :: [k]) :: k where
Last '[x] = x
Last (x :+ xs) = Last xs
Last '[] = TypeError ( 'Text
"Last -- empty type-level list."
)
class ( asbs ~ Concat as bs
, as ~ Prefix bs asbs
, bs ~ Suffix as asbs
, IsSuffix bs asbs ~ 'True
, IsPrefix as asbs ~ 'True
) => ConcatList (as :: [k]) (bs :: [k]) (asbs :: [k])
| as bs -> asbs
, as asbs -> bs
, bs asbs -> as where
tlPrefix :: ConcatEvidence as bs asbs -> Proxy as
tlSuffix :: ConcatEvidence as bs asbs -> Proxy bs
tlConcat :: ConcatEvidence as bs asbs -> Proxy asbs
instance ( asbs ~ Concat as bs
, as ~ Prefix bs asbs
, bs ~ Suffix as asbs
, IsSuffix bs asbs ~ 'True
, IsPrefix as asbs ~ 'True
) => ConcatList (as :: [k]) (bs :: [k]) (asbs :: [k]) where
tlPrefix _ = Proxy
tlSuffix _ = Proxy
tlConcat _ = Proxy
data TypeList (xs :: [k]) where
TLEmpty :: TypeList '[]
TLCons :: FiniteList xs => !(Proxy# x) -> !(TypeList xs) -> TypeList (x :+ xs)
instance Show (TypeList xs) where
show TLEmpty = "TLEmpty"
show (TLCons _ xs) = "TLCons " ++ show xs
class FiniteList (xs :: [k]) where
type Length xs :: Nat
order :: Int
tList :: TypeList xs
instance FiniteList ('[] :: [k]) where
type Length '[] = 0
order = 0
tList = TLEmpty
instance FiniteList xs => FiniteList (x :+ xs :: [k]) where
type Length (x :+ xs) = Length xs + 1
order = 1 + order @k @xs
tList = TLCons proxy# (tList @k @xs)
unsafeEqEvidence :: forall x y . Evidence (x ~ y)
unsafeEqEvidence = case (unsafeCoerce Refl :: x :~: y) of Refl -> Evidence
inferKnownLength :: forall xs . FiniteList xs => Evidence (KnownDim (Length xs))
inferKnownLength = reifyDim (order @_ @xs) f
where
f :: forall n . KnownDim n => Proxy# n -> Evidence (KnownDim (Length xs))
f _ = unsafeCoerce (Evidence @(KnownDim n))
inferTailFiniteList :: forall xs . FiniteList xs => Maybe (Evidence (FiniteList (Tail xs)))
inferTailFiniteList = case tList @_ @xs of
TLEmpty -> Nothing
TLCons _ _ -> Just Evidence
inferConcatFiniteList :: forall as bs
. (FiniteList as, FiniteList bs)
=> Evidence (FiniteList (as ++ bs))
inferConcatFiniteList = case tList @_ @as of
TLEmpty -> Evidence
TLCons _ (_ :: TypeList as') -> case inferConcatFiniteList @as' @bs of
Evidence -> case unsafeEqEvidence @(as ++ bs) @(Head as ': (as' ++ bs)) of
Evidence -> Evidence
inferPrefixFiniteList :: forall bs asbs
. (IsSuffix bs asbs ~ 'True, FiniteList bs, FiniteList asbs)
=> Evidence (FiniteList (Prefix bs asbs))
inferPrefixFiniteList = reifyDim (order @_ @asbs order @_ @bs) f
where
f :: forall n . KnownDim n => Proxy# n -> Evidence (FiniteList (Prefix bs asbs))
f _ = unsafeCoerce (inferTakeNFiniteList @n @asbs)
inferSuffixFiniteList :: forall as asbs
. (IsPrefix as asbs ~ 'True, FiniteList as, FiniteList asbs)
=> Evidence (FiniteList (Suffix as asbs))
inferSuffixFiniteList = case tList @_ @as of
TLEmpty -> Evidence
TLCons _ (_ :: TypeList as') -> case tList @_ @asbs of
TLCons _ (_ :: TypeList asbs') -> case unsafeEqEvidence @(IsPrefix as' asbs') @'True
`sumEvs` unsafeEqEvidence @(Suffix as' asbs') @(Suffix as asbs) of
Evidence -> inferSuffixFiniteList @as' @asbs'
inferSnocFiniteList :: forall xs z
. FiniteList xs
=> Evidence (FiniteList (xs +: z))
inferSnocFiniteList = case tList @_ @xs of
TLEmpty -> Evidence
TLCons _ (_ :: TypeList xs') -> case inferSnocFiniteList @xs' @z
`sumEvs` unsafeEqEvidence @(Head xs :+ (xs' +: z)) @(xs +: z) of
Evidence -> Evidence
inferInitFiniteList :: forall xs
. FiniteList xs
=> Maybe (Evidence (FiniteList (Init xs)))
inferInitFiniteList = case tList @_ @xs of
TLEmpty -> Nothing
TLCons _ TLEmpty -> Just Evidence
TLCons _ (TLCons _ _ :: TypeList xs') -> case inferInitFiniteList @xs' of
Just Evidence -> Just Evidence
Nothing -> Nothing
inferTakeNFiniteList :: forall n xs
. (KnownDim n, FiniteList xs)
=> Evidence (FiniteList (Take n xs))
inferTakeNFiniteList = magic @n @xs (dimVal' @n) (tList @_ @xs)
where
magic :: forall m ns . Int -> TypeList ns -> Evidence (FiniteList (Take m ns))
magic _ TLEmpty = Evidence
magic 0 _ = case unsafeEqEvidence @(Take m ns) @'[] of
Evidence -> Evidence
magic n (TLCons _ tl) = case unsafeEqEvidence @(Head ns ': Take (m1) (Tail ns)) @(Take m ns) of
Evidence -> case magic @(m1) @(Tail ns) (n1) tl of
Evidence -> Evidence
inferDropNFiniteList :: forall n xs
. (KnownDim n, FiniteList xs)
=> Evidence (FiniteList (Drop n xs))
inferDropNFiniteList = case magic (dimVal' @n) (tList @_ @xs) of
TLEmpty -> Evidence
TLCons _ _ -> Evidence
where
magic :: forall ns . Int -> TypeList ns -> TypeList (Drop n ns)
magic _ TLEmpty = TLEmpty
magic 0 tl = unsafeCoerce tl
magic n (TLCons _ tl) = unsafeCoerce $ magic (n1) tl
inferReverseFiniteList :: forall xs . FiniteList xs => Evidence (FiniteList (Reverse xs))
inferReverseFiniteList = case magic (tList @_ @xs) TLEmpty of
TLEmpty -> Evidence
TLCons _ _ -> Evidence
where
magic :: forall (ns :: [k]) (bs :: [k])
. FiniteList bs
=> TypeList ns -> TypeList bs -> TypeList (Reverse ns)
magic TLEmpty xs = unsafeCoerce xs
magic (TLCons p sx) xs = magic (unsafeCoerce sx :: TypeList ns) (TLCons p xs)
type ConcatEvidence (as :: [k]) (bs :: [k]) (asbs :: [k])
= Evidence ( asbs ~ Concat as bs
, as ~ Prefix bs asbs
, bs ~ Suffix as asbs
, IsSuffix bs asbs ~ 'True
, IsPrefix as asbs ~ 'True
)
type FiniteListEvidence (xs :: [k])
= Evidence (FiniteList xs)
inferConcat :: forall as bs . ConcatEvidence as bs (as ++ bs)
inferConcat = unsafeCoerce (Evidence :: ConcatEvidence ('[] :: [()]) ('[] :: [()]) ('[] :: [()]))
inferSuffix :: forall as asbs
. IsPrefix as asbs ~ 'True
=> ConcatEvidence as (Suffix as asbs) asbs
inferSuffix = unsafeCoerce (Evidence :: ConcatEvidence ('[] :: [()]) ('[] :: [()]) ('[] :: [()]))
inferPrefix :: forall bs asbs
. IsSuffix bs asbs ~ 'True
=> ConcatEvidence (Prefix bs asbs) bs asbs
inferPrefix = unsafeCoerce (Evidence :: ConcatEvidence ('[] :: [()]) ('[] :: [()]) ('[] :: [()]))
data Snocing k = SSingle k | Snocing [k]
type family DoSnoc (xs :: [k]) (z::k) = (ys :: Snocing k) | ys -> xs z where
DoSnoc '[] x = 'SSingle x
#if __GLASGOW_HASKELL__ >= 802
DoSnoc (x :+ xs :: [k]) (y :: k) = ('Snocing (x :+ GetSnoc (DoSnoc xs y) :: [k]) :: Snocing k)
#else
DoSnoc (x :+ xs :: [Nat]) (y :: Nat) = ('Snocing (x :+ GetSnoc (DoSnoc xs y) :: [Nat]) :: Snocing Nat)
DoSnoc (x :+ xs :: [XNat]) (y :: XNat) = ('Snocing (x :+ GetSnoc (DoSnoc xs y) :: [XNat]) :: Snocing XNat)
#endif
type family GetSnoc (xs :: Snocing k) = (ys :: [k]) | ys -> xs where
GetSnoc ('SSingle x) = '[x]
#if __GLASGOW_HASKELL__ >= 802
GetSnoc ('Snocing (y :+ x :+ xs)) = y :+ x :+ xs
#else
GetSnoc ('Snocing (y :+ x :+ xs) :: Snocing Nat) = (y :+ x :+ xs :: [Nat])
GetSnoc ('Snocing (y :+ x :+ xs) :: Snocing XNat) = (y :+ x :+ xs :: [XNat])
#endif
data Reversing k = REmpty | Reversing [k]
type family Reversed (ts :: Reversing k) = (rs :: [k]) | rs -> ts where
Reversed 'REmpty = '[]
#if __GLASGOW_HASKELL__ >= 802
Reversed ('Reversing (x :+ xs)) = x :+ xs
#else
Reversed ('Reversing (x :+ xs) :: Reversing Nat) = (x :+ xs :: [Nat])
Reversed ('Reversing (x :+ xs) :: Reversing XNat) = (x :+ xs :: [XNat])
#endif
type family DoReverse (as :: [k]) = (rs :: Reversing k) | rs -> as where
DoReverse '[] = 'REmpty
#if __GLASGOW_HASKELL__ >= 802
DoReverse (a :+ as) = 'Reversing (Reversed (DoReverse as) +: a)
#else
DoReverse (a :+ as :: [Nat]) = ('Reversing (Reversed (DoReverse as) +: a :: [Nat]) :: Reversing Nat)
DoReverse (a :+ as :: [XNat]) = ('Reversing (Reversed (DoReverse as) +: a :: [XNat]) :: Reversing XNat)
#endif